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
def
MeasureTheory.eLorentzNorm'
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
[ENorm ε]
(f : α → ε)
(p q : ENNReal)
(μ : Measure α)
:
The Lorentz seminorm of a function, for 0 < p < ∞
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
MeasureTheory.eLorentzNorm'_exponent_zero'
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
[ENorm ε]
{f : α → ε}
{μ : Measure α}
:
theorem
MeasureTheory.eLorentzNorm'_eq
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
{p q : ENNReal}
[ENorm ε]
(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}
{ε : Type u_2}
{m0 : MeasurableSpace α}
{p q : ENNReal}
[ENorm ε]
(p_nonzero : p ≠ 0)
(p_ne_top : p ≠ ⊤)
{f : α → ε}
{μ : Measure α}
:
theorem
MeasureTheory.eLorentzNorm'_eq_integral_distribution_rpow
{α : Type u_1}
{ε : Type u_2}
{p : ENNReal}
[ENorm ε]
{x✝ : MeasurableSpace α}
{f : α → ε}
{μ : Measure α}
:
def
MeasureTheory.eLorentzNorm
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
[ENorm ε]
(f : α → ε)
(p q : ENNReal)
(μ : Measure α)
:
The Lorentz seminorm of a function
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MeasureTheory.eLorentzNorm_eq_eLorentzNorm'
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
{p q : ENNReal}
[ENorm ε]
{μ : Measure α}
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
{f : α → ε}
:
theorem
MeasureTheory.eLorentzNorm_eq
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
{p q : ENNReal}
[ENorm ε]
{μ : Measure α}
(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)⁻¹)
@[simp]
theorem
MeasureTheory.eLorentzNorm_exponent_zero
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
{q : ENNReal}
[ENorm ε]
{μ : Measure α}
{f : α → ε}
:
@[simp]
theorem
MeasureTheory.eLorentzNorm_exponent_zero'
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
[ENorm ε]
{μ : Measure α}
{f : α → ε}
:
@[simp]
theorem
MeasureTheory.eLorentzNorm_exponent_top_top
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
[ENorm ε]
{μ : Measure α}
{f : α → ε}
:
theorem
MeasureTheory.eLorentzNorm_exponent_top'
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
{q : ENNReal}
[ENorm ε]
{μ : Measure α}
{f : α → ε}
(q_ne_zero : q ≠ 0)
(q_ne_top : q ≠ ⊤)
(hf : eLpNormEssSup f μ ≠ 0)
:
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 =ᶠ[ae μ] 0)
:
def
MeasureTheory.MemLorentz
{α : Type u_1}
{ε : Type u_2}
{m0 : MeasurableSpace α}
[ENorm ε]
[TopologicalSpace ε]
(f : α → ε)
(p r : ENNReal)
(μ : Measure α)
:
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.AEStronglyMeasurable f μ ∧ MeasureTheory.eLorentzNorm f p r μ < ⊤)
Instances For
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 μ)
:
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 μ