Source indexedlemma · leanprover/lean4:v4.32.0

const_n_prop_3

Carleson.TileExistence · Carleson/TileExistence.lean:1330 to 1340

Mathematical statement

Exact Lean statement

lemma const_n_prop_3 (ht : t ∈ Ioo 0 1) :
    (t * D ^ K' : ℝ)⁻¹ ≤ ↑D ^ (const_n a ht * K')

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma const_n_prop_3 (ht : t ∈ Ioo 0 1) :    (t * D ^ K' : ℝ)⁻¹ ≤ ↑D ^ (const_n a ht * K') := by  dsimp only [const_n]  rw [mul_inv, ← div_eq_mul_inv, div_le_iff₀ (by positivity [realD_pos a]), ← pow_add]  nth_rw 3 [← one_mul K']  rw [← right_distrib]  nth_rw 1 [← Real.rpow_logb (realD_pos a) (one_lt_realD X).ne.symm ht.left]  rw [← Real.rpow_neg (realD_nonneg a), ← Real.rpow_natCast, Real.rpow_le_rpow_left_iff (one_lt_realD X)]  push_cast  rw [← div_le_iff₀ (K_pos)]  exact Nat.lt_floor_add_one (-Real.logb (↑D) t / ↑const_K) |>.le