MeasureTheory.hasStrongType_iff_hasLorentzType

lemma hasStrongType_iff_hasLorentzType [ESeminormedAddMonoid ε₁] [ESeminormedAddMonoid ε₂]  {T : (α → ε₁) → (α' → ε₂)} {c : ℝ≥0∞} :    HasStrongType T p q μ ν c ↔ HasLorentzType T p p q q μ ν c := by  unfold HasStrongType HasLorentzType  constructor  · intro h f hf    unfold MemLp MemLorentz at *    rw [eLorentzNorm_eq_eLpNorm hf.1] at *    have := h f hf    rwa [eLorentzNorm_eq_eLpNorm this.1]  · intro h f hf    unfold MemLp MemLorentz at *    rw [← eLorentzNorm_eq_eLpNorm hf.1] at *    have := h f hf    rwa [← eLorentzNorm_eq_eLpNorm this.1]