Source indexedlemma · leanprover/lean4:v4.32.0

Real.dyadicShell_lower_bound

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/Dyadic.lean:50 to 63

Source documentation

If k = ⌊log₂ (x / r₀)⌋, then r₀ * 2^k is a lower dyadic bound for x.

Exact Lean statement

lemma dyadicShell_lower_bound {r0 x : ℝ} {k : ℕ} (hr0 : 0 < r0) (hx : r0 ≤ x)
    (hk : ⌊Real.logb 2 (x / r0)⌋₊ = k) :
    r0 * (2 : ℝ) ^ (k : ℝ) ≤ x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma dyadicShell_lower_bound {r0 x : ℝ} {k : ℕ} (hr0 : 0 < r0) (hx : r0 ≤ x)    (hk : ⌊Real.logb 2 (x / r0)⌋₊ = k) :    r0 * (2 : ℝ) ^ (k : ℝ) ≤ x := by  have hr0ne : r0 ≠ 0 := ne_of_gt hr0  have hx1 : (1 : ℝ) ≤ x / r0 := by    have : r0 / r0 ≤ x / r0 := div_le_div_of_nonneg_right hx hr0.le    simpa [hr0ne] using this  have hle : (2 : ℝ) ^ (k : ℝ) ≤ x / r0 := by    have := Real.two_pow_floor_logb_le (x := x / r0) hx1    simpa [hk] using this  have := mul_le_mul_of_nonneg_left hle hr0.le  have hxEq : r0 * (x / r0) = x := by    field_simp [hr0ne]  simpa [mul_assoc, hxEq] using this