Source indexedlemma · leanprover/lean4:v4.32.0

boundary_sum_eq

Carleson.TileExistence · Carleson/TileExistence.lean:1171 to 1185

Mathematical statement

Exact Lean statement

lemma boundary_sum_eq {k : ℤ} (hk : -S ≤ k) {k' : ℤ} (hk' : -S ≤ k') (y : Yk X k) :
    ∑'(y' : Yk X k'), ∑ᶠ (_ : clProp(hk',y'|hk,y)), volume (I3 hk' y') =
      volume (⋃ (y' : Yk X k'), ⋃ (_ : clProp(hk',y'|hk,y)), I3 hk' y')

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma boundary_sum_eq {k : ℤ} (hk : -S ≤ k) {k' : ℤ} (hk' : -S ≤ k') (y : Yk X k) :    ∑'(y' : Yk X k'), ∑ᶠ (_ : clProp(hk',y'|hk,y)), volume (I3 hk' y') =      volume (⋃ (y' : Yk X k'), ⋃ (_ : clProp(hk',y'|hk,y)), I3 hk' y') := by  have := (Yk_countable X k').to_subtype  rw [measure_iUnion]  · congr with y'    classical    rw [finsum_eq_if, iUnion_eq_if]    by_cases h: clProp(hk', y' | hk, y) <;> simp [h]  · intro i i' hneq    simp only [disjoint_iUnion_right, disjoint_iUnion_left]    rw [Set.disjoint_iff]    intro _ _ x hx    exact hneq (I3_prop_1 _ hx)  exact fun y' ↦ MeasurableSet.iUnion (fun _ ↦ I3_measurableSet hk' y')