Source indexedlemma · leanprover/lean4:v4.32.0

Real.dyadicShell_upper_bound

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/Dyadic.lean:66 to 79

Source documentation

If k = ⌊log₂ (x / r₀)⌋, then x is bounded by the next dyadic endpoint.

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma dyadicShell_upper_bound {r0 x : ℝ} {k : ℕ} (hr0 : 0 < r0) (hx : r0 ≤ x)    (hk : ⌊Real.logb 2 (x / r0)⌋₊ = k) :    x ≤ r0 * (2 : ℝ) ^ ((k : ℝ) + 1) := 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 hlt : x / r0 < (2 : ℝ) ^ ((k : ℝ) + 1) := by    have := Real.lt_two_pow_floor_logb_add_one (x := x / r0) hx1    simpa [hk] using this  have := mul_lt_mul_of_pos_left hlt hr0  have hxEq : r0 * (x / r0) = x := by    field_simp [hr0ne]  exact le_of_lt (by simpa [mul_assoc, hxEq] using this)