Lorentz space

This file describes properties of almost everywhere strongly measurable functions with finite (p,q)-seminorm, denoted by eLorentzNorm f p q μ.

The Prop-valued MemLorentz f p q μ states that a function f : α → ε has finite (p,q)-seminorm and is almost everywhere strongly measurable.

Main definitions

• TODO

noncomputable def MeasureTheory.eLorentzNorm' {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [ENorm ε] (f : α → ε) (p q : ENNReal) (μ : Measure α) : ENNReal

The Lorentz seminorm of a function, for 0 < p < ∞

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MeasureTheory.eLorentzNorm'_exponent_zero' {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} [ENorm ε] {f : α → ε} {μ : Measure α} : eLorentzNorm' f p 0 μ = 0

theorem MeasureTheory.eLorentzNorm'_eq_integral_distribution_rpow {α : Type u_1} {ε : Type u_2} {p : ENNReal} [ENorm ε] {x✝ : MeasurableSpace α} {f : α → ε} {μ : Measure α} : eLorentzNorm' f p 1 μ = p * ∫⁻ (t : NNReal), distribution f (↑t) μ ^ p.toReal⁻¹

theorem MeasureTheory.eLorentzNorm'_exponent_top {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} [ENorm ε] {f : α → ε} {μ : Measure α} : eLorentzNorm' f p ⊤ μ = ⨆ (t : NNReal), ↑t * distribution f (↑t) μ ^ p.toReal⁻¹

theorem MeasureTheory.iSup_mul_distribution_rpow_eq_iSup_rpow_mul_rearrangement {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [ENorm ε] {p : ℝ} (hp : 0 < p) {f : α → ε} {μ : Measure α} : ⨆ (t : NNReal), ↑t * distribution f (↑t) μ ^ p⁻¹ = ⨆ (t : NNReal), ↑t ^ p⁻¹ * rearrangement f (↑t) μ

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

noncomputable def MeasureTheory.eLorentzNorm {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [ENorm ε] [TopologicalSpace ε] (f : α → ε) (p q : ENNReal) (μ : Measure α) : ENNReal

The Lorentz seminorm of a function

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.eLorentzNorm_of_not_aestronglyMeasurable {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [ENorm ε] {μ : Measure α} [TopologicalSpace ε] {f : α → ε} {p q : ENNReal} (h : ¬AEStronglyMeasurable f μ) : eLorentzNorm f p q μ = ⊤

theorem MeasureTheory.aestronglyMeasurable_of_eLorentzNorm_ne_top {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [ENorm ε] {μ : Measure α} [TopologicalSpace ε] {f : α → ε} {p q : ENNReal} (h : eLorentzNorm f p q μ ≠ ⊤) : AEStronglyMeasurable f μ

theorem MeasureTheory.eLorentzNorm_eq_eLorentzNorm' {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p q : ENNReal} [ENorm ε] {μ : Measure α} [TopologicalSpace ε] (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) {f : α → ε} (hf : AEStronglyMeasurable f μ) : eLorentzNorm f p q μ = eLorentzNorm' f p q μ

@[simp]

theorem MeasureTheory.eLorentzNorm_exponent_zero {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {q : ENNReal} [ENorm ε] {μ : Measure α} [TopologicalSpace ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) : eLorentzNorm f 0 q μ = 0

@[simp]

theorem MeasureTheory.eLorentzNorm_exponent_zero' {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} [ENorm ε] {μ : Measure α} [TopologicalSpace ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) : eLorentzNorm f p 0 μ = 0

@[simp]

theorem MeasureTheory.eLorentzNorm_exponent_top_top {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [ENorm ε] {μ : Measure α} [TopologicalSpace ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) : eLorentzNorm f ⊤ ⊤ μ = eLpNormEssSup f μ

theorem MeasureTheory.eLorentzNorm_exponent_top' {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {q : ENNReal} [ENorm ε] {μ : Measure α} [TopologicalSpace ε] {f : α → ε} (q_ne_zero : q ≠ 0) (q_ne_top : q ≠ ⊤) (hf : eLpNormEssSup f μ ≠ 0) : eLorentzNorm f ⊤ q μ = ⊤

theorem MeasureTheory.eLorentzNorm_exponent_top {α : Type u_1} {m0 : MeasurableSpace α} {q : ENNReal} {μ : Measure α} {ε : Type u_4} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε} (q_ne_zero : q ≠ 0) (q_ne_top : q ≠ ⊤) (hf : ¬f =ᵐ[μ] 0) : eLorentzNorm f ⊤ q μ = ⊤

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

def MeasureTheory.MemLorentz {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [ENorm ε] [TopologicalSpace ε] (f : α → ε) (p r : ENNReal) (μ : Measure α) : Prop

A function is in the Lorentz space L^{p,q} if it is (strongly a.e.)-measurable and has finite Lorentz seminorm.

Equations

• MeasureTheory.MemLorentz f p r μ = (MeasureTheory.eLorentzNorm f p r μ < ⊤)

theorem MeasureTheory.memLorentz_iff {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p q : ENNReal} [ENorm ε] {μ : Measure α} [TopologicalSpace ε] {f : α → ε} : MemLorentz f p q μ ↔ eLorentzNorm f p q μ < ⊤

theorem MeasureTheory.MemLorentz.aestronglyMeasurable {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {q : ENNReal} [ENorm ε] {μ : Measure α} [TopologicalSpace ε] {f : α → ε} {p : ENNReal} (h : MemLorentz f p q μ) : AEStronglyMeasurable f μ

theorem MeasureTheory.MemLorentz.aemeasurable {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {q : ENNReal} [ENorm ε] {μ : Measure α} [MeasurableSpace ε] [TopologicalSpace ε] [TopologicalSpace.PseudoMetrizableSpace ε] [BorelSpace ε] {f : α → ε} {p : ENNReal} (hf : MemLorentz f p q μ) : AEMeasurable f μ