adjointCarleson_adjoint

lemma adjointCarleson_adjoint    (hf : BoundedCompactSupport f) (hg : BoundedCompactSupport g) (p : 𝔓 X) :    ∫ x, conj (g x) * carlesonOn p f x = ∫ y, conj (adjointCarleson p g y) * f y := by  let H := fun x ↦ fun y ↦ conj (g x) * (E p).indicator 1 x * MKD (𝔰 p) x y * f y  have hH : Integrable (uncurry H) := by    let H₀ := fun x y ↦ ‖g x‖ * ‖f y‖    obtain ⟨M₀, hM₀nn, hM₀⟩ := hg.hasCompactSupport.isBounded.exists_bound_of_norm_Ks (𝔰 p)    have hHleH₀ x y : ‖H x y‖ ≤ M₀ * ‖g x‖ * ‖f y‖ := by      by_cases h : x ∈ tsupport g      · unfold H        rw [norm_mul, norm_mul, norm_mul, norm_conj]        nth_rw 2 [mul_assoc, mul_comm]        gcongr        apply mul_le_mul (norm_indicator_one_le ..) norm_MKD_le_norm_Ks (by simp) (by simp) |>.trans        linarith [hM₀ x y h]      · suffices hz : H x y = 0 by rw [hz]; simp only [norm_zero, ge_iff_le]; positivity        unfold H; simp [image_eq_zero_of_notMem_tsupport h]    have : Integrable (fun z : X × X ↦ M₀ * ‖g z.1‖ * ‖f z.2‖) :=      (hg.norm.const_mul _).integrable.mul_prod hf.norm.integrable    apply this.mono    · refine .mul ?_ hf.aestronglyMeasurable.comp_snd      refine .mul ?_ ?_      · refine .mul ?_ ?_        · exact RCLike.continuous_conj.comp_aestronglyMeasurable hg.aestronglyMeasurable.comp_fst        · exact aestronglyMeasurable_const.indicator measurableSet_E |>.comp_fst      · unfold MKD        fun_prop    · apply ae_of_all      exact fun z ↦ (hHleH₀ z.1 z.2).trans <| Real.le_norm_self _  calc    _ = ∫ x, conj (g x) * ∫ y, (E p).indicator 1 x * MKD (𝔰 p) x y * f y := by      congr 1; ext x; congr 1      rw [carlesonOn, indicator_eq_indicator_one_mul, ← smul_eq_mul, ← integral_smul]      congr 1; ext y; unfold MKD; simp [smul_eq_mul]; ring    _ = ∫ x, ∫ y, H x y := by      unfold H; congr 1; ext x      calc conj (g x) * ∫ y, (E p).indicator 1 x * MKD (𝔰 p) x y * f y          = ∫ y, conj (g x) * ((E p).indicator 1 x * MKD (𝔰 p) x y * f y) :=            (integral_const_mul _ _).symm        _ = ∫ y, conj (g x) * (E p).indicator 1 x * MKD (𝔰 p) x y * f y := by            congr 1; ext y; ring    _ = ∫ y, ∫ x, H x y := integral_integral_swap hH    _ = ∫ y, (∫ x, conj (g x) * (E p).indicator 1 x * MKD (𝔰 p) x y) * f y := by      simp_rw [H]; congr 1; ext y      exact integral_mul_const _ _    _ = ∫ y, conj (∫ x, g x * (E p).indicator 1 x * conj (MKD (𝔰 p) x y)) * f y := by      congr 1; ext y; congr 1      have h : ∀ x, conj (g x) * (E p).indicator 1 x * MKD (𝔰 p) x y =          conj (g x * (E p).indicator 1 x * conj (MKD (𝔰 p) x y)) :=        fun x => by rw [map_mul, conj_conj, map_mul, conj_indicator, map_one]      simp_rw [h]      exact integral_conj    _ = _ := by      congr! with y      simp_rw [mul_comm (g _) _]      calc        _ = ∫ x, (E p).indicator (fun x ↦ g x * conj (MKD (𝔰 p) x y)) x := by          congr with x; simp only [indicator]; split_ifs <;> simp        _ = ∫ x in E p, g x * conj (MKD (𝔰 p) x y) := integral_indicator measurableSet_E        _ = ∫ x in E p, conj (MKD (𝔰 p) x y) * g x := by congr; funext; rw [mul_comm]        _ = _ := by          unfold adjointCarleson MKD          congr; funext; rw [map_mul, ← exp_conj, mul_comm (cexp _)]          congr; simp; ring