MeasureTheory.HasRestrictedWeakType'.hasLorentzType

lemma HasRestrictedWeakType'.hasLorentzType [SigmaFinite ν]  {𝕂 : Type*} [RCLike 𝕂] [TopologicalSpace ε'] [ENormedSpace ε']  {T : (α → 𝕂) → (α' → ε')} (hpq : p.HolderConjugate q) (hp : p ≠ ⊤) (hq : q ≠ ⊤)  {c : ℝ≥0∞} (hc : c ≠ ⊤) (hT : HasRestrictedWeakType' T p q μ ν c) :    HasLorentzType T p 1 p ∞ μ ν c := by  intro f hf  have hf' : AEStronglyMeasurable (T f) ν := (hT f hf ∅ MeasurableSet.empty).1  use (hT f hf ∅ MeasurableSet.empty).1  rw [eLorentzNorm_eq_wnorm hpq.ne_zero, wnorm_ne_top hp, wnorm']  apply iSup_le  intro l  by_cases l_zero : l = 0  · simp [l_zero]  set G := {x | ↑l < ‖T f x‖ₑ}  have hG : NullMeasurableSet G ν := by    unfold G    exact nullMeasurableSet_lt aemeasurable_const (by fun_prop)  rcases hG.exists_measurable_superset_ae_eq  with ⟨G', _, hG', G'G⟩  have measure_G'G := measure_congr G'G  have measure_G : ν G = distribution (T f) l ν := by rfl  rw [← measure_G]  have p_toReal_pos : 0 < p.toReal := toReal_pos hpq.ne_zero hp  have q_toReal_pos : 0 < q.toReal := toReal_pos hpq.symm.ne_zero hq  by_cases G_finite : ν G = ⊤  · exfalso    rw [← measure_G'G] at G_finite    set r := (c * eLorentzNorm f p 1 μ / ↑l) ^ p.toReal with r_def    have : r < ν G' := by      rw [G_finite]      unfold r      apply (ENNReal.rpow_lt_top_iff_of_pos p_toReal_pos).mpr      have := hf.2.ne      exact ENNReal.div_lt_top (by finiteness) (by simpa)    rcases ν.exists_subset_measure_lt_top hG' this with ⟨H, hH, H_subset_G', H_gt, H_finite⟩    have H_pos := zero_le.trans_lt H_gt    apply (hT f hf H hH).2.not_gt    calc _      _ < l * ν H := by        rw [← ENNReal.lt_div_iff_mul_lt            (by left; rw [ne_eq, ENNReal.rpow_eq_zero_iff_of_pos (by simpa)]; exact H_pos.ne.symm)            (by left; apply ENNReal.rpow_ne_top_of_nonneg (by simp) H_finite.ne), mul_div_assoc]        nth_rw 1 [← ENNReal.rpow_one (ν H)]        have : 1 - q⁻¹.toReal = p⁻¹.toReal := by          have hpq' := ENNReal.holderConjugate_iff.mp hpq          have : 1 = ENNReal.toReal 1 := by simp          rw [this, ← hpq', toReal_add, add_sub_cancel_right]          · simp only [ne_eq, inv_eq_top]            exact hpq.ne_zero          · simp only [ne_eq, inv_eq_top]            exact hpq.symm.ne_zero        rw [← ENNReal.rpow_sub _ _ H_pos.ne.symm H_finite.ne, this, mul_comm (ofNNReal l),            ← ENNReal.div_lt_iff (by left; simpa) (by left; simp),            ← ENNReal.rpow_rpow_inv (toReal_ne_zero.mpr ⟨hpq.ne_zero, hp⟩) (c * _ / ↑l),            ← r_def, toReal_inv]        apply ENNReal.rpow_lt_rpow H_gt (inv_pos.mpr p_toReal_pos)      _ = ∫⁻ (x : α') in H, l ∂ν := by        rw [setLIntegral_const]      _ ≤ ∫⁻ (x : α') in H, ‖T f x‖ₑ ∂ν := by        apply setLIntegral_mono_ae' hH        filter_upwards [G'G]        intro x h hx        have : G x := by          rw [← h]          exact H_subset_G' hx        exact this.le      _ = eLpNorm (T f) 1 (ν.restrict H) := by        rw [eLpNorm_one_eq_lintegral_enorm]  rw [← Ne, ← lt_top_iff_ne_top] at G_finite  have G'_finite : ν G' < ∞ := by    convert G_finite  by_cases G_zero : ν G = 0  · rw [G_zero, zero_rpow_of_pos]    · simp    simp only [inv_pos]    exact toReal_pos hpq.ne_zero hp  calc _    _ = ↑l * ν G / ν G ^ q⁻¹.toReal := by      rw [mul_div_assoc]      congr      rw [ENNReal.eq_div_iff,          ← ENNReal.rpow_add, ← ENNReal.toReal_inv, ← ENNReal.toReal_add, add_comm, ENNReal.holderConjugate_iff.mp hpq]      · simp only [ENNReal.toReal_one, ENNReal.rpow_one]      · rw [ne_eq, ENNReal.inv_eq_top]        exact hpq.symm.ne_zero      · rw [ne_eq, ENNReal.inv_eq_top]        exact hpq.ne_zero      · exact G_zero      · exact G_finite.ne      · simp only [toReal_inv, ne_eq, ENNReal.rpow_eq_zero_iff, inv_pos, inv_neg'', not_or,        not_and, not_lt, toReal_nonneg, implies_true, and_true]        intro        contradiction      · simp only [toReal_inv, ne_eq, rpow_eq_top_iff, inv_neg'', inv_pos, not_or, not_and,        not_lt, toReal_nonneg, implies_true, true_and]        intro h        exfalso        exact G_finite.ne h    _ ≤ (∫⁻ (x : α') in G, ‖T f x‖ₑ ∂ν) / ν G ^ q⁻¹.toReal := by      gcongr      rw [← Measure.restrict_eq_self _ (subset_refl G)]      calc _        _ ≤ ↑l * (ν.restrict G) {x | ↑l ≤ ‖T f x‖ₑ} := by          gcongr          intro x hx          unfold G at hx          rw [Set.mem_setOf_eq] at hx ⊢; exact hx.le      apply mul_meas_ge_le_lintegral₀ hf'.enorm.restrict    _ ≤ (c * _ * ν G ^ q⁻¹.toReal) / ν G ^ q⁻¹.toReal := by      gcongr      convert (hT f hf G' hG').2 using 2      · rw [eLpNorm_one_eq_lintegral_enorm]        apply setLIntegral_congr G'G.symm      · congr 1        exact measure_G'G.symm    _ = c * _  := by      apply ENNReal.mul_div_cancel_right      · contrapose! G_zero        rwa [ENNReal.rpow_eq_zero_iff_of_pos] at G_zero        simp only [toReal_inv, inv_pos]        apply toReal_pos hpq.symm.ne_zero hq      · exact ENNReal.rpow_ne_top' G_zero G_finite.ne