Source indexedlemma · leanprover/lean4:v4.32.0

calculation_3

Carleson.Calculations · Carleson/Calculations.lean:85 to 103

Mathematical statement

Exact Lean statement

lemma calculation_3 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {x y : ℤ} (h : x + 3 < y) :
    100 * D ^ (x + 3) + ((4 * D ^ (-2 : ℝ)) * D ^ (x + 3)) + (((8 : ℝ)⁻¹ * D ^ (-3 : ℝ)) * D ^ (x + 3)) + 8 * D ^ y < 10 * D ^ y

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma calculation_3 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {x y : ℤ} (h : x + 3 < y) :    100 * D ^ (x + 3) + ((4 * D ^ (-2 : ℝ)) * D ^ (x + 3)) + (((8 : ℝ)⁻¹ * D ^ (-3 : ℝ)) * D ^ (x + 3)) + 8 * D ^ y < 10 * D ^ y := by  rw [← show (2 : ℝ) + 8 = 10 by norm_num, right_distrib]  gcongr  rw [← distrib_three_right ..]  calc (100 + 4 * (D : ℝ) ^ (-2 : ℝ) + 8⁻¹ * D ^ (-3 : ℝ)) * D ^ (x + 3)  _ ≤ (100 + 4 * (D : ℝ) ^ (-2 : ℝ) + 8⁻¹ * D ^ (-3 : ℝ)) * D ^ (y - 1) := by    have h1 : x + 3 ≤ y - 1 := by lia    gcongr    linarith [four_le_realD X]  _ = (100 + 4 * (D : ℝ) ^ (-2 : ℝ) + 8⁻¹ * D ^ (-3 : ℝ)) * (D ^ (y) * D ^ (- 1 : ℝ)) := by    congr    exact_mod_cast Real.rpow_add (y := y) (z:= (-1)) (hx := realD_pos a)  _ < 2 * D ^ y := by    nth_rw 4 [mul_comm ..]    rw [← mul_assoc ..]    have D_pos : (0 : ℝ) < D := realD_pos a    gcongr    exact calculation_10 (hundred_lt_realD X)