carlesonSum_𝔓₁_compl_eq_𝔓pos_inter

lemma carlesonSum_𝔓₁_compl_eq_𝔓pos_inter (f : X → ℂ) :    ∀ᵐ x, x ∈ G \ G' → carlesonSum 𝔓₁ᶜ f x = carlesonSum (𝔓pos (X := X) ∩ 𝔓₁ᶜ) f x := by  have A p (hp : p ∈ (𝔓pos (X := X))ᶜ) : ∀ᵐ x, x ∈ G \ G' → x ∉ 𝓘 p := by    simp only [𝔓pos, mem_compl_iff, mem_setOf_eq, not_lt, nonpos_iff_eq_zero] at hp    filter_upwards [measure_eq_zero_iff_ae_notMem.mp hp] with x hx h'x (h''x : x ∈ (𝓘 p : Set X))    exact hx ⟨⟨h''x, h'x.1⟩, h'x.2⟩  rw [← ae_ball_iff (to_countable 𝔓posᶜ)] at A  filter_upwards [A] with x hx h'x  simp only [carlesonSum]  symm  apply Finset.sum_subset  · intro p hp    simp_rw [Finset.mem_filter_univ] at hp ⊢    exact hp.2  · intro p hp h'p    simp_rw [Finset.mem_filter_univ] at hp h'p    simp only [mem_inter_iff, hp, and_true] at h'p    have : x ∉ 𝓘 p := hx _ h'p h'x    have : x ∉ E p := by simp at this; simp [E, this]    simp [carlesonOn, this]