Measurable lco Convergent

lemma measurable_lcoConvergent {n : ℕ} (mf : Measurable f) (nf : (‖f ·‖) ≤ 1) :    Measurable (lcoConvergent K Q f n) := by  refine measurable_of_Ioi fun c ↦ ?_  let J : Set (ℚ × ℚ) := {p | (2 ^ n)⁻¹ < p.1 ∧ p.1 < p.2 ∧ p.2 < 2 ^ n}  suffices lcoConvergent K Q f n ⁻¹' Ioi c = ⋃ j ∈ J, {x | c < ‖T_R K Q j.1 j.2 (2 ^ n) f x‖ₑ} by    rw [this]; refine MeasurableSet.biUnion J.to_countable fun j mj ↦ ?_    exact measurableSet_lt measurable_const      ((measurable_carlesonOperatorIntegrand mf).indicator measurableSet_ball).enorm  ext x  simp_rw [mem_preimage, mem_Ioi, lcoConvergent, lt_biSup_iff, mem_iUnion₂, mem_setOf_eq,    exists_prop]  constructor <;> intro h  · obtain ⟨R₁, mR₁, R₂, mR₂, hR⟩ := h; unfold T_R at hR ⊢    by_cases mx : x ∈ Metric.ball (cancelPt X) (2 ^ n); swap    · simp [indicator_of_notMem mx] at hR    simp_rw [indicator_of_mem mx] at hR ⊢    lift c to ℝ≥0 using hR.ne_top    simp_rw [coe_lt_enorm, ← NNReal.coe_lt_coe, coe_nnnorm] at hR ⊢    let ε := ‖carlesonOperatorIntegrand K (Q x) R₁ R₂ f x‖ - c    have εpos : 0 < ε := by linarith only [hR]    have hR₁ : 0 < R₁ := lt_of_le_of_lt (by positivity) mR₁.1    have hR₂ : R₁ < R₂ := mR₂.1    obtain ⟨q₁, q₂, lq₁, lq, lq₂, dq⟩ :=      exists_rat_near_carlesonOperatorIntegrand (Q x) x mf nf hR₁ hR₂ εpos    have qmJ : (q₁, q₂) ∈ J := by      refine ⟨?_, Rat.cast_lt.mp lq, ?_⟩      · simp_rw [← Rat.cast_lt (K := ℝ), Rat.cast_inv, Rat.cast_pow, Rat.cast_ofNat]        exact mR₁.1.trans lq₁      · simp_rw [← Rat.cast_lt (K := ℝ), Rat.cast_pow, Rat.cast_ofNat]        exact lq₂.trans mR₂.2    use (q₁, q₂), qmJ    simp_rw [ε, lt_sub_comm, dist_eq_norm'] at dq; apply dq.trans_le    rw [sub_le_comm]; exact norm_sub_norm_le ..  · obtain ⟨⟨R₁, R₂⟩, ⟨bR₁, bR₂, bR₃⟩, hR⟩ := h; dsimp only at hR    simp_rw [← Rat.cast_lt (K := ℝ), Rat.cast_inv, Rat.cast_pow, Rat.cast_ofNat] at bR₁ bR₂ bR₃    use R₁, ⟨bR₁, bR₂.trans bR₃⟩, R₂, ⟨bR₂, bR₃⟩