Source indexedlemma · leanprover/lean4:v4.32.0

calculation_14

Carleson.Calculations · Carleson/Calculations.lean:235 to 246

Mathematical statement

Exact Lean statement

lemma calculation_14 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (n : ℕ) :
    (2 : ℝ) ^ ((Z : ℝ) * n / 2 - (2 * 𝕔 + 1) * a ^ 3) ≤
      2 ^ ((Z : ℝ) * n / 2 - (2 * 𝕔 * a ^ 3 + 4 * a))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma calculation_14 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (n : ℕ) :    (2 : ℝ) ^ ((Z : ℝ) * n / 2 - (2 * 𝕔 + 1) * a ^ 3) ≤      2 ^ ((Z : ℝ) * n / 2 - (2 * 𝕔 * a ^ 3 + 4 * a)) := by  gcongr  · linarith  rw [show (2 * 𝕔 + 1) * (a : ℝ) ^ 3 = 2 * 𝕔 * (a : ℝ) ^ 3 + a ^ 3 by ring]  gcongr _ + ?_  rw [show (a : ℝ) ^ 3 = a ^ 2 * a by ring]  gcongr  suffices 4 ^ 2 ≤ (a : ℝ) ^ 2 by linarith  apply pow_le_pow_left₀ (ha := by linarith)  exact_mod_cast four_le_a X