iSup_lcoConvergent

lemma iSup_lcoConvergent : ⨆ n, lcoConvergent K Q f n = linearizedCarlesonOperator Q K f := by  ext x; rw [iSup_apply]; unfold lcoConvergent linearizedCarlesonOperator  apply le_antisymm  · refine iSup_le fun n ↦ iSup₂_le fun R₁ mR₁ ↦ iSup₂_le fun R₂ mR₂ ↦ ?_    rw [T_R, enorm_indicator_eq_indicator_enorm]    conv_rhs => enter [1, R₁]; rw [iSup_comm]    have b₁ : 0 < R₁ := lt_trans (by positivity) mR₁.1    have b₂ := mR₂.1    calc      _ ≤ _ := indicator_enorm_le_enorm_self _ x      _ ≤ ⨆ R₂, ⨆ (_ : R₁ < R₂), ‖carlesonOperatorIntegrand K (Q x) R₁ R₂ f x‖ₑ := by        apply le_iSup₂ R₂ b₂      _ ≤ _ := by apply le_iSup₂ R₁ b₁  · refine iSup₂_le fun R₁ R₂ ↦ iSup₂_le fun lR₁ lR₂ ↦ ?_    suffices ∃ n, (2 ^ n)⁻¹ < R₁ ∧ R₂ < 2 ^ n ∧ dist x (cancelPt X) < 2 ^ n by      obtain ⟨n, hn₁, hn₂, hn₃⟩ := this      have b₁ : R₁ ∈ Ioo (2 ^ n)⁻¹ (2 ^ n) := ⟨hn₁, lR₂.trans hn₂⟩      have b₂ : R₂ ∈ Ioo R₁ (2 ^ n) := ⟨lR₂, hn₂⟩      calc        _ = ‖T_R K Q R₁ R₂ (2 ^ n) f x‖ₑ := by          rw [T_R, enorm_indicator_eq_indicator_enorm, indicator_of_mem (Metric.mem_ball.mpr hn₃)]        _ ≤ ⨆ R₂ ∈ Ioo R₁ (2 ^ n), ‖T_R K Q R₁ R₂ (2 ^ n) f x‖ₑ := by apply le_iSup₂ _ b₂        _ ≤ ⨆ R₁ ∈ Ioo (2 ^ n)⁻¹ (2 ^ n), ⨆ R₂ ∈ Ioo R₁ (2 ^ n), ‖T_R K Q R₁ R₂ (2 ^ n) f x‖ₑ := by          apply le_iSup₂ _ b₁        _ ≤ _ := by apply le_iSup _ n    obtain ⟨n₁, hn₁⟩ := pow_unbounded_of_one_lt R₁⁻¹ one_lt_two    replace hn₁ := inv_lt_of_inv_lt₀ lR₁ hn₁    obtain ⟨n₂, hn₂⟩ := pow_unbounded_of_one_lt (max R₂ (dist x (cancelPt X))) one_lt_two    refine ⟨max n₁ n₂, ?_, ?_, ?_⟩    · refine lt_of_le_of_lt ?_ hn₁      exact inv_anti₀ (by positivity) (pow_le_pow_right₀ one_le_two (le_max_left ..))    · exact ((le_max_left ..).trans_lt hn₂).trans_le        (pow_le_pow_right₀ one_le_two (le_max_right ..))    · exact ((le_max_right ..).trans_lt hn₂).trans_le        (pow_le_pow_right₀ one_le_two (le_max_right ..))