carlesonOperatorReal_measurable

lemma carlesonOperatorReal_measurable {f : ℝ → ℂ} (meas_f : AEStronglyMeasurable f)  (hf : ∀ x, IntegrableOn f (Set.Ioo x (x + 2))) :    Measurable (T f) := by  wlog f_measurable : Measurable f  · rcases meas_f with ⟨g, hg, hfg⟩    convert this (f := g) hg.aestronglyMeasurable _ hg.measurable using 1    · unfold carlesonOperatorReal      congr with x      congr with n      congr with r      congr with _      congr with _      congr 1      apply integral_congr_ae      apply Filter.EventuallyEq.restrict      filter_upwards [hfg]      intro y hy      congr    intro x    exact (integrableOn_congr_fun_ae hfg.restrict).mp (hf x)  apply Measurable.iSup  intro n  set F : ℝ → ℝ → ℝ → ℂ :=    fun x r y ↦      {y | dist x y ∈ Set.Ioo r 1}.indicator (fun t ↦ f t * K x t * (Complex.I * ↑n * ↑t).exp) y    with Fdef  set G : ℝ → ℝ → ENNReal := fun x r ↦ ‖∫ (y : ℝ), F x r y‖ₑ with Gdef  have hFG : (fun x ↦ ⨆ r, ⨆ (_ : 0 < r), ⨆ (_ : r < 1), ‖∫ (y : ℝ) in                {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖ₑ)             = fun x ↦ ⨆ (r : ℝ) (_ : r ∈ Set.Ioo 0 1), G x r := by    ext    congr with r    simp_rw [iSup_and', ← Set.mem_Ioo, Gdef, Fdef]    congr    rw [← integral_indicator annulus_measurableSet]  rw [hFG]  have hGr : (⨆ (r ∈ Set.Ioo 0 1), G · r) = (⨆ (r ∈ (Set.Ioo 0 1) ∩ Qᵣ), G · r) := by    ext x    rw [sup_eq_sup_dense_of_continuous Qᵣ isOpen_Ioo Qᵣ_dense]    refine fun r ⟨hr, _⟩ ↦      (((EReal.continuous_coe_ennreal_iff.mp (EReal.continuous_coe_iff.mpr          (continuous_iff_le_induced.mpr fun _ ↦ id))).continuousAt).comp (ContinuousAt.nnnorm ?_)        ).continuousWithinAt    set S := Set.Ioo (r / 2) (2 * r) with Sdef    set bound := fun y ↦ ‖F x (r / 2) y‖ with bound_def    have h_bound : ∀ᶠ (s : ℝ) in nhds r, ∀ᵐ (a : ℝ), ‖F x s a‖ ≤ bound a := by      rw [eventually_nhds_iff]      use S      constructor      · intro s ⟨_, _⟩        apply Filter.Eventually.of_forall        intro y        rw [bound_def, Fdef, norm_indicator_eq_indicator_norm]        simp only        rw [norm_indicator_eq_indicator_norm]        apply Set.indicator_le_indicator_of_subset        · intro y ⟨_, _⟩          constructor <;> linarith        · intro y          apply norm_nonneg      constructor      · apply isOpen_Ioo      · rw [Sdef]        constructor <;> linarith    apply continuousAt_of_dominated _  h_bound    · rw [bound_def, Fdef]      conv => pattern ‖_‖; rw [norm_indicator_eq_indicator_norm]      rw [integrable_indicator_iff annulus_measurableSet]      have bound_on_set : ∀ᵐ a ∂(volume.restrict {y | dist x y ∈ Set.Ioo (r / 2) 1}),          ‖K x a * (Complex.I * (↑n * ↑a)).exp‖ ≤ ‖2 ^ (2 : ℝ) / (2 * (r / 2))‖ := by        rw [ae_restrict_iff' annulus_measurableSet]        filter_upwards with a ha        rw [norm_mul, mul_comm Complex.I]        norm_cast        rw [Complex.norm_exp_ofReal_mul_I, mul_one]        rw [Real.norm_eq_abs, abs_of_nonneg (by apply div_nonneg (by norm_num); linarith)]        calc _          _ ≤ 2 ^ (2 : ℝ) / (2 * |x - a|) := Hilbert_kernel_bound          _ ≤ 4 / (2 * (r / 2)) := by            gcongr            · linarith            · rw [← Real.dist_eq]              exact ha.1.le      simp_rw [Complex.norm_mul] at bound_on_set      simp_rw [Complex.norm_mul, mul_assoc]      unfold IntegrableOn      apply Integrable.mul_bdd _ (by fun_prop) (by simpa only [norm_mul, norm_norm])      apply Integrable.norm      rw [annulus_real_eq (by linarith [hr]), ← IntegrableOn]      apply IntegrableOn.mono_set (hf (x - 1))      intro y      grind    · have contOn1 : ∀ (y : ℝ), ContinuousOn (F x · y) (Set.Iio (dist x y)) := by        intro y        rw [continuousOn_iff_continuous_restrict]        apply continuous_of_const        simp only [Set.restrict_apply, Subtype.forall]        intro s hs t ht        rw [Fdef]        simp only [Set.mem_Ioo]        by_cases! h : dist x y < 1        · rw [Set.indicator_apply, ite_cond_eq_true, Set.indicator_apply, ite_cond_eq_true]          · simpa using ⟨ht, h⟩          · simpa using ⟨hs, h⟩        · rw [Set.indicator_apply, ite_cond_eq_false, Set.indicator_apply, ite_cond_eq_false]          all_goals simpa using fun _ ↦ h      have contOn2 : ∀ (y : ℝ), ContinuousOn (fun s ↦ F x s y) (Set.Ioi (min (dist x y) 1)) := by        intro y        rw [continuousOn_iff_continuous_restrict]        apply continuous_of_const        simp only [Set.restrict_apply, Subtype.forall]        intro s hs t ht        rw [Fdef]        simp only [Set.mem_Ioo]        rw [Set.indicator_apply, ite_cond_eq_false, Set.indicator_apply, ite_cond_eq_false]        · rw [Set.mem_Ioi, min_lt_iff] at ht          simp only [Set.mem_setOf_eq, eq_iff_iff, iff_false, not_and, not_lt]          intro h          rcases ht with h' | h'          · exfalso            exact (lt_self_iff_false _).mp (h'.trans h)          · exact (h'.trans h).le        · rw [Set.mem_Ioi, min_lt_iff] at hs          simp only [Set.mem_setOf_eq, eq_iff_iff, iff_false, not_and, not_lt]          intro h          rcases hs with h' | h'          · exfalso            exact (lt_self_iff_false _).mp (h'.trans h)          · exact (h'.trans h).le      have contOn : ∀ y, ∀ t ≠ dist x y, ContinuousAt (F x · y) t := by        intro y t ht        by_cases! h : t < dist x y        · exact_mod_cast (contOn1 y).continuousAt (Iio_mem_nhds h)        · exact ContinuousOn.continuousAt (contOn2 y) (Ioi_mem_nhds            ((min_le_left _ _).trans_lt (lt_of_le_of_ne h ht.symm)))      have subset_finite :          {y | ¬ContinuousAt (F x · y) r} ⊆ ({x - r, x + r} : Finset ℝ) := by        intro y hy        have hxy : dist x y = r := by          contrapose! hy          rw [Set.mem_setOf_eq, not_not]          exact contOn y r hy.symm        rw [Real.dist_eq, abs_eq hr.le] at hxy        simp only [Finset.coe_insert, Finset.coe_singleton, Set.mem_insert_iff,          Set.mem_singleton_iff]        cases hxy        · left; linarith        · right; linarith      rw [ae_iff]      exact measure_mono_null subset_finite (Finset.measure_zero _ _)    · filter_upwards with r      apply AEStronglyMeasurable.indicator _ annulus_measurableSet      apply AEStronglyMeasurable.mul      · apply AEStronglyMeasurable.mul meas_f (by fun_prop)      · fun_prop  rw [hGr]  refine Measurable.biSup _ (Set.Countable.mono Set.inter_subset_right Qᵣ_countable) (fun r _ ↦ ?_)  apply measurable_coe_nnreal_ennreal.comp (measurable_nnnorm.comp _)  rw [← stronglyMeasurable_iff_measurable]  apply StronglyMeasurable.integral_prod_right  rw [stronglyMeasurable_iff_measurable, Fdef]  exact (measurable_mul_kernel f_measurable).indicator (measurable_dist measurableSet_Ioo)