carlesonOperatorIntegrand_measurable

@[fun_prop]theorem carlesonOperatorIntegrand_measurable {θ : Θ X} (mf : AEStronglyMeasurable f) :    Measurable (carlesonOperatorIntegrand K θ R₁ R₂ f) := by  unfold carlesonOperatorIntegrand  revert f  apply AEStronglyMeasurable.induction  · intro f g stronglyMeasurable_f hfg hf    have {x : X} : ∫ (y : X) in Annulus.oo x R₁ R₂, K x y * f y * cexp (I * ↑(θ y))                 = ∫ (y : X) in Annulus.oo x R₁ R₂, K x y * g y * cexp (I * ↑(θ y)) := by      apply integral_congr_ae      apply ae_restrict_le      simp only [mul_eq_mul_right_iff, mul_eq_mul_left_iff, exp_ne_zero, or_false]      filter_upwards [hfg] with x hx using Or.inl hx    simp_rw [← this]    exact hf  intro f mf  rw [← stronglyMeasurable_iff_measurable]  conv => congr; ext x; rw [← integral_indicator Annulus.measurableSet_oo]  apply StronglyMeasurable.integral_prod_right  rw [stronglyMeasurable_iff_measurable]  have hK : Measurable (fun (x, y) ↦ K x y) := measurable_K  exact Measurable.indicator (by fun_prop) (measurable_dist measurableSet_Ioo)