finitary_carleson_step

theorem finitary_carleson_step    (CP : CP304 q q' F f σ₁ σ₂) (bG : IsBounded G) (mG : MeasurableSet G) :    ∃ G' ⊆ G, IsBounded G' ∧ MeasurableSet G' ∧ 2 * volume G' ≤ volume G ∧    ∫⁻ x in G \ G', ‖T_lin CP.Q σ₁ σ₂ f x‖ₑ ≤    C2_0_1 a q * (volume G) ^ (q' : ℝ)⁻¹ * (volume F) ^ (q : ℝ)⁻¹ := by  obtain ⟨Q, BST_T_Q, hq, hqq', bF, mF, mf, nf, mσ₁, mσ₂, rσ₁, rσ₂, lσ⟩ := CP  let PD : ProofData a q K σ₁ σ₂ F G :=    ⟨‹_›, hq, bF, bG, mF, mG, mσ₁, mσ₂, rσ₁, rσ₂, lσ, Q, BST_T_Q⟩  obtain ⟨G₁, mG₁, vG₁, hG₁⟩ := finitary_carleson X  refine ⟨G ∩ G₁, inter_subset_left, bG.subset inter_subset_left, mG.inter mG₁, ?_, ?_⟩  · refine le_trans ?_ vG₁; gcongr; exact inter_subset_right  · simp_rw [sdiff_self_inter]; simp_rw [toFinset_Icc, show nnq = q by rfl] at hG₁    convert! hG₁ f mf nf using 4; rw [eq_sub_iff_add_eq]; norm_cast    exact hqq'.symm.inv_add_inv_eq_one