theorem MeasureTheory.eLorentzNorm'_mono_enorm_ae {α : Type u_1} {ε : Type u_2} {ε' : Type u_3} {m0 : MeasurableSpace α} {p q : ENNReal} {μ : Measure α} [ENorm ε] [ENorm ε'] {f : α → ε'} {g : α → ε} (h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ) : eLorentzNorm' f p q μ ≤ eLorentzNorm' g p q μ

theorem MeasureTheory.eLorentzNorm_mono_enorm_ae {α : Type u_1} {ε : Type u_2} {ε' : Type u_3} {m0 : MeasurableSpace α} {p q : ENNReal} {μ : Measure α} [ENorm ε] [ENorm ε'] {f : α → ε'} {g : α → ε} (h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ) : eLorentzNorm f p q μ ≤ eLorentzNorm g p q μ

theorem MeasureTheory.eLorentzNorm_congr_enorm_ae {α : Type u_1} {ε : Type u_2} {ε' : Type u_3} {m0 : MeasurableSpace α} {p q : ENNReal} {μ : Measure α} [ENorm ε] [ENorm ε'] {f : α → ε'} {g : α → ε} (hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = ‖g x‖ₑ) : eLorentzNorm f p q μ = eLorentzNorm g p q μ

theorem MeasureTheory.eLorentzNorm_congr_ae {α : Type u_1} {ε' : Type u_3} {m0 : MeasurableSpace α} {p q : ENNReal} {μ : Measure α} [ENorm ε'] {f g : α → ε'} (hfg : f =ᶠ[ae μ] g) : eLorentzNorm f p q μ = eLorentzNorm g p q μ

@[simp]

theorem MeasureTheory.eLorentzNorm_enorm {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p q : ENNReal} {μ : Measure α} [ENorm ε] (f : α → ε) : eLorentzNorm (fun (x : α) => ‖f x‖ₑ) p q μ = eLorentzNorm f p q μ

theorem MeasureTheory.eLorentzNorm'_eq_zero_of_ae_enorm_zero {α : Type u_1} {m0 : MeasurableSpace α} {p q : ENNReal} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε} (h : enorm ∘ f =ᶠ[ae μ] 0) (p_ne_zero : p ≠ 0) (p_ne_top : p ≠ ⊤) : eLorentzNorm' f p q μ = 0

theorem MeasureTheory.eLorentzNorm_eq_zero_of_ae_enorm_zero {α : Type u_1} {m0 : MeasurableSpace α} {p q : ENNReal} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε} (h : enorm ∘ f =ᶠ[ae μ] 0) : eLorentzNorm f p q μ = 0

theorem MeasureTheory.eLorentzNorm'_eq_zero_of_ae_zero {α : Type u_1} {m0 : MeasurableSpace α} {p q : ENNReal} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε} (p_ne_zero : p ≠ 0) (p_ne_top : p ≠ ⊤) (h : f =ᶠ[ae μ] 0) : eLorentzNorm' f p q μ = 0

theorem MeasureTheory.eLorentzNorm_eq_zero_of_ae_zero {α : Type u_1} {m0 : MeasurableSpace α} {p q : ENNReal} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε} (h : f =ᶠ[ae μ] 0) : eLorentzNorm f p q μ = 0

theorem MeasureTheory.ae_eq_zero_of_eLorentzNorm'_eq_zero {α : Type u_1} {m0 : MeasurableSpace α} {p q : ENNReal} {μ : Measure α} {ε : Type u_5} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} (p_ne_zero : p ≠ 0) (p_ne_top : p ≠ ⊤) (q_ne_zero : q ≠ 0) (h : eLorentzNorm' f p q μ = 0) : f =ᶠ[ae μ] 0

theorem MeasureTheory.eLorentzNorm'_eq_zero_iff {α : Type u_1} {m0 : MeasurableSpace α} {p q : ENNReal} {μ : Measure α} {ε : Type u_5} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} (p_ne_zero : p ≠ 0) (p_ne_top : p ≠ ⊤) (q_ne_zero : q ≠ 0) : eLorentzNorm' f p q μ = 0 ↔ f =ᶠ[ae μ] 0

theorem MeasureTheory.eLorentzNorm_eq_zero_iff {α : Type u_1} {m0 : MeasurableSpace α} {p q : ENNReal} {μ : Measure α} {ε : Type u_5} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} (p_ne_zero : p ≠ 0) (q_ne_zero : q ≠ 0) : eLorentzNorm f p q μ = 0 ↔ f =ᶠ[ae μ] 0

@[simp]

theorem MeasureTheory.eLorentzNorm_zero {α : Type u_1} {m0 : MeasurableSpace α} {p q : ENNReal} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] : eLorentzNorm 0 p q μ = 0

@[simp]

theorem MeasureTheory.eLorentzNorm_zero' {α : Type u_1} {m0 : MeasurableSpace α} {p q : ENNReal} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] : eLorentzNorm (fun (x : α) => 0) p q μ = 0

theorem MeasureTheory.eLorentzNorm_eq_eLpNorm {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) : eLorentzNorm f p p μ = eLpNorm f p μ

theorem MeasureTheory.eLorentzNorm'_eq_wnorm {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] (p_ne_top : p ≠ ⊤) {f : α → ε} {μ : Measure α} : eLorentzNorm' f p ⊤ μ = wnorm f p μ

theorem MeasureTheory.eLorentzNorm_eq_wnorm {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] (p_ne_zero : p ≠ 0) {f : α → ε} {μ : Measure α} : eLorentzNorm f p ⊤ μ = wnorm f p μ

theorem MeasureTheory.eLorentzNorm'_eq {α : Type u_1} {m0 : MeasurableSpace α} {p q : ENNReal} {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] (p_nonzero : p ≠ 0) (p_ne_top : p ≠ ⊤) {f : α → ε} {μ : Measure α} : eLorentzNorm' f p q μ = eLpNorm (fun (t : NNReal) => ↑t ^ p⁻¹.toReal * rearrangement f (↑t) μ) q (volume.withDensity fun (t : NNReal) => (↑t)⁻¹)

theorem MeasureTheory.eLorentzNorm'_eq' {α : Type u_1} {m0 : MeasurableSpace α} {p q : ENNReal} {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] (p_nonzero : p ≠ 0) (p_ne_top : p ≠ ⊤) {f : α → ε} {μ : Measure α} : eLorentzNorm' f p q μ = eLpNorm (fun (t : NNReal) => ↑t ^ (p⁻¹.toReal - q⁻¹.toReal) * rearrangement f (↑t) μ) q volume

theorem MeasureTheory.eLorentzNorm_eq {α : Type u_1} {m0 : MeasurableSpace α} {p q : ENNReal} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] (p_nonzero : p ≠ 0) (p_ne_top : p ≠ ⊤) {f : α → ε} : eLorentzNorm f p q μ = eLpNorm (fun (t : NNReal) => ↑t ^ p⁻¹.toReal * rearrangement f (↑t) μ) q (volume.withDensity fun (t : NNReal) => (↑t)⁻¹)

theorem MeasureTheory.eLorentzNorm'_indicator_const {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {a : ε} (ha : ‖a‖ₑ ≠ ⊤) {s : Set α} (p_ne_zero : p ≠ 0) (p_ne_top : p ≠ ⊤) : eLorentzNorm' (s.indicator (Function.const α a)) p 1 μ = p * (‖a‖ₑ * μ s ^ p⁻¹.toReal)

theorem MeasureTheory.eLorentzNorm'_indicator_const' {α : Type u_1} {m0 : MeasurableSpace α} {p q : ENNReal} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {a : ε} {s : Set α} (p_ne_zero : p ≠ 0) (p_ne_top : p ≠ ⊤) (q_ne_zero : q ≠ 0) (q_ne_top : q ≠ ⊤) : eLorentzNorm' (s.indicator (Function.const α a)) p q μ = (p / q) ^ q.toReal⁻¹ * μ s ^ p.toReal⁻¹ * ‖a‖ₑ

@[simp]

theorem MeasureTheory.eLorentzNorm_indicator_const {α : Type u_1} {m0 : MeasurableSpace α} {p q : ENNReal} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {a : ε} {s : Set α} : eLorentzNorm (s.indicator (Function.const α a)) p q μ = if p = 0 then 0 else if q = 0 then 0 else if p = ⊤ then if μ s = 0 then 0 else if q = ⊤ then ‖a‖ₑ else ⊤ * ‖a‖ₑ else if q = ⊤ then μ s ^ p.toReal⁻¹ * ‖a‖ₑ else (p / q) ^ q.toReal⁻¹ * μ s ^ p.toReal⁻¹ * ‖a‖ₑ

theorem MeasureTheory.MemLorentz_iff_MemLp {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε} : MemLorentz f p p μ ↔ MemLp f p μ

theorem MeasureTheory.MemLorentz_of_MemLorentz_ge {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {r₁ r₂ : ENNReal} (r₁_pos : 0 < r₁) (r₁_le_r₂ : r₁ ≤ r₂) {f : α → ε} (hf : MemLorentz f p r₁ μ) : MemLorentz f p r₂ μ

theorem MeasureTheory.MemLorentz.memLp {α : Type u_1} {m0 : MeasurableSpace α} {p q : ENNReal} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε} (hf : MemLorentz f p q μ) (h : q ∈ Set.Ioc 0 p) : MemLp f p μ