Source indexedlemma · leanprover/lean4:v4.32.0

Real.one_le_dyadicRadius_succ_of_inv_le_two_pow

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/Dyadic.lean:89 to 105

Source documentation

Once the dyadic scale is past r₀⁻¹, the upper endpoint r₀ 2^(k+1) is at least 1.

Exact Lean statement

lemma one_le_dyadicRadius_succ_of_inv_le_two_pow
    {r0 : ℝ} {k0 kk : ℕ} (hr0 : 0 < r0)
    (hk0 : ∀ n ≥ k0, (1 / r0 : ℝ) ≤ (2 : ℝ) ^ n) (hkk : k0 ≤ kk + 1) :
    (1 : ℝ) ≤ r0 * (2 : ℝ) ^ ((kk : ℝ) + 1)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma one_le_dyadicRadius_succ_of_inv_le_two_pow    {r0 : ℝ} {k0 kk : ℕ} (hr0 : 0 < r0)    (hk0 : ∀ n ≥ k0, (1 / r0 : ℝ) ≤ (2 : ℝ) ^ n) (hkk : k0 ≤ kk + 1) :    (1 : ℝ) ≤ r0 * (2 : ℝ) ^ ((kk : ℝ) + 1) := by  have hr0ne : r0 ≠ 0 := ne_of_gt hr0  have hpow_nat : (1 / r0 : ℝ) ≤ (2 : ℝ) ^ (kk + 1) := hk0 (kk + 1) hkk  have hpow_rpow : (1 / r0 : ℝ) ≤ (2 : ℝ) ^ ((kk : ℝ) + 1) := by    have hcast : (2 : ℝ) ^ ((kk : ℝ) + 1) = (2 : ℝ) ^ (kk + 1) := by      calc        (2 : ℝ) ^ ((kk : ℝ) + 1) = (2 : ℝ) ^ ((kk + 1 : ℕ) : ℝ) := by          simp [Nat.cast_add, Nat.cast_one]        _ = (2 : ℝ) ^ (kk + 1) := by          simpa using (Real.rpow_natCast (2 : ℝ) (kk + 1))    simpa [hcast] using hpow_nat  have : (r0 * (1 / r0) : ℝ) ≤ r0 * (2 : ℝ) ^ ((kk : ℝ) + 1) :=    mul_le_mul_of_nonneg_left hpow_rpow hr0.le  simpa [one_div, hr0ne, mul_assoc] using this