MeasureTheory.HasRestrictedWeakType'.of_hasRestrictedWeakType'_nnreal

lemma HasRestrictedWeakType'.of_hasRestrictedWeakType'_nnreal  {𝕂 : Type*} [RCLike 𝕂] [TopologicalSpace ε'] [ENormedSpace ε']  {T : (α → 𝕂) → (α' → ε')}  (T_meas : ∀ {f : α → 𝕂}, (MemLorentz f p 1 μ) → AEStronglyMeasurable (T f) ν)  (T_zero : T 0 =ᶠ[ae ν] 0)  (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‖ₑ)  {c : ℝ≥0∞} (hT_nnreal : HasRestrictedWeakType' (fun f ↦ T (⇑(algebraMap ℝ 𝕂) ∘ toReal ∘ f)) p q μ ν c) :    HasRestrictedWeakType' T p q μ ν (4 * c) := by  intro f hf G hG  use T_meas hf  have : (4 : ℝ≥0∞) = 1 * 2 * 2 := by norm_num  rw [this]  revert f  apply RCLike.induction (motive := fun f n ↦ eLpNorm (T f) 1 (ν.restrict G) ≤ (n : ℝ≥0∞) * c * eLorentzNorm f p 1 μ * (ν G) ^ q⁻¹.toReal)  · exact MemLorentz.add  · intro f c hc hf    constructor    · have := hf.1      rw [aestronglyMeasurable_iff_aemeasurable]      apply AEMeasurable.comp_aemeasurable (by fun_prop)      apply AEMeasurable.comp_aemeasurable (by fun_prop)      unfold RCLike.component      apply AEMeasurable.comp_aemeasurable (by fun_prop) hf.1.aemeasurable    · apply hf.2.trans_le'      apply eLorentzNorm_mono_enorm_ae      apply Eventually.of_forall      intro x      have : NNNorm 𝕂 := by infer_instance      rw [← ofReal_norm, ← ofReal_norm]      simp only [comp_apply, norm_algebraMap', Real.norm_eq_abs, NNReal.abs_eq,        ofReal_coe_nnreal, ofReal_norm, coe_le_enorm, ge_iff_le]      exact RCLike.component_le_nnnorm hc  · intro f c hc hf    constructor    · apply AEStronglyMeasurable.const_smul hf.1    · apply hf.2.trans_le'      apply eLorentzNorm_mono_enorm_ae      apply Eventually.of_forall      intro x      simp only [Pi.smul_apply, smul_eq_mul, enorm_mul]      nth_rw 2 [← one_mul ‖f x‖ₑ]      gcongr      rw [← ofReal_norm]      apply ENNReal.ofReal_le_of_le_toReal      simp only [toReal_one]      exact RCLike.Components.norm_le_one hc  · rw [one_mul]    intro f hf    rw [memLorentz_iff_memLorentz_embedRCLike] at hf    rw [eLorentzNorm_congr_enorm_ae (Eventually.of_forall RCLike.enorm_eq_enorm_embedRCLike)]    apply (hT_nnreal f hf G hG).2  · intro n f g hf_add hg_add hf hg hf' hg'    calc _      _ ≤ eLpNorm ((fun x ↦ ‖T f x‖ₑ) + (fun x ↦ ‖T g x‖ₑ)) 1 (ν.restrict G) := by        apply eLpNorm_mono_enorm_ae        simp only [enorm_eq_self]        apply ae_restrict_le        exact T_subadd hf hg    apply (eLpNorm_add_le (T_meas hf).enorm.aestronglyMeasurable.restrict                          (T_meas hg).enorm.aestronglyMeasurable.restrict                          (by simp)).trans    rw [mul_comm n, mul_assoc 2, mul_assoc 2, mul_assoc 2, two_mul]    rw [eLpNorm_enorm, eLpNorm_enorm]    apply (add_le_add hf' hg').trans    gcongr    · apply eLorentzNorm_mono_enorm_ae      apply Eventually.of_forall      intro x      rw [← ofReal_norm, ← ofReal_norm, Pi.add_apply]      apply ENNReal.ofReal_le_ofReal hf_add    · apply eLorentzNorm_mono_enorm_ae      apply Eventually.of_forall      intro x      rw [← ofReal_norm, ← ofReal_norm]      apply ENNReal.ofReal_le_ofReal hg_add  · intro f b n hb hf    by_cases h : b = 0    · intro _      rw [h]      simp only [zero_smul, eLorentzNorm_zero, mul_zero, toReal_inv, zero_mul, nonpos_iff_eq_zero]      apply eLpNorm_zero_of_ae_zero      exact ae_restrict_le T_zero    gcongr    · apply eLpNorm_mono_enorm_ae      apply ae_restrict_le      filter_upwards [T_submul b f]      intro x hx      rw [← one_mul ‖T f x‖ₑ]      apply hx.trans      gcongr      rw [enorm_eq_nnnorm]      simp only [coe_le_one_iff]      apply RCLike.Components.norm_le_one hb    · apply eLorentzNorm_mono_enorm_ae      apply Eventually.of_forall      intro x      simp only [Pi.smul_apply, smul_eq_mul, enorm_mul]      rw [← ofReal_norm, ← ofReal_norm, RCLike.Components.norm_eq_one hb h]      simp