MeasureTheory.HasRestrictedWeakType.without_finiteness

lemma HasRestrictedWeakType.without_finiteness [ESeminormedAddMonoid ε₂] {T : (α → β) → (α' → ε₂)}    (p_ne_zero : p ≠ 0) (p_ne_top : p ≠ ⊤) (q_ne_zero : q ≠ 0) (q_ne_top : q ≠ ⊤)    {c : ℝ≥0} (c_pos : 0 < c) (hT : HasRestrictedWeakType T p q μ ν c)    (T_zero_of_ae_zero : ∀ {f : α → β} (_ : f =ᶠ[ae μ] 0), enorm ∘ T f =ᶠ[ae ν] 0) :  ∀ (F : Set α) (G : Set α'), (MeasurableSet F) → (MeasurableSet G) →    eLpNorm (T (F.indicator (fun _ ↦ 1))) 1 (ν.restrict G)      ≤ c * (μ F) ^ p⁻¹.toReal * (ν G) ^ q⁻¹.toReal := by  intro F G hF hG  have p_inv_pos : 0 < p⁻¹.toReal := by    simp only [ENNReal.toReal_inv, inv_pos, ENNReal.toReal_pos p_ne_zero p_ne_top]  have q_inv_pos : 0 < q⁻¹.toReal := by    simp only [ENNReal.toReal_inv, inv_pos, ENNReal.toReal_pos q_ne_zero q_ne_top]  by_cases hFG : μ F < ∞ ∧ ν G < ∞  · exact (hT F G hF hFG.1 hG hFG.2).2  · rw [not_and_or] at hFG    rcases hFG with hF | hG    · by_cases G_zero : ν G = 0      · rw [G_zero, ENNReal.zero_rpow_of_pos q_inv_pos]        simp only [ENNReal.toReal_inv, mul_zero, nonpos_iff_eq_zero]        convert eLpNorm_measure_zero        simpa      simp only [not_lt, top_le_iff] at hF      rw [hF]      convert le_top      rw [ENNReal.mul_eq_top]      right      constructor      · rw [ENNReal.top_rpow_of_pos p_inv_pos, ENNReal.mul_top (by simp [c_pos.ne'])]      simp only [ENNReal.toReal_inv, ne_eq, ENNReal.rpow_eq_zero_iff, inv_pos, inv_neg'', not_or,        not_and, not_lt, ENNReal.toReal_nonneg, implies_true, and_true]      intro h      exfalso      exact G_zero h    · by_cases F_zero : μ F = 0      · rw [F_zero, ENNReal.zero_rpow_of_pos p_inv_pos]        simp only [mul_zero, ENNReal.toReal_inv, zero_mul, nonpos_iff_eq_zero]        rw [← nonpos_iff_eq_zero]        apply (eLpNorm_restrict_le _ _ _ _).trans        simp only [nonpos_iff_eq_zero]        apply eLpNorm_zero_of_ae_zero' (T_zero_of_ae_zero (indicator_meas_zero F_zero))      simp only [not_lt, top_le_iff] at hG      rw [hG]      convert le_top      rw [ENNReal.mul_eq_top]      left      constructor      · simp only [ENNReal.toReal_inv, ne_eq, mul_eq_zero, ENNReal.rpow_eq_zero_iff, inv_pos,          inv_neg'', not_or, not_and, not_lt, ENNReal.toReal_nonneg, implies_true, and_true]        use (by simp [c_pos.ne'])        intro h        exfalso        exact F_zero h      rw [ENNReal.top_rpow_of_pos q_inv_pos]