TileStructure.Forest.adjointCarlesonRowSum_adjoint

lemma adjointCarlesonRowSum_adjoint    (hf : BoundedCompactSupport f) (hg : BoundedCompactSupport g) (j : ℕ) :    ∫ x, conj (g x) * carlesonRowSum t j f x = ∫ x, conj (adjointCarlesonRowSum t j g x) * f x := by  classical calc    _ = ∫ x, ∑ u with u ∈ rowDecomp t j, conj (g x) * carlesonSum (t u) f x := by      unfold carlesonRowSum; simp_rw [Finset.mul_sum]    _ = ∑ u with u ∈ rowDecomp t j, ∫ x, conj (g x) * carlesonSum (t u) f x := by      apply integral_finsetSum; intro p _      exact hg.conj.mul hf.carlesonSum |>.integrable    _ = ∑ u with u ∈ rowDecomp t j, ∫ y, conj (adjointCarlesonSum (t u) g y) * f y := by      simp_rw [adjointCarlesonSum_adjoint hf hg]    _ = ∫ y, ∑ u with u ∈ rowDecomp t j, conj (adjointCarlesonSum (t u) g y) * f y := by      symm; apply integral_finsetSum; intro p _      refine BoundedCompactSupport.mul ?_ hf |>.integrable      exact hg.adjointCarlesonSum.conj    _ = _ := by congr!; rw [← Finset.sum_mul, ← map_sum]; rfl