MeasureTheory.StronglyMeasurable.adjointCarleson

@[fun_prop]lemma StronglyMeasurable.adjointCarleson (hf : StronglyMeasurable f) :    StronglyMeasurable (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 .mul (.mul ?_ ?_) (by fun_prop)  · exact Complex.continuous_conj.comp_stronglyMeasurable (stronglyMeasurable_Ks.prod_swap)  · refine Complex.continuous_exp.comp_stronglyMeasurable (.const_mul (.sub ?_ ?_) _)    · exact Measurable.stronglyMeasurable (by fun_prop)    · exact continuous_ofReal.comp_stronglyMeasurable stronglyMeasurable_Q₂.prod_swap