Source indexedlemma · leanprover/lean4:v4.32.0

small_boundary

Carleson.TileExistence · Carleson/TileExistence.lean:1148 to 1160

Mathematical statement

Exact Lean statement

lemma small_boundary (k : ℤ) (hk : -S ≤ k) (hk_mK : -S ≤ k - K') (y : Yk X k) :
    ∑' (z : Yk X (k - K')), ∑ᶠ (_ : clProp(hk_mK,z|hk,y)), volume (I3 hk_mK z)
      ≤ 2⁻¹ * volume (I3 hk y)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma small_boundary (k : ℤ) (hk : -S ≤ k) (hk_mK : -S ≤ k - K') (y : Yk X k) :    ∑' (z : Yk X (k - K')), ∑ᶠ (_ : clProp(hk_mK,z|hk,y)), volume (I3 hk_mK z)      ≤ 2⁻¹ * volume (I3 hk y) := by  calc    ∑' (z : Yk X (k - K')), ∑ᶠ (_ : clProp(hk_mK,z|hk,y)), volume (I3 hk_mK z)    _ = ∑' (z : Yk X (k - K')), volume (⋃ (_ : clProp(hk_mK,z|hk,y)), I3 hk_mK z) := by      congr with z      classical      rw [finsum_eq_if, iUnion_eq_if]      by_cases h : clProp(hk_mK, z | hk, y)      · simp_rw [if_pos h]      · simp_rw [if_neg h, measure_empty]    _ ≤ 2⁻¹ * volume (I3 hk y) := small_boundary' k hk hk_mK y