Source indexedlemma · leanprover/lean4:v4.32.0

near_1_geometric_bound

Carleson.Calculations · Carleson/Calculations.lean:282 to 293

Source documentation

A bound on the sum of a geometric series whose ratio is close to 1.

Exact Lean statement

lemma near_1_geometric_bound {t : ℝ} (ht : t ∈ Set.Icc 0 1) :
    (1 - 2 ^ (-t))⁻¹ ≤ 2 * (ENNReal.ofReal t)⁻¹

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma near_1_geometric_bound {t : ℝ} (ht : t ∈ Set.Icc 0 1) :    (1 - 2 ^ (-t))⁻¹ ≤ 2 * (ENNReal.ofReal t)⁻¹ := by  obtain ⟨lb, ub⟩ := ht  rw [ENNReal.inv_le_iff_inv_le, ENNReal.mul_inv (.inl two_ne_zero) (.inl ENNReal.ofNat_ne_top),    inv_inv, ← ENNReal.div_eq_inv_mul, ← ENNReal.ofReal_ofNat 2, ← ENNReal.ofReal_one,    ← ENNReal.ofReal_div_of_pos (by positivity), ENNReal.ofReal_rpow_of_pos (by positivity),    ← ENNReal.ofReal_sub _ (by positivity)]  apply ENNReal.ofReal_le_ofReal; change t / 2 ≤ 1 - 2 ^ (-t)  have bne := rpow_one_add_le_one_add_mul_self (show -1 ≤ -1 / 2 by norm_num) lb ub  rw [show (1 : ℝ) + -1 / 2 = 2⁻¹ by norm_num, Real.inv_rpow zero_le_two,    ← Real.rpow_neg zero_le_two] at bne  linarith only [bne]