linearizedCarlesonOperator_measurable

@[fun_prop]theorem linearizedCarlesonOperator_measurable {θ : Θ X} (hf : LocallyIntegrable f) :    Measurable (linearizedCarlesonOperator (fun _ ↦ θ) K f) := by  unfold linearizedCarlesonOperator  have {x : X} :      ⨆ R₁, ⨆ R₂, ⨆ (_ : 0 < R₁), ⨆ (_ : R₁ < R₂), ‖carlesonOperatorIntegrand K ((fun x ↦ θ) x) R₁ R₂ f x‖ₑ      = ⨆ (R₁ : ℚ), ⨆ (R₂ : ℚ), ⨆ (_ : 0 < R₁), ⨆ (_ : R₁ < R₂), ‖carlesonOperatorIntegrand K ((fun x ↦ θ) x) R₁ R₂ f x‖ₑ := by    apply le_antisymm    · apply le_of_forall_lt_imp_le_of_dense      intro c  hc      rw [lt_iSup_iff] at hc      rcases hc with ⟨R₁, h⟩      rw [lt_iSup_iff] at h      rcases h with ⟨R₂, h⟩      rw [lt_iSup_iff] at h      rcases h with ⟨R₁_pos, h⟩      rw [lt_iSup_iff] at h      rcases h with ⟨R₁_lt_R₂, h⟩      set ε := ‖carlesonOperatorIntegrand K ((fun x ↦ θ) x) R₁ R₂ f x‖ - c.toReal      have ε_pos : 0 < ε := by        unfold ε        apply sub_pos_of_lt        apply toReal_lt_of_lt_ofReal        rwa [ofReal_norm]      have mf : IntegrableOn f (Annulus.oo x R₁ R₂) volume := by        apply IntegrableOn.mono_set _ (Annulus.oo_subset_ball)        apply IntegrableOn.mono_set _ (ball_subset_closedBall)        apply hf.integrableOn_isCompact (isCompact_closedBall _ _)      have exist_rats := exists_rat_near_carlesonOperatorIntegrand' θ x mf R₁_pos R₁_lt_R₂ ε_pos      rcases exist_rats with ⟨q₁, q₂, R₁_lt_q₁, q₁_lt_q₂, q₂_lt_R₂, h_dist⟩      have q₁_pos : (0 : ℝ) < q₁ := R₁_pos.trans R₁_lt_q₁      simp only [Rat.cast_pos] at q₁_pos      apply le_iSup₂_of_le q₁ q₂      apply le_iSup₂_of_le q₁_pos q₁_lt_q₂      rw [dist_eq_norm] at h_dist      have c_ne_top := h.ne_top      rw [← ofReal_norm, lt_ofReal_iff_toReal_lt c_ne_top] at h      have : c.toReal = ‖carlesonOperatorIntegrand K ((fun x ↦ θ) x) R₁ R₂ f x‖ - ε := by simp [ε]      rw [← ofReal_norm, le_ofReal_iff_toReal_le c_ne_top (by simp), this]      have : ‖carlesonOperatorIntegrand K ((fun x ↦ θ) x) R₁ R₂ f x‖              ≤ ε + ‖carlesonOperatorIntegrand K ((fun x ↦ θ) x) q₁ q₂ f x‖ := by        simp only        apply le_trans _ (add_le_add_left h_dist.le _)        rw [add_comm]        apply norm_le_norm_add_norm_sub      apply le_trans (sub_le_sub_right this _)      simp    · apply iSup_le      intro q₁      apply iSup_le      intro q₂      apply iSup_le      intro q₁_pos      apply iSup_le      intro q₁_lt_q₂      apply le_iSup₂_of_le (Rat.cast q₁) (Rat.cast q₂)      apply le_iSup₂_of_le (by simpa) (by simpa)      rfl  simp_rw [this]  have := hf.aestronglyMeasurable  fun_prop