ℒp space

This file describes properties of almost everywhere strongly measurable functions with finite p-seminorm, denoted by eLpNorm f p μ and defined for p:ℝ≥0∞ as 0 if p=0, (∫ ‖f a‖^p ∂μ) ^ (1/p) for 0 < p < ∞ and essSup ‖f‖ μ for p=∞.

The Prop-valued MemLp f p μ states that a function f : α → E has finite p-seminorm and is almost everywhere strongly measurable.

Main definitions

• eLpNorm' f p μ : (∫ ‖f a‖^p ∂μ) ^ (1/p) for f : α → F and p : ℝ, where α is a measurable space and F is a normed group.

• eLpNormEssSup f μ : seminorm in ℒ∞, equal to the essential supremum essSup ‖f‖ μ.

• eLpNorm f p μ : for p : ℝ≥0∞, seminorm in ℒp, equal to 0 for p=0, to eLpNorm' f p μ for 0 < p < ∞ and to eLpNormEssSup f μ for p = ∞.

• MemLp f p μ : property that the function f is almost everywhere strongly measurable and has finite p-seminorm for the measure μ (eLpNorm f p μ < ∞)

ℒp seminorm

We define the ℒp seminorm, denoted by eLpNorm f p μ. For real p, it is given by an integral formula (for which we use the notation eLpNorm' f p μ), and for p = ∞ it is the essential supremum (for which we use the notation eLpNormEssSup f μ).

We also define a predicate MemLp f p μ, requesting that a function is almost everywhere measurable and has finite eLpNorm f p μ.

This paragraph is devoted to the basic properties of these definitions. It is constructed as follows: for a given property, we prove it for eLpNorm' and eLpNormEssSup when it makes sense, deduce it for eLpNorm, and translate it in terms of MemLp.

def MeasureTheory.eLpNorm' {α : Type u_1} {ε : Type u_2} [ENorm ε] {x✝ : MeasurableSpace α} (f : α → ε) (q : ℝ) (μ : Measure α) : ENNReal

(∫ ‖f a‖^q ∂μ) ^ (1/q), which is a seminorm on the space of measurable functions for which this quantity is finite.

Note: this is a purely auxiliary quantity; lemmas about eLpNorm' should only be used to prove results about eLpNorm; every eLpNorm' lemma should have a eLpNorm' version.

Equations

• MeasureTheory.eLpNorm' f q μ = (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q)

theorem MeasureTheory.eLpNorm'_eq_lintegral_enorm {α : Type u_1} {ε : Type u_2} [ENorm ε] {x✝ : MeasurableSpace α} (f : α → ε) (q : ℝ) (μ : Measure α) : eLpNorm' f q μ = (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q)

def MeasureTheory.eLpNormEssSup {α : Type u_1} {ε : Type u_2} [ENorm ε] {x✝ : MeasurableSpace α} (f : α → ε) (μ : Measure α) : ENNReal

seminorm for ℒ∞, equal to the essential supremum of ‖f‖.

Equations

• MeasureTheory.eLpNormEssSup f μ = essSup (fun (x : α) => ‖f x‖ₑ) μ

theorem MeasureTheory.eLpNormEssSup_eq_essSup_enorm {α : Type u_1} {ε : Type u_2} [ENorm ε] {x✝ : MeasurableSpace α} (f : α → ε) (μ : Measure α) : eLpNormEssSup f μ = essSup (fun (x : α) => ‖f x‖ₑ) μ

def MeasureTheory.eLpNorm {α : Type u_1} {ε : Type u_2} [ENorm ε] {x✝ : MeasurableSpace α} (f : α → ε) (p : ENNReal) (μ : Measure α := by volume_tac) : ENNReal

ℒp seminorm, equal to 0 for p=0, to (∫ ‖f a‖^p ∂μ) ^ (1/p) for 0 < p < ∞ and to essSup ‖f‖ μ for p = ∞.

Equations

• MeasureTheory.eLpNorm f p μ = if p = 0 then 0 else if p = ⊤ then MeasureTheory.eLpNormEssSup f μ else MeasureTheory.eLpNorm' f p.toReal μ

theorem MeasureTheory.eLpNorm_eq_eLpNorm' {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} [ENorm ε] {μ : Measure α} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) {f : α → ε} : eLpNorm f p μ = eLpNorm' f p.toReal μ

theorem MeasureTheory.eLpNorm_nnreal_eq_eLpNorm' {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [ENorm ε] {μ : Measure α} {f : α → ε} {p : NNReal} (hp : p ≠ 0) : eLpNorm f (↑p) μ = eLpNorm' f (↑p) μ

theorem MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} [ENorm ε] {μ : Measure α} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) {f : α → ε} : eLpNorm f p μ = (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

theorem MeasureTheory.eLpNorm_nnreal_eq_lintegral {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [ENorm ε] {μ : Measure α} {f : α → ε} {p : NNReal} (hp : p ≠ 0) : eLpNorm f (↑p) μ = (∫⁻ (x : α), ‖f x‖ₑ ^ ↑p ∂μ) ^ (1 / ↑p)

theorem MeasureTheory.eLpNorm_one_eq_lintegral_enorm {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [ENorm ε] {μ : Measure α} {f : α → ε} : eLpNorm f 1 μ = ∫⁻ (x : α), ‖f x‖ₑ ∂μ

@[simp]

theorem MeasureTheory.eLpNorm_exponent_top {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [ENorm ε] {μ : Measure α} {f : α → ε} : eLpNorm f ⊤ μ = eLpNormEssSup f μ

def MeasureTheory.MemLp {ε : Type u_2} [ENorm ε] {α : Type u_7} {x✝ : MeasurableSpace α} [TopologicalSpace ε] (f : α → ε) (p : ENNReal) (μ : Measure α := by volume_tac) : Prop

The property that f : α → E is a.e. strongly measurable and (∫ ‖f a‖ ^ p ∂μ) ^ (1/p) is finite if p < ∞, or essSup ‖f‖ < ∞ if p = ∞.

Equations

• MeasureTheory.MemLp f p μ = (MeasureTheory.AEStronglyMeasurable f μ ∧ MeasureTheory.eLpNorm f p μ < ⊤)

@[deprecated MeasureTheory.MemLp (since := "2025-02-21")]

def MeasureTheory.Memℒp {ε : Type u_2} [ENorm ε] {α : Type u_7} {x✝ : MeasurableSpace α} [TopologicalSpace ε] (f : α → ε) (p : ENNReal) (μ : Measure α := by volume_tac) : Prop

Alias of MeasureTheory.MemLp.

---

The property that f : α → E is a.e. strongly measurable and (∫ ‖f a‖ ^ p ∂μ) ^ (1/p) is finite if p < ∞, or essSup ‖f‖ < ∞ if p = ∞.

Equations

• @MeasureTheory.Memℒp = @MeasureTheory.MemLp

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

@[deprecated MeasureTheory.MemLp.aestronglyMeasurable (since := "2025-02-21")]

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

Alias of MeasureTheory.MemLp.aestronglyMeasurable.

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

theorem MeasureTheory.lintegral_rpow_enorm_eq_rpow_eLpNorm' {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {q : ℝ} [ENorm ε] {μ : Measure α} {f : α → ε} (hq0_lt : 0 < q) : ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ = eLpNorm' f q μ ^ q

theorem MeasureTheory.eLpNorm_nnreal_pow_eq_lintegral {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [ENorm ε] {μ : Measure α} {f : α → ε} {p : NNReal} (hp : p ≠ 0) : eLpNorm f (↑p) μ ^ ↑p = ∫⁻ (x : α), ‖f x‖ₑ ^ ↑p ∂μ