MeasureTheory.AEStronglyMeasurable.adjointCarleson

@[fun_prop]lemma AEStronglyMeasurable.adjointCarleson (hf : AEStronglyMeasurable f) :    AEStronglyMeasurable (adjointCarleson p f) := by  refine .integral_prod_right'    (f := fun z ↦ conj (Ks (𝔰 p) z.2 z.1) * exp (Complex.I * (Q z.2 z.2 - Q z.2 z.1)) * f z.2) ?_  refine .mono_ac (.prod .rfl restrict_absolutelyContinuous) ?_  refine .mul (.mul ?_ ?_) hf.comp_snd  · exact Complex.continuous_conj.comp_aestronglyMeasurable aestronglyMeasurable_Ks.prod_swap  · refine Complex.continuous_exp.comp_aestronglyMeasurable (.const_mul (.sub ?_ ?_) _)    · exact Measurable.aestronglyMeasurable (by fun_prop)    · exact continuous_ofReal.comp_aestronglyMeasurable aestronglyMeasurable_Q₂.prod_swap