Modular functionals and perturbations of Nakano spaces

ITAI BEN-YAACOV

defines L₀(X,𝓑,μ) to be the space of measurable functions f:X→ℝ up to a.e. equality.

Here we define that and give an example.

Note that the Lp seminorm MeasureTheory.eLpNorm is equal to 0 for p=0.

def L₀ {X : Type u_1} : {x : MeasureTheory.MeasureSpace X} → AddSubgroup (X →ₘ[MeasureTheory.volume] ℝ)

Equations

• L₀ = MeasureTheory.Lp ℝ 0 MeasureTheory.volume

def constant_ae (c : NNReal) : ℝ →ₘ[MeasureTheory.volume] ℝ

Equations

• constant_ae c = MeasureTheory.AEEqFun.mk (fun (x : ℝ) => ↑c) ⋯

def c₀ : ℝ →ₘ[MeasureTheory.volume] ℝ

Equations

• c₀ = constant_ae 0

def c₁ : ℝ →ₘ[MeasureTheory.volume] ℝ

Equations

• c₁ = constant_ae 1