Source indexedlemma · leanprover/lean4:v4.32.0

volume_xDsp_bound

Carleson.TileStructure · Carleson/TileStructure.lean:101 to 111

Source documentation

A bound used in both nontrivial cases of Lemma 7.5.5.

Exact Lean statement

lemma volume_xDsp_bound {x : X} (hx : x ∈ 𝓘 p) :
    volume (ball (𝔠 p) (4 * D ^ 𝔰 p)) / 2 ^ (3 * a) ≤ volume (ball x (D ^ 𝔰 p))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma volume_xDsp_bound {x : X} (hx : x ∈ 𝓘 p) :    volume (ball (𝔠 p) (4 * D ^ 𝔰 p)) / 2 ^ (3 * a) ≤ volume (ball x (D ^ 𝔰 p)) := by  apply ENNReal.div_le_of_le_mul'  have h : dist x (𝔠 p) + 4 * D ^ 𝔰 p ≤ 8 * D ^ 𝔰 p := by    calc      _ ≤ 4 * (D : ℝ) ^ 𝔰 p + 4 * ↑D ^ 𝔰 p := by        gcongr; exact (mem_ball.mp (Grid_subset_ball hx)).le      _ = _ := by rw [← add_mul]; norm_num  convert measure_ball_le_of_dist_le' (μ := volume) (by norm_num) h  unfold As defaultA; norm_cast  rw [← pow_mul', show (8 : ℕ) = 2 ^ 3 by norm_num, Nat.clog_pow]; norm_num