Source indexedlemma · leanprover/lean4:v4.32.0

ball_bound

Carleson.TileExistence · Carleson/TileExistence.lean:16 to 37

Mathematical statement

Exact Lean statement

lemma ball_bound {Y : Set X} (k : ℤ) (hk_lower : -S ≤ k)
    (hY : Y ⊆ ball o (4 * D ^ (S : ℤ) - D ^ k)) (y : X) (hy : y ∈ Y) :
    ball o (4 * D ^ (S : ℤ)) ⊆ ball y (8 * D ^ (2 * S : ℤ) * D ^ k)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ball_bound {Y : Set X} (k : ℤ) (hk_lower : -S ≤ k)    (hY : Y ⊆ ball o (4 * D ^ (S : ℤ) - D ^ k)) (y : X) (hy : y ∈ Y) :    ball o (4 * D ^ (S : ℤ)) ⊆ ball y (8 * D ^ (2 * S : ℤ) * D ^ k) := by  calc    ball o (4 * D ^ (S:ℤ))      ⊆ ball y (2 * (4 * D ^ (S:ℤ)):ℝ) := by        rw [two_mul]        refine ball_subset ?h        simp only [add_sub_cancel_right]        obtain hy' := hY hy        rw [mem_ball, dist_comm] at hy'        apply hy'.le.trans        rw [tsub_le_iff_right, le_add_iff_nonneg_right]        positivity    _ = ball y (8 * D ^ (S : ℤ) : ℝ) := by congr! 1; ring    _ ⊆ ball y (8 * D ^ (2 * S : ℤ) * D ^ k) := by        apply ball_subset_ball        rw [mul_assoc]        gcongr        rw [← zpow_add₀ (realD_pos a).ne.symm]        apply zpow_le_zpow_right₀ (one_le_realD a)        linarith