S truncation

lemma S_truncation    [IsCancellative X (defaultτ a)] {B : ℕ} (hq : q ∈ Ioc 1 2) (hqq' : q.HolderConjugate q')    (bF : IsBounded F) (bG : IsBounded G) (mF : MeasurableSet F) (mG : MeasurableSet G)    (mf : Measurable f) (nf : (‖f ·‖) ≤ F.indicator 1)    (BST_T_Q : ∀ θ : Θ X, HasBoundedStrongType (linearizedNontangentialOperator Q θ K · ·)      2 2 volume volume (C_Ts a)) :    ∫⁻ x in G, ⨆ s₁ ∈ Finset.Icc (-B : ℤ) B, ⨆ s₂ ∈ Finset.Icc s₁ B, ‖T_S Q s₁ s₂ f x‖ₑ ≤    C3_0_4 a q * volume G ^ (q' : ℝ)⁻¹ * volume F ^ (q : ℝ)⁻¹ := by  -- Define `T1'` and `T1` and prove their measurability  let T1' (x : X) (s' : ℤ) := ⨆ s₂ ∈ Finset.Icc s' B, ‖T_S Q s' s₂ f x‖ₑ  have mT1' {n : ℤ} : Measurable (T1' · n) :=    Measurable.iSup fun _ ↦ Measurable.iSup fun _ ↦ (measurable_T_S mf).enorm  let T1 (x : X) := ⨆ s₁ ∈ Finset.Icc (-B : ℤ) B, T1' x s₁  have mT1 : Measurable T1 := Measurable.iSup fun _ ↦ Measurable.iSup fun _ ↦ mT1'  -- For each `x` define a candidate set of values for `σ₁ x`;  -- the final value is the minimum in this set. Also prove measurability of membership  let candσ₁ (x : X) := (Finset.Icc (-B : ℤ) B).filter (T1 x = T1' x ·)  have necσ₁ (x : X) : (candσ₁ x).Nonempty := by    rw [Finset.filter_nonempty_iff]    obtain ⟨s', ms', hs'⟩ := (Finset.Icc (-B : ℤ) B).exists_max_image (T1' x) ⟨0, by simp⟩    use s', ms'; apply le_antisymm    · exact iSup₂_le hs'    · apply le_biSup _ ms'  have scσ₁ (x : X) : candσ₁ x ⊆ Finset.Icc (-B) B := by simp [candσ₁]  have mcσ₁ {n : ℤ} : Measurable (n ∈ candσ₁ ·) := by    simp_rw [candσ₁, Finset.mem_filter, Finset.mem_Icc]    apply measurable_const.and; rw [← measurableSet_setOf]; exact measurableSet_eq_fun mT1 mT1'  -- Define `σ₁` and prove its measurability and finite range  let σ₁ (x : X) := (candσ₁ x).min' (necσ₁ x)  have eσ₁ (x : X) : σ₁ x ∈ candσ₁ x := (candσ₁ x).min'_mem (necσ₁ x)  have minσ₁ (x : X) {n : ℤ} (hn : n ∈ candσ₁ x) : σ₁ x ≤ n := (candσ₁ x).min'_le _ hn  have mσ₁ : Measurable σ₁ := by    classical    refine measurable_to_countable' fun n ↦ ?_    have eqv : σ₁ ⁻¹' {n} =        candσ₁ ⁻¹' ((Finset.Icc (-B : ℤ) B).powerset.filter fun c ↦ n ∈ c ∧ ∀ m ∈ c, n ≤ m) := by      ext x      simp_rw [mem_preimage, mem_singleton_iff, Finset.coe_filter, Finset.mem_powerset,        mem_setOf_eq, scσ₁, true_and]      constructor <;> intro h      · rw [← h]; exact ⟨eσ₁ x, fun m ↦ minσ₁ x⟩      · rw [← (candσ₁ x).le_min'_iff (necσ₁ x)] at h; obtain ⟨h₁, h₂ : n ≤ σ₁ x⟩ := h        exact le_antisymm ((candσ₁ x).min'_le _ h₁) h₂    simp_rw [eqv, Finset.coe_filter, Finset.mem_powerset, preimage_setOf_eq, measurableSet_setOf]    refine Measurable.and ?_ (mcσ₁.and (Measurable.forall fun m ↦ mcσ₁.imp measurable_const))    simp [scσ₁]  have rσ₁ : (range σ₁).Finite := by    suffices range σ₁ ⊆ Set.Icc (-B) B by exact (finite_Icc (-B : ℤ) B).subset this    simp_rw [range_subset_iff, mem_Icc, ← Finset.mem_Icc]; exact fun x ↦ scσ₁ x (eσ₁ x)  -- Incorporate `σ₁` into the main integral  simp_rw [candσ₁, Finset.mem_filter, Finset.mem_Icc] at eσ₁  change ∫⁻ x in G, T1 x ≤ _  conv_lhs => enter [2, x]; rw [(eσ₁ x).2]  -- Work analogously to define `σ₂`  let candσ₂ (x : X) :=    (Finset.Icc (σ₁ x) B).filter (fun s'' : ℤ ↦ T1' x (σ₁ x) = ‖T_S Q (σ₁ x) s'' f x‖ₑ)  have necσ₂ (x : X) : (candσ₂ x).Nonempty := by    rw [Finset.filter_nonempty_iff]    obtain ⟨s', ms', hs'⟩ := (Finset.Icc (σ₁ x) B).exists_max_image      (‖T_S Q (σ₁ x) · f x‖ₑ) ⟨σ₁ x, by simpa using (eσ₁ x).1.2⟩    use s', ms'; apply le_antisymm    · exact iSup₂_le hs'    · apply le_biSup _ ms'  have scσ₂ (x : X) : candσ₂ x ⊆ Finset.Icc (-B : ℤ) B :=    subset_trans (by simp [candσ₂]) (Finset.Icc_subset_Icc_left (eσ₁ x).1.1)  have mcσ₂ {n : ℤ} : Measurable (n ∈ candσ₂ ·) := by    simp_rw [candσ₂, Finset.mem_filter, Finset.mem_Icc]    apply Measurable.and    · apply Measurable.and ?_ measurable_const      rw [← measurableSet_setOf]; exact measurableSet_le mσ₁ measurable_const    · rw [← measurableSet_setOf]; apply measurableSet_eq_fun      · apply Measurable.comp (f := fun x ↦ (x, σ₁ x)) (g := fun p ↦ T1' p.1 p.2)        · exact measurable_from_prod_countable_left fun _ ↦ mT1'        · exact measurable_id.prodMk mσ₁      · apply Measurable.enorm        apply (Measurable.comp (f := fun x ↦ (x, σ₁ x)) (g := fun p ↦ T_S Q p.2 n f p.1))        · exact measurable_from_prod_countable_left fun _ ↦ measurable_T_S mf        · exact measurable_id.prodMk mσ₁  -- Work analogously to prove `σ₂`'s properties  let σ₂ (x : X) := (candσ₂ x).min' (necσ₂ x)  have eσ₂ (x : X) : σ₂ x ∈ candσ₂ x := (candσ₂ x).min'_mem (necσ₂ x)  have minσ₂ (x : X) {n : ℤ} (hn : n ∈ candσ₂ x) : σ₂ x ≤ n := (candσ₂ x).min'_le _ hn  have mσ₂ : Measurable σ₂ := by    classical    refine measurable_to_countable' fun n ↦ ?_    have eqv : σ₂ ⁻¹' {n} =        candσ₂ ⁻¹' ((Finset.Icc (-B : ℤ) B).powerset.filter fun c ↦ n ∈ c ∧ ∀ m ∈ c, n ≤ m) := by      ext x      simp_rw [mem_preimage, mem_singleton_iff, Finset.coe_filter, Finset.mem_powerset,        mem_setOf_eq, scσ₂, true_and]      constructor <;> intro h      · rw [← h]; exact ⟨eσ₂ x, fun m ↦ minσ₂ x⟩      · rw [← (candσ₂ x).le_min'_iff (necσ₂ x)] at h; obtain ⟨h₁, h₂ : n ≤ σ₂ x⟩ := h        exact le_antisymm ((candσ₂ x).min'_le _ h₁) h₂    simp_rw [eqv, Finset.coe_filter, Finset.mem_powerset, preimage_setOf_eq, measurableSet_setOf]    refine Measurable.and ?_ (mcσ₂.and (Measurable.forall fun m ↦ mcσ₂.imp measurable_const))    simp [scσ₂]  have rσ₂ : (range σ₂).Finite := by    suffices range σ₂ ⊆ Set.Icc (-B) B by exact (finite_Icc (-B : ℤ) B).subset this    simp_rw [range_subset_iff, mem_Icc, ← Finset.mem_Icc]; exact fun x ↦ scσ₂ x (eσ₂ x)  simp_rw [candσ₂, Finset.mem_filter, Finset.mem_Icc] at eσ₂  have lσ : σ₁ ≤ σ₂ := by intro x; exact (eσ₂ x).1.1  -- Complete the reduction  conv_lhs => enter [2, x]; rw [(eσ₂ x).2]  exact linearized_truncation hq hqq' bF bG mF mG mf nf mσ₁ mσ₂ rσ₁ rσ₂ lσ BST_T_Q