Tile sum operator

theorem tile_sum_operator {G' : Set X} {f : X → ℂ} {x : X} (hx : x ∈ G \ G') :    ∑ (p : 𝔓 X), carlesonOn p f x =    ∑ s ∈ Icc (σ₁ x) (σ₂ x), ∫ y, Ks s x y * f y * exp (I * (Q x y - Q x x)) := by  classical  rw [𝔓_biUnion, Finset.sum_biUnion]; swap  · exact fun s _ s' _ hss' A hAs hAs' p pA ↦ False.elim <| hss' (𝔰_eq (hAs pA) ▸ 𝔰_eq (hAs' pA))  rw [← (Icc (-S : ℤ) S).toFinset.sum_filter_add_sum_filter_not (fun s ↦ s ∈ Icc (σ₁ x) (σ₂ x))]  rw [Finset.sum_eq_zero sum_eq_zero_of_notMem_Icc, add_zero]  refine Finset.sum_congr (Finset.ext fun s ↦ ⟨fun hs ↦ ?_, fun hs ↦ ?_⟩) (fun s hs ↦ ?_)  · rw [Finset.mem_filter, ← mem_toFinset] at hs    exact hs.2  · rw [mem_toFinset] at hs    rw [toFinset_Icc, Finset.mem_filter]    exact ⟨Finset.mem_Icc.2 (Icc_σ_subset_Icc_S hs), hs⟩  · rcases exists_Grid hx.1 hs with ⟨I, Is, xI⟩    obtain ⟨p, 𝓘pI, Qp⟩ : ∃ (p : 𝔓 X), 𝓘 p = I ∧ Q x ∈ Ω p := by simpa using! biUnion_Ω ⟨x, rfl⟩    have p𝔓Xs : p ∈ 𝔓X_s s := Finset.mem_filter.mpr ⟨Finset.mem_univ _, by rw [𝔰, 𝓘pI]; exact Is⟩    have : ∀ p' ∈ 𝔓X_s s, p' ≠ p → carlesonOn p' f x = 0 := by      intro p' p'𝔓Xs p'p      apply indicator_of_notMem      simp only [E, mem_setOf_eq, not_and]      refine fun x_in_𝓘p' Qp' ↦ False.elim ?_      have s_eq := 𝔰_eq p𝔓Xs ▸ 𝔰_eq p'𝔓Xs      have : ¬ Disjoint (𝓘 p' : Set X) (𝓘 p : Set X) := not_disjoint_iff.2 ⟨x, x_in_𝓘p', 𝓘pI ▸ xI⟩      exact disjoint_left.1 (disjoint_Ω p'p <| Or.resolve_right (eq_or_disjoint s_eq) this) Qp' Qp    rw [Finset.sum_eq_single_of_mem p p𝔓Xs this]    have xEp : x ∈ E p :=      ⟨𝓘pI ▸ xI, Qp, by simpa only [toFinset_Icc, Finset.mem_Icc, 𝔰_eq p𝔓Xs] using! hs⟩    simp_rw [carlesonOn_def', indicator_of_mem xEp, 𝔰_eq p𝔓Xs]