carlesonOperator_eq_biSup_Θ'_J102

lemma carlesonOperator_eq_biSup_Θ'_J102 {x : X} (mf : Measurable f) (nf : (‖f ·‖) ≤ 1) :    carlesonOperator K f x =    ⨆ θ ∈ Θ' X, ⨆ j ∈ J102, ‖carlesonOperatorIntegrand K θ j.1 j.2 f x‖ₑ := by  unfold carlesonOperator linearizedCarlesonOperator; apply le_antisymm  · refine iSup_le fun θ ↦ iSup₂_le fun R₁ R₂ ↦ iSup₂_le fun hR₁ hR₂ ↦ ?_    refine ENNReal.le_of_forall_pos_le_add fun ε εpos ltt ↦ ?_    rw [← NNReal.coe_pos] at εpos    -- Shift `θ` to an element of `Θ'` with error less than `ε / 2`    have tcon := @continuous_carlesonOperatorIntegrand _ _ _ _ _ R₁ R₂ _ x mf nf hR₁    rw [continuous_iff] at tcon; specialize tcon θ _ (half_pos εpos)    obtain ⟨δ₀, δ₀pos, dθ⟩ := tcon    have dΘ' := dense_Θ' (X := X)    rw [dense_iff] at dΘ'; specialize dΘ' θ _ δ₀pos; obtain ⟨θ', mθ'₁, mθ'₂⟩ := dΘ'    rw [mem_ball] at mθ'₁; specialize dθ _ mθ'₁    -- Shift `R₁, R₂` to rationals with error less than `ε / 2`    obtain ⟨q₁, q₂, lq₁, lq, -, dq⟩ :=      exists_rat_near_carlesonOperatorIntegrand θ' x mf nf hR₁ hR₂ (half_pos εpos)    -- Combine `dq` and `dθ`    have final_bound := (dist_triangle ..).trans_lt (add_lt_add dq dθ)    rw [add_halves] at final_bound    calc      _ = ‖carlesonOperatorIntegrand K θ' q₁ q₂ f x +          (carlesonOperatorIntegrand K θ R₁ R₂ f x -          carlesonOperatorIntegrand K θ' q₁ q₂ f x)‖ₑ := by rw [add_sub_cancel]      _ ≤ ‖carlesonOperatorIntegrand K θ' q₁ q₂ f x‖ₑ +          edist (carlesonOperatorIntegrand K θ' q₁ q₂ f x)          (carlesonOperatorIntegrand K θ R₁ R₂ f x) := by          rw [edist_comm, edist_eq_enorm_sub]          exact enorm_add_le _ _      _ ≤ _ := by        gcongr        · calc            _ ≤ ⨆ j ∈ J102, ‖carlesonOperatorIntegrand K θ' j.1 j.2 f x‖ₑ := by              have : (q₁, q₂) ∈ J102 := ⟨Rat.cast_pos.mp (hR₁.trans lq₁), lq⟩              convert! le_iSup₂ _ this; rfl            _ ≤ _ := by apply le_iSup₂ _ mθ'₂        · rw [edist_dist, coe_nnreal_eq]; exact ofReal_le_ofReal final_bound.le  · refine iSup₂_le fun θ mθ ↦ iSup₂_le fun ⟨q₁, q₂⟩ ⟨hq₁, hq₂⟩ ↦ ?_    conv_rhs => enter [1, θ, 1, R₁]; rw [iSup_comm]    simp_rw [← Rat.cast_lt (K := ℝ), Rat.cast_zero] at hq₁ hq₂    calc      _ ≤ ⨆ (R₂ : ℝ), ⨆ (_ : q₁ < R₂),          ‖carlesonOperatorIntegrand K θ q₁ R₂ f x‖ₑ := by convert! le_iSup₂ _ hq₂; rfl      _ ≤ ⨆ (R₁ : ℝ), ⨆ (_ : 0 < R₁), ⨆ R₂, ⨆ (_ : R₁ < R₂),          ‖carlesonOperatorIntegrand K θ R₁ R₂ f x‖ₑ := by convert! le_iSup₂ _ hq₁; rfl      _ ≤ _ := le_iSup_iff.mpr fun _ a ↦ a θ