MeasureTheory.HasRestrictedWeakType.hasLorentzType

lemma HasRestrictedWeakType.hasLorentzType {𝕂 : Type*}  [RCLike 𝕂] [TopologicalSpace ε'] [ENormedSpace ε']  {T : (α → 𝕂) → (α' → ε')} {p q : ℝ≥0∞} (hpq : p.HolderConjugate q) (p_ne_top : p ≠ ⊤) (q_ne_top : q ≠ ⊤)  [SigmaFinite ν] {c : ℝ≥0} (c_pos : 0 < c)  (hT : HasRestrictedWeakType T p q μ ν c)  (T_meas : ∀ {f : α → 𝕂}, (MemLorentz f p 1 μ) → AEStronglyMeasurable (T f) ν)  (T_subadd : ∀ {f g : α → 𝕂}, (MemLorentz f p 1 μ) → (MemLorentz g p 1 μ) →    ∀ᵐ x ∂ν, ‖T (f + g) x‖ₑ ≤ ‖T f x‖ₑ + ‖T g x‖ₑ)  (T_submul : ∀ (a : 𝕂) (f : α → 𝕂), ∀ᵐ (x : α') ∂ν, ‖T (a • f) x‖ₑ ≤ ‖a‖ₑ * ‖T f x‖ₑ)  (weakly_cont_T : ∀ {f : α → 𝕂} {fs : ℕ → α → 𝕂},                     (MemLorentz f p 1 μ) →                     (∀ (n : ℕ), AEStronglyMeasurable (fs n) μ) →                     (∀ (a : α), Monotone (fun n ↦ ‖fs n a‖)) →                     (∀ (a : α), Filter.Tendsto (fun (n : ℕ) => fs n a) Filter.atTop (nhds (f a))) →                     (G : Set α') →    eLpNorm (T f) 1 (ν.restrict G) ≤ Filter.limsup (fun n ↦ eLpNorm (T (fs n)) 1 (ν.restrict G)) Filter.atTop)  (T_zero : T 0 =ᶠ[ae ν] 0)  (T_ae_eq_of_ae_eq : ∀ {f g : α → 𝕂} (_ : f =ᶠ[ae μ] g), T f =ᶠ[ae ν] T g) --TODO: incorporate into weakly_cont_T?    :    HasLorentzType T p 1 p ∞ μ ν (4 * c / p) := by  rw [mul_div_assoc]  apply HasRestrictedWeakType'.hasLorentzType hpq p_ne_top q_ne_top (by finiteness [hpq.ne_zero])  apply HasRestrictedWeakType'.of_hasRestrictedWeakType'_nnreal T_meas T_zero T_subadd T_submul  apply hasRestrictedWeakType'_nnreal c_pos p_ne_top q_ne_top hpq  · intro f hf    apply T_meas    rwa [memLorentz_iff_memLorentz_embedRCLike]  · intro f g hf hg    rw [← memLorentz_iff_memLorentz_embedRCLike (𝕂 := 𝕂)] at hf    rw [← memLorentz_iff_memLorentz_embedRCLike (𝕂 := 𝕂)] at hg    filter_upwards [T_subadd hf hg]    intro x h    apply h.trans_eq'    congr with x    simp  · intro a f    filter_upwards [T_submul (NNReal.toReal a) (RCLike.ofReal ∘ NNReal.toReal ∘ f)]    intro x h    convert h    · ext x      simp    · rw [enorm_eq_nnnorm, enorm_eq_nnnorm]      simp  · intro f g hfg    apply T_ae_eq_of_ae_eq    filter_upwards [hfg]    simp  · simpa  · intro F G hF F_finite hG G_finite    have := hT F G hF F_finite hG G_finite    constructor    · apply T_meas      rw [memLorentz_iff_memLorentz_embedRCLike]      constructor      · apply Measurable.aestronglyMeasurable        apply Measurable.indicator measurable_const hF      · rw [const_def, eLorentzNorm_indicator_const]        simp only [one_ne_zero, ↓reduceIte, one_ne_top, enorm_NNReal, ENNReal.coe_one, mul_one,          div_one, toReal_one, inv_one, ENNReal.rpow_one]        split_ifs        · simp        apply mul_lt_top (Ne.lt_top p_ne_top)        exact rpow_lt_top_of_nonneg (by simp) F_finite.ne    · simp only      convert this.2      ext x      simp only [comp_apply, NNReal.coe_indicator, NNReal.coe_one]      unfold indicator      split_ifs <;> simp  · intro fs hfs bddAbove_fs f hf G    apply weakly_cont_T    · rwa [memLorentz_iff_memLorentz_embedRCLike]    · intro n      apply Measurable.aestronglyMeasurable      apply RCLike.measurable_ofReal.comp      apply measurable_coe_nnreal_real.comp (SimpleFunc.measurable (fs n))    · intro x      simp only [Function.comp_apply, norm_algebraMap', Real.norm_eq_abs, NNReal.abs_eq]      exact fun ⦃a b⦄ a_1 ↦ hfs a_1 x    · intro x      have : Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x)) := by        apply tendsto_atTop_ciSup        · intro n m hmn          apply hfs hmn        · rw [bddAbove_def] at *          rcases bddAbove_fs with ⟨g, hg⟩          use g x          intro y hy          rcases hy with ⟨n, hn⟩          rw [← hn]          apply hg          use n      apply Filter.Tendsto.comp (y := (𝓝 ((toReal ∘ f) x)))      · apply Continuous.tendsto'        · continuity        · simp      apply Filter.Tendsto.comp (z := 𝓝 (toReal (f x))) _ this      apply NNReal.continuous_coe.tendsto'      rfl