Source indexedlemma · leanprover/lean4:v4.32.0

calculation_convexity_bound

Carleson.Calculations · Carleson/Calculations.lean:295 to 311

Mathematical statement

Exact Lean statement

lemma calculation_convexity_bound [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G]
    {n : ℕ} {t : ℝ} (ht : t ∈ Set.Icc 0 1) :
    ∑ k ∈ Finset.range n, ((D : ENNReal) ^ (-t)) ^ k ≤ 2 * (ENNReal.ofReal t)⁻¹

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma calculation_convexity_bound [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G]    {n : ℕ} {t : ℝ} (ht : t ∈ Set.Icc 0 1) :    ∑ k ∈ Finset.range n, ((D : ENNReal) ^ (-t)) ^ k ≤ 2 * (ENNReal.ofReal t)⁻¹ := by  have a4 := four_le_a X  refine le_trans ?_ (near_1_geometric_bound ht)  calc    _ ≤ ∑ k ∈ Finset.range n, ((2 : ENNReal) ^ (-t)) ^ k := by      refine Finset.sum_le_sum fun k mk ↦ pow_le_pow_left' ?_ k      rw [ENNReal.rpow_neg, ENNReal.rpow_neg, ENNReal.inv_le_inv]      refine ENNReal.rpow_le_rpow ?_ ht.1      unfold defaultD      norm_cast      apply Nat.le_pow      have : 0 < 𝕔 := by linarith [seven_le_c]      positivity    _ ≤ ∑' k : ℕ, ((2 : ENNReal) ^ (-t)) ^ k := ENNReal.sum_le_tsum _    _ = _ := ENNReal.tsum_geometric _