Source indexedlemma · leanprover/lean4:v4.32.0

Real.two_pow_floor_logb_le

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/Dyadic.lean:28 to 37

Source documentation

The dyadic lower endpoint associated to ⌊log₂ x⌋ is at most x, for 1 ≤ x.

Exact Lean statement

lemma two_pow_floor_logb_le {x : ℝ} (hx : 1 ≤ x) :
    (2 : ℝ) ^ (⌊Real.logb 2 x⌋₊ : ℝ) ≤ x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma two_pow_floor_logb_le {x : ℝ} (hx : 1 ≤ x) :    (2 : ℝ) ^ (⌊Real.logb 2 x⌋₊ : ℝ) ≤ x := by  have hx0 : 0 < x := lt_of_lt_of_le (by norm_num : (0 : ℝ) < 1) hx  have hlog_nonneg : 0 ≤ Real.logb 2 x :=    Real.logb_nonneg (b := (2 : ℝ)) (by norm_num : (1 : ℝ) < 2) hx  have hfloor_le : (⌊Real.logb 2 x⌋₊ : ℝ) ≤ Real.logb 2 x := by    simpa using (Nat.floor_le hlog_nonneg)  exact (Real.le_logb_iff_rpow_le (b := (2 : ℝ))    (x := (⌊Real.logb 2 x⌋₊ : ℝ)) (y := x)    (by norm_num : (1 : ℝ) < 2) hx0).1 hfloor_le