Source indexedlemma · leanprover/lean4:v4.32.0

tsum_czRemainder'

Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:737 to 748

Source documentation

Part of Lemma 10.2.5, this is essentially (10.2.16) (both cases).

Exact Lean statement

lemma tsum_czRemainder' (hX : GeneralCase f α) (x : X) :
    ∑' i, czRemainder' hX i x = czRemainder f α x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma tsum_czRemainder' (hX : GeneralCase f α) (x : X) :    ∑' i, czRemainder' hX i x = czRemainder f α x := by  simp only [czRemainder', czRemainder]  by_cases hx : ∃ j, x ∈ czPartition hX j  · have ⟨j, hj⟩ := hx    rw [tsum_eq_single j, indicator_of_mem hj]    · rfl    · refine fun i hi ↦ indicator_of_notMem ?_ _      exact (czPartition_pairwise_disjoint_on hi).notMem_of_mem_right hj  · simp only [czApproximation, hX, reduceDIte, hx, sub_self]    convert tsum_zero with i    exact indicator_of_notMem (fun hi ↦ hx ⟨i, hi⟩) _