metric_carleson

theorem metric_carleson [IsCancellative X (defaultτ a)]    (hq : q ∈ Ioc 1 2) (hqq' : q.HolderConjugate q') (mF : MeasurableSet F) (mG : MeasurableSet G)    (mf : Measurable f) (nf : (‖f ·‖) ≤ F.indicator 1)    (hT : HasBoundedStrongType (nontangentialOperator K · ·) 2 2 volume volume (C_Ts a)) :    ∫⁻ x in G, carlesonOperator K f x ≤    C1_0_2 a q * volume G ^ (q' : ℝ)⁻¹ * volume F ^ (q : ℝ)⁻¹ := by  have nf' : (‖f ·‖) ≤ 1 := nf.trans (indicator_le_self' (by simp))  calc    _ = ∫⁻ x in G, ⨆ θ ∈ Θ' X, ⨆ j ∈ J102, ‖carlesonOperatorIntegrand K θ j.1 j.2 f x‖ₑ := by      congr with x; exact carlesonOperator_eq_biSup_Θ'_J102 mf nf'    _ ≤ _ := ?_  rcases (Θ' X).eq_empty_or_nonempty with eΘ' | nΘ'  · simp_rw [eΘ', iSup_emptyset, bot_eq_zero, lintegral_zero]; exact zero_le  let g (θ : Θ X) (x : X) := ⨆ j ∈ J102, ‖carlesonOperatorIntegrand K θ j.1 j.2 f x‖ₑ  have mg (θ : Θ X) : Measurable (g θ) :=    Measurable.biSup _ J102.to_countable fun j mj ↦      (measurable_carlesonOperatorIntegrand (Q := SimpleFunc.const X θ) mf).enorm  calc    _ = ∫⁻ x in G, ⨆ n, ⨆ i ∈ Finset.range (n + 1), g (enumΘ' nΘ' i) x := by      congr with x; exact biSup_Θ'_eq_biSup_enumΘ' nΘ' g    _ = ⨆ n, ∫⁻ x in G, ⨆ i ∈ Finset.range (n + 1), g (enumΘ' nΘ' i) x := by      refine lintegral_iSup (fun n ↦ ?_) (fun i j hl ↦ ?_)      · refine Measurable.iSup fun i ↦ Measurable.iSup fun mi ↦ ?_        refine Measurable.iSup fun j ↦ Measurable.iSup fun mj ↦ Measurable.enorm ?_        exact measurable_carlesonOperatorIntegrand (Q := SimpleFunc.const X (enumΘ' nΘ' i)) mf      · intro x; apply biSup_mono; simp_rw [Finset.mem_range]; lia    _ ≤ ⨆ n, ∫⁻ x in G, g (QΘ' nΘ' mg n x) x := by      gcongr with n x; exact biSup_enumΘ'_le_QΘ' nΘ' mg    _ ≤ ⨆ n, ∫⁻ x in G, linearizedCarlesonOperator (QΘ' nΘ' mg n) K f x := by      gcongr with n x; set Q := QΘ' nΘ' mg n; unfold linearizedCarlesonOperator      refine iSup₂_le fun ⟨q₁, q₂⟩ ⟨hq₁, hq₂⟩ ↦ ?_      conv_rhs => enter [1, R₁]; rw [iSup_comm]      simp_rw [← Rat.cast_lt (K := ℝ), Rat.cast_zero] at hq₁ hq₂      calc        _ ≤ ⨆ (R₂ : ℝ), ⨆ (_ : q₁ < R₂),            ‖carlesonOperatorIntegrand K (Q x) q₁ R₂ f x‖ₑ := by convert! le_iSup₂ _ hq₂; rfl        _ ≤ _ := by convert! le_iSup₂ _ hq₁; rfl    _ ≤ _ := iSup_le fun n ↦ linearized_metric_carleson hq hqq' mF mG mf nf (BST_LNT_of_BST_NT hT)