MeasureTheory.HasRestrictedWeakType.hasRestrictedWeakType'_nnreal

theorem HasRestrictedWeakType.hasRestrictedWeakType'_nnreal [TopologicalSpace ε'] [ENormedSpace ε']    {c : ℝ≥0} (c_pos : 0 < c) {T : (α → ℝ≥0) → α' → ε'} (p_ne_top : p ≠ ⊤) (q_ne_top : q ≠ ⊤)    (hpq : p.HolderConjugate q)    (T_meas : ∀ {f : α → ℝ≥0}, (MemLorentz f p 1 μ) → AEStronglyMeasurable (T f) ν)    (T_subadd : ∀ {f g : α → ℝ≥0}, (MemLorentz f p 1 μ) → (MemLorentz g p 1 μ) →      ∀ᵐ x ∂ν, ‖T (f + g) x‖ₑ ≤ ‖T f x‖ₑ + ‖T g x‖ₑ)    (T_submul : ∀ (a : ℝ≥0) (f : α → ℝ≥0), ∀ᵐ x ∂ν, ‖T (a • f) x‖ₑ ≤ ‖a‖ₑ * ‖T f x‖ₑ)    (T_ae_eq_of_ae_eq : ∀ {f g : α → ℝ≥0}, (f =ᶠ[ae μ] g) → T f =ᶠ[ae ν] T g)    (T_zero : T 0 =ᶠ[ae ν] 0)    (hT : HasRestrictedWeakType T p q μ ν c)    (weakly_cont_T : WeaklyContinuous T p μ ν) :      HasRestrictedWeakType' T p q μ ν (c / p) := by  have T_zero_of_ae_zero : ∀ {f : α → ℝ≥0} (_ : f =ᶠ[ae μ] 0), enorm ∘ T f =ᶠ[ae ν] 0 := by    intro f hf    filter_upwards [T_ae_eq_of_ae_eq hf, T_zero]    intro a h h'    simp only [comp_apply, Pi.zero_apply, enorm_eq_zero]    rwa [h]  have hcp : 0 < ↑c / p := by    simp only [ENNReal.div_pos_iff, ne_eq, ENNReal.coe_eq_zero]    use c_pos.ne', p_ne_top  intro f hf' G hG  use T_meas hf'  wlog hf : Measurable f generalizing f  · rcases hf'.1 with ⟨g, stronglyMeasurable_g, hfg⟩    have hg' : MemLorentz g p 1 μ := by      use StronglyMeasurable.aestronglyMeasurable stronglyMeasurable_g      convert hf'.2 using 1      symm      exact eLorentzNorm_congr_ae hfg    have hg : Measurable g := stronglyMeasurable_g.measurable    convert this g hg' hg using 1    · apply eLpNorm_congr_ae      apply ae_restrict_le      exact T_ae_eq_of_ae_eq hfg    · congr 2      exact eLorentzNorm_congr_ae hfg  have hp : 1 ≤ p := hpq.one_le  have p_ne_zero : p ≠ 0 := hpq.ne_zero  rw [eLorentzNorm_eq_eLorentzNorm' p_ne_zero p_ne_top]  revert hf'  revert f  apply @Measurable.nnreal_induction _ m0  · intro f    induction f using SimpleFunc.induction''    · rename_i a s hs      rw [SimpleFunc.coe_restrict _ hs]      have : s.indicator (Function.const α a) = a • (s.indicator (fun _ ↦ 1)) := by        ext x        simp only [Pi.smul_apply, smul_eq_mul]        rw [← Set.indicator_const_mul]        congr        simp      intro hf'      calc _        _ = eLpNorm (T (a • (s.indicator (fun _ ↦ 1)))) 1 (ν.restrict G) := by          congr 1          ext x          congr        _ ≤ ‖a‖ₑ * eLpNorm (T ((s.indicator (fun _ ↦ 1)))) 1 (ν.restrict G) := by          rw [← eLpNorm_const_smul']          apply eLpNorm_mono_enorm_ae          apply ae_restrict_le          simp only [Pi.smul_apply, enorm_smul_eq_smul]          apply T_submul        _ ≤ ‖a‖ₑ * (c * (μ s) ^ p⁻¹.toReal * (ν G) ^ q⁻¹.toReal) := by          gcongr          apply hT.without_finiteness p_ne_zero p_ne_top hpq.symm.ne_zero q_ne_top c_pos T_zero_of_ae_zero s G hs hG        _ = c * (‖a‖ₑ * μ s ^ p⁻¹.toReal) * (ν G) ^ q⁻¹.toReal := by ring        _ = (c / p) * eLorentzNorm' (s.indicator (Function.const α a)) p 1 μ * ν G ^ q⁻¹.toReal := by          rw [eLorentzNorm'_indicator_const (by simp) p_ne_zero p_ne_top]          rw [← mul_assoc (c / p), ENNReal.div_mul_cancel p_ne_zero p_ne_top]    · rename_i f a s hs hfs hf hg      rw [SimpleFunc.coe_add]      set g := (SimpleFunc.const α a).restrict s with g_def      intro hfg'      have hf' : MemLorentz f p 1 μ :=        ⟨by fun_prop, hfg'.2.trans_le' <| eLorentzNorm_mono_enorm_ae (by simp)⟩      have hg' : MemLorentz g p 1 μ := ⟨by fun_prop, hfg'.2.trans_le' <| eLorentzNorm_mono_enorm_ae (by simp)⟩      calc _        _ ≤ eLpNorm (T f) 1 (ν.restrict G) + eLpNorm (T g) 1 (ν.restrict G) := by          nth_rw 2 [← eLpNorm_enorm]          nth_rw 3 [← eLpNorm_enorm]          apply (eLpNorm_add_le _ _ (by rfl)).trans'          · apply eLpNorm_mono_enorm_ae            simp only [Pi.add_apply, enorm_eq_self]            exact ae_restrict_le (T_subadd hf' hg')          · exact (T_meas hf').enorm.aestronglyMeasurable.restrict          · exact (T_meas hg').enorm.aestronglyMeasurable.restrict        _ ≤ c / p * eLorentzNorm' f p 1 μ * ν G ^ q⁻¹.toReal + c / p *  eLorentzNorm' g p 1 μ * ν G ^ q⁻¹.toReal := by          gcongr          · exact hf hf'          · exact hg hg'        _ = c / p * eLorentzNorm' (f + g) p 1 μ * ν G ^ q⁻¹.toReal := by          rw [← add_mul, ← mul_add]          congr          rw [eLorentzNorm'_eq_integral_distribution_rpow,            eLorentzNorm'_eq_integral_distribution_rpow, eLorentzNorm'_eq_integral_distribution_rpow]          rw [← mul_add]          congr 1          rw [SimpleFunc.coe_add, g_def, SimpleFunc.coe_restrict _ hs, SimpleFunc.coe_const]          symm          calc _            _ = ∫⁻ (t : ℝ≥0), (if t < a then μ s else distribution f (t - a) μ) ^ p.toReal⁻¹ := by              congr with t              congr              rw [distribution_indicator_add_of_support_subset_nnreal (μ := μ) hfs]              simp only [ENNReal.coe_lt_coe]            _ = ∫⁻ (t : ℝ≥0), if t < a then μ s ^ p.toReal⁻¹ else distribution f (t - a) μ ^ p.toReal⁻¹ := by              simp only [ite_pow]            _ = ∫⁻ (t : ℝ≥0), (Set.Iio a).indicator (fun _ ↦ μ s ^ p.toReal⁻¹) t                  + (Set.Ici a).indicator (fun t ↦ distribution f (t - a) μ ^ p.toReal⁻¹) t := by              congr with t              rw [← Set.compl_Iio, ← Pi.add_apply, Set.indicator_add_compl_eq_piecewise]              unfold Set.piecewise              simp            _ = a * μ s ^ p.toReal⁻¹ + ∫⁻ (t : ℝ≥0), distribution f t μ ^ p.toReal⁻¹ := by              rw [lintegral_add_left (by measurability)]              congr 1              · rw [lintegral_indicator_const measurableSet_Iio, NNReal.volume_Iio, mul_comm]              · rw [lintegral_indicator measurableSet_Ici, setLIntegral_nnreal_Ici]                simp          rw [add_comm]          congr          apply (ENNReal.mul_right_inj p_ne_zero p_ne_top).mp          rw [← eLorentzNorm'_eq_integral_distribution_rpow, eLorentzNorm'_indicator_const (by simp) p_ne_zero p_ne_top]          simp  · intro f hf h hf'    by_cases f_zero : f =ᶠ[ae μ] 0    · have := T_zero_of_ae_zero f_zero      rw [← eLorentzNorm_eq_eLorentzNorm' hpq.ne_zero p_ne_top, eLorentzNorm_congr_ae f_zero,          eLpNorm_zero_of_ae_zero' (T_zero_of_ae_zero f_zero).restrict]      simp only [eLorentzNorm_zero, mul_zero, toReal_inv, zero_mul, nonpos_iff_eq_zero]    by_cases hG' : ν G = ∞    · rw [hG', ENNReal.top_rpow_of_pos, ENNReal.mul_top]      · exact le_top      · apply mul_ne_zero hcp.ne'        contrapose! f_zero        rwa [eLorentzNorm'_eq_zero_iff p_ne_zero p_ne_top (by simp)] at f_zero      · simp only [toReal_inv, inv_pos]        exact ENNReal.toReal_pos hpq.symm.ne_zero q_ne_top    rw [← SimpleFunc.iSup_nnapprox hf] at hf'    calc _      _ ≤ Filter.limsup (fun n ↦ eLpNorm (T (SimpleFunc.nnapprox f n)) 1 (ν.restrict G)) Filter.atTop := by        nth_rw 1 [← SimpleFunc.iSup_nnapprox hf]        apply weakly_cont_T SimpleFunc.monotone_nnapprox _ hf' G        use f        rw [mem_upperBounds]        intro g hg        rcases hg with ⟨n, hn⟩        rw [← hn]        intro x        apply SimpleFunc.nnapprox_le hf      _ ≤ Filter.limsup (fun n ↦ (c / p) * eLorentzNorm' (SimpleFunc.nnapprox f n) p 1 μ * ν G ^ q⁻¹.toReal) Filter.atTop := by        apply Filter.limsup_le_limsup _        filter_upwards        intro n        apply h n _        use (by fun_prop)        apply hf'.2.trans_le'        apply eLorentzNorm_mono_enorm_ae        apply Filter.Eventually.of_forall        intro x        simp only [enorm_NNReal, ENNReal.coe_le_coe]        rw [SimpleFunc.iSup_nnapprox_apply hf]        apply SimpleFunc.nnapprox_le hf      _ ≤ (c / p) * eLorentzNorm' f p 1 μ * ν G ^ q⁻¹.toReal := by        simp_rw [mul_assoc]        rw [ENNReal.limsup_const_mul_of_ne_top (ENNReal.div_ne_top (by simp) p_ne_zero)]        gcongr        rw [ENNReal.limsup_mul_const_of_ne_top (ENNReal.rpow_ne_top_of_nonneg (by simp) hG'),          mul_comm]        gcongr        apply Filter.limsup_le_of_le (f := _)        filter_upwards with n        apply eLorentzNorm'_mono_enorm_ae        filter_upwards with x        simp only [enorm_NNReal, ENNReal.coe_le_coe]        exact SimpleFunc.approx_le hf bot_eq_zero'