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.essSup_le_iSup {α : Type u_5} {β : Type u_6} {m : MeasurableSpace α} {μ : Measure α} [CompleteLattice β] (f : α → β) : essSup f μ ≤ ⨆ (i : α), f i

theorem MeasureTheory.iSup_le_essSup {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (h : ∀ {x : α} {a : ENNReal}, a < f x → μ {y : α | a < f y} ≠ 0) : ⨆ (x : α), f x ≤ essSup f μ

theorem MeasureTheory.helper {f : ENNReal → ENNReal} {x : ENNReal} (hx : x ≠ ⊤) (hf : ContinuousWithinAt f (Set.Ioi x) x) {a : ENNReal} (ha : a < f x) : volume {y : ENNReal | a < f y} ≠ 0

theorem MeasureTheory.ContinuousWithinAt.ennreal_mul {X : Type u_5} [TopologicalSpace X] {f g : X → ENNReal} {s : Set X} {t : X} (hf : ContinuousWithinAt f s t) (hg : ContinuousWithinAt g s t) (h₁ : f t ≠ 0 ∨ g t ≠ ⊤) (h₂ : g t ≠ 0 ∨ f t ≠ ⊤) : ContinuousWithinAt (fun (x : X) => f x * g x) s t

theorem MeasureTheory.ContinuousWithinAt.ennrpow_const {α : Type u_1} [TopologicalSpace α] {f : α → ENNReal} {s : Set α} {x : α} {p : ℝ} (hf : ContinuousWithinAt f s x) : ContinuousWithinAt (fun (x : α) => f x ^ p) s x

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

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 μ