Documentation

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Density of simple functions #

Show that each Lᵖ Borel measurable function can be approximated in Lᵖ norm by a sequence of simple functions.

Main definitions #

Main results #

TODO #

For E finite-dimensional, simple functions α →ₛ E are dense in L^∞ -- prove this.

Notations #

Lp approximation by simple functions #

theorem MeasureTheory.SimpleFunc.nnnorm_approxOn_le {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] [OpensMeasurableSpace E] {f : βE} (hf : Measurable f) {s : Set E} {y₀ : E} (h₀ : y₀ s) [TopologicalSpace.SeparableSpace s] (x : β) (n : ) :
(approxOn f hf s y₀ h₀ n) x - f x‖₊ f x - y₀‖₊
theorem MeasureTheory.SimpleFunc.norm_approxOn_y₀_le {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] [OpensMeasurableSpace E] {f : βE} (hf : Measurable f) {s : Set E} {y₀ : E} (h₀ : y₀ s) [TopologicalSpace.SeparableSpace s] (x : β) (n : ) :
(approxOn f hf s y₀ h₀ n) x - y₀ f x - y₀ + f x - y₀
theorem MeasureTheory.SimpleFunc.norm_approxOn_zero_le {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] [OpensMeasurableSpace E] {f : βE} (hf : Measurable f) {s : Set E} (h₀ : 0 s) [TopologicalSpace.SeparableSpace s] (x : β) (n : ) :
(approxOn f hf s 0 h₀ n) x f x + f x
theorem MeasureTheory.SimpleFunc.tendsto_approxOn_Lp_eLpNorm {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] {p : ENNReal} [OpensMeasurableSpace E] {f : βE} (hf : Measurable f) {s : Set E} {y₀ : E} (h₀ : y₀ s) [TopologicalSpace.SeparableSpace s] (hp_ne_top : p ) {μ : Measure β} (hμ : ∀ᵐ (x : β) μ, f x closure s) (hi : eLpNorm (fun (x : β) => f x - y₀) p μ < ) :
Filter.Tendsto (fun (n : ) => eLpNorm ((approxOn f hf s y₀ h₀ n) - f) p μ) Filter.atTop (nhds 0)
theorem MeasureTheory.SimpleFunc.memLp_approxOn {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] {p : ENNReal} [BorelSpace E] {f : βE} {μ : Measure β} (fmeas : Measurable f) (hf : MemLp f p μ) {s : Set E} {y₀ : E} (h₀ : y₀ s) [TopologicalSpace.SeparableSpace s] (hi₀ : MemLp (fun (x : β) => y₀) p μ) (n : ) :
MemLp (⇑(approxOn f fmeas s y₀ h₀ n)) p μ
theorem MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp_eLpNorm {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] {p : ENNReal} [BorelSpace E] {f : βE} (hp_ne_top : p ) {μ : Measure β} (fmeas : Measurable f) [TopologicalSpace.SeparableSpace ↑(Set.range f {0})] (hf : eLpNorm f p μ < ) :
Filter.Tendsto (fun (n : ) => eLpNorm ((approxOn f fmeas (Set.range f {0}) 0 n) - f) p μ) Filter.atTop (nhds 0)
theorem MeasureTheory.SimpleFunc.memLp_approxOn_range {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] {p : ENNReal} [BorelSpace E] {f : βE} {μ : Measure β} (fmeas : Measurable f) [TopologicalSpace.SeparableSpace ↑(Set.range f {0})] (hf : MemLp f p μ) (n : ) :
MemLp (⇑(approxOn f fmeas (Set.range f {0}) 0 n)) p μ
theorem MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] {p : ENNReal} [BorelSpace E] {f : βE} [hp : Fact (1 p)] (hp_ne_top : p ) {μ : Measure β} (fmeas : Measurable f) [TopologicalSpace.SeparableSpace ↑(Set.range f {0})] (hf : MemLp f p μ) :
Filter.Tendsto (fun (n : ) => MemLp.toLp (approxOn f fmeas (Set.range f {0}) 0 n) ) Filter.atTop (nhds (MemLp.toLp f hf))
theorem MeasureTheory.MemLp.exists_simpleFunc_eLpNorm_sub_lt {β : Type u_2} [MeasurableSpace β] {p : ENNReal} {E : Type u_7} [NormedAddCommGroup E] {f : βE} {μ : Measure β} (hf : MemLp f p μ) (hp_ne_top : p ) {ε : ENNReal} (hε : ε 0) :
∃ (g : SimpleFunc β E), eLpNorm (f - g) p μ < ε MemLp (⇑g) p μ

Any function in ℒp can be approximated by a simple function if p < ∞.

L1 approximation by simple functions #

theorem MeasureTheory.SimpleFunc.tendsto_approxOn_L1_enorm {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] [OpensMeasurableSpace E] {f : βE} (hf : Measurable f) {s : Set E} {y₀ : E} (h₀ : y₀ s) [TopologicalSpace.SeparableSpace s] {μ : Measure β} (hμ : ∀ᵐ (x : β) μ, f x closure s) (hi : HasFiniteIntegral (fun (x : β) => f x - y₀) μ) :
Filter.Tendsto (fun (n : ) => ∫⁻ (x : β), (approxOn f hf s y₀ h₀ n) x - f x‖ₑ μ) Filter.atTop (nhds 0)
@[deprecated MeasureTheory.SimpleFunc.tendsto_approxOn_L1_enorm (since := "2025-01-21")]
theorem MeasureTheory.SimpleFunc.tendsto_approxOn_L1_nnnorm {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] [OpensMeasurableSpace E] {f : βE} (hf : Measurable f) {s : Set E} {y₀ : E} (h₀ : y₀ s) [TopologicalSpace.SeparableSpace s] {μ : Measure β} (hμ : ∀ᵐ (x : β) μ, f x closure s) (hi : HasFiniteIntegral (fun (x : β) => f x - y₀) μ) :
Filter.Tendsto (fun (n : ) => ∫⁻ (x : β), (approxOn f hf s y₀ h₀ n) x - f x‖ₑ μ) Filter.atTop (nhds 0)

Alias of MeasureTheory.SimpleFunc.tendsto_approxOn_L1_enorm.

theorem MeasureTheory.SimpleFunc.integrable_approxOn {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] [BorelSpace E] {f : βE} {μ : Measure β} (fmeas : Measurable f) (hf : Integrable f μ) {s : Set E} {y₀ : E} (h₀ : y₀ s) [TopologicalSpace.SeparableSpace s] (hi₀ : Integrable (fun (x : β) => y₀) μ) (n : ) :
Integrable (⇑(approxOn f fmeas s y₀ h₀ n)) μ
@[deprecated MeasureTheory.SimpleFunc.tendsto_approxOn_range_L1_enorm (since := "2025-01-21")]
theorem MeasureTheory.SimpleFunc.tendsto_approxOn_range_L1_nnnorm {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] [OpensMeasurableSpace E] {f : βE} {μ : Measure β} [TopologicalSpace.SeparableSpace ↑(Set.range f {0})] (fmeas : Measurable f) (hf : Integrable f μ) :
Filter.Tendsto (fun (n : ) => ∫⁻ (x : β), (approxOn f fmeas (Set.range f {0}) 0 n) x - f x‖ₑ μ) Filter.atTop (nhds 0)

Alias of MeasureTheory.SimpleFunc.tendsto_approxOn_range_L1_enorm.

theorem MeasureTheory.SimpleFunc.integrable_approxOn_range {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] [BorelSpace E] {f : βE} {μ : Measure β} (fmeas : Measurable f) [TopologicalSpace.SeparableSpace ↑(Set.range f {0})] (hf : Integrable f μ) (n : ) :
Integrable (⇑(approxOn f fmeas (Set.range f {0}) 0 n)) μ

Properties of simple functions in Lp spaces #

A simple function f : α →ₛ E into a normed group E verifies, for a measure μ:

theorem MeasureTheory.SimpleFunc.exists_forall_norm_le {α : Type u_1} {F : Type u_5} [MeasurableSpace α] [NormedAddCommGroup F] (f : SimpleFunc α F) :
∃ (C : ), ∀ (x : α), f x C
theorem MeasureTheory.SimpleFunc.memLp_zero {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (f : SimpleFunc α E) (μ : Measure α) :
MemLp (⇑f) 0 μ
theorem MeasureTheory.SimpleFunc.memLp_top {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (f : SimpleFunc α E) (μ : Measure α) :
MemLp f μ
theorem MeasureTheory.SimpleFunc.eLpNorm'_eq {α : Type u_1} {F : Type u_5} [MeasurableSpace α] [NormedAddCommGroup F] {p : } (f : SimpleFunc α F) (μ : Measure α) :
eLpNorm' (⇑f) p μ = (∑ yf.range, y‖ₑ ^ p * μ (f ⁻¹' {y})) ^ (1 / p)
theorem MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_memLp {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : Measure α} {p : ENNReal} (hp_pos : p 0) (hp_ne_top : p ) (f : SimpleFunc α E) (hf : MemLp (⇑f) p μ) (y : E) (hy_ne : y 0) :
μ (f ⁻¹' {y}) <
theorem MeasureTheory.SimpleFunc.memLp_of_finite_measure_preimage {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : Measure α} (p : ENNReal) {f : SimpleFunc α E} (hf : ∀ (y : E), y 0μ (f ⁻¹' {y}) < ) :
MemLp (⇑f) p μ
theorem MeasureTheory.SimpleFunc.memLp_iff {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : Measure α} {p : ENNReal} {f : SimpleFunc α E} (hp_pos : p 0) (hp_ne_top : p ) :
MemLp (⇑f) p μ ∀ (y : E), y 0μ (f ⁻¹' {y}) <
theorem MeasureTheory.SimpleFunc.integrable_iff {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : Measure α} {f : SimpleFunc α E} :
Integrable (⇑f) μ ∀ (y : E), y 0μ (f ⁻¹' {y}) <
theorem MeasureTheory.SimpleFunc.memLp_iff_integrable {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : Measure α} {p : ENNReal} {f : SimpleFunc α E} (hp_pos : p 0) (hp_ne_top : p ) :
MemLp (⇑f) p μ Integrable (⇑f) μ
theorem MeasureTheory.SimpleFunc.memLp_iff_finMeasSupp {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : Measure α} {p : ENNReal} {f : SimpleFunc α E} (hp_pos : p 0) (hp_ne_top : p ) :
MemLp (⇑f) p μ f.FinMeasSupp μ
theorem MeasureTheory.SimpleFunc.FinMeasSupp.integrable {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : Measure α} {f : SimpleFunc α E} (h : f.FinMeasSupp μ) :
Integrable (⇑f) μ
theorem MeasureTheory.SimpleFunc.integrable_pair {α : Type u_1} {E : Type u_4} {F : Type u_5} [MeasurableSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] {μ : Measure α} {f : SimpleFunc α E} {g : SimpleFunc α F} :
Integrable (⇑f) μIntegrable (⇑g) μIntegrable (⇑(f.pair g)) μ
theorem MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_integrable {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : Measure α} (f : SimpleFunc α E) (hf : Integrable (⇑f) μ) {x : E} (hx : x 0) :
μ (f ⁻¹' {x}) <
theorem MeasureTheory.SimpleFunc.measure_support_lt_top_of_memLp {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : Measure α} {p : ENNReal} (f : SimpleFunc α E) (hf : MemLp (⇑f) p μ) (hp_ne_zero : p 0) (hp_ne_top : p ) :
theorem MeasureTheory.SimpleFunc.measure_lt_top_of_memLp_indicator {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : Measure α} {p : ENNReal} (hp_pos : p 0) (hp_ne_top : p ) {c : E} (hc : c 0) {s : Set α} (hs : MeasurableSet s) (hcs : MemLp (⇑(piecewise s hs (const α c) (const α 0))) p μ) :
μ s <

Construction of the space of Lp simple functions, and its dense embedding into Lp.

def MeasureTheory.Lp.simpleFunc {α : Type u_1} (E : Type u_4) [MeasurableSpace α] [NormedAddCommGroup E] (p : ENNReal) (μ : Measure α) :
AddSubgroup (Lp E p μ)

Lp.simpleFunc is a subspace of Lp consisting of equivalence classes of an integrable simple function.

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

Simple functions in Lp space form a NormedSpace.

theorem MeasureTheory.Lp.simpleFunc.eq' {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} {f g : (simpleFunc E p μ)} :
f = gf = g

Implementation note: If Lp.simpleFunc E p μ were defined as a 𝕜-submodule of Lp E p μ, then the next few lemmas, putting a normed 𝕜-group structure on Lp.simpleFunc E p μ, would be unnecessary. But instead, Lp.simpleFunc E p μ is defined as an AddSubgroup of Lp E p μ, which does not permit this (but has the advantage of working when E itself is a normed group, i.e. has no scalar action).

def MeasureTheory.Lp.simpleFunc.smul {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] :
SMul 𝕜 (simpleFunc E p μ)

If E is a normed space, Lp.simpleFunc E p μ is a SMul. Not declared as an instance as it is (as of writing) used only in the construction of the Bochner integral.

Equations
@[simp]
theorem MeasureTheory.Lp.simpleFunc.coe_smul {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] (c : 𝕜) (f : (simpleFunc E p μ)) :
↑(c f) = c f
def MeasureTheory.Lp.simpleFunc.module {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] :
Module 𝕜 (simpleFunc E p μ)

If E is a normed space, Lp.simpleFunc E p μ is a module. Not declared as an instance as it is (as of writing) used only in the construction of the Bochner integral.

Equations
theorem MeasureTheory.Lp.simpleFunc.boundedSMul {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] [Fact (1 p)] :
BoundedSMul 𝕜 (simpleFunc E p μ)

If E is a normed space, Lp.simpleFunc E p μ is a normed space. Not declared as an instance as it is (as of writing) used only in the construction of the Bochner integral.

def MeasureTheory.Lp.simpleFunc.normedSpace {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} {𝕜 : Type u_7} [NormedField 𝕜] [NormedSpace 𝕜 E] [Fact (1 p)] :
NormedSpace 𝕜 (simpleFunc E p μ)

If E is a normed space, Lp.simpleFunc E p μ is a normed space. Not declared as an instance as it is (as of writing) used only in the construction of the Bochner integral.

Equations
@[reducible, inline]
abbrev MeasureTheory.Lp.simpleFunc.toLp {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (f : SimpleFunc α E) (hf : MemLp (⇑f) p μ) :
(simpleFunc E p μ)

Construct the equivalence class [f] of a simple function f satisfying MemLp.

Equations
theorem MeasureTheory.Lp.simpleFunc.toLp_eq_toLp {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (f : SimpleFunc α E) (hf : MemLp (⇑f) p μ) :
(toLp f hf) = MemLp.toLp (⇑f) hf
theorem MeasureTheory.Lp.simpleFunc.toLp_eq_mk {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (f : SimpleFunc α E) (hf : MemLp (⇑f) p μ) :
(toLp f hf) = AEEqFun.mk f
theorem MeasureTheory.Lp.simpleFunc.toLp_zero {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} :
toLp 0 = 0
theorem MeasureTheory.Lp.simpleFunc.toLp_add {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (f g : SimpleFunc α E) (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ) :
toLp (f + g) = toLp f hf + toLp g hg
theorem MeasureTheory.Lp.simpleFunc.toLp_neg {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (f : SimpleFunc α E) (hf : MemLp (⇑f) p μ) :
toLp (-f) = -toLp f hf
theorem MeasureTheory.Lp.simpleFunc.toLp_sub {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (f g : SimpleFunc α E) (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ) :
toLp (f - g) = toLp f hf - toLp g hg
theorem MeasureTheory.Lp.simpleFunc.toLp_smul {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] (f : SimpleFunc α E) (hf : MemLp (⇑f) p μ) (c : 𝕜) :
toLp (c f) = c toLp f hf
theorem MeasureTheory.Lp.simpleFunc.norm_toLp {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [Fact (1 p)] (f : SimpleFunc α E) (hf : MemLp (⇑f) p μ) :
toLp f hf = (eLpNorm (⇑f) p μ).toReal
theorem MeasureTheory.Lp.simpleFunc.measurable {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [MeasurableSpace E] (f : (simpleFunc E p μ)) :

(toSimpleFunc f) is measurable.

theorem MeasureTheory.Lp.simpleFunc.toSimpleFunc_eq_toFun {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (f : (simpleFunc E p μ)) :
(toSimpleFunc f) =ᶠ[ae μ] f
theorem MeasureTheory.Lp.simpleFunc.memLp {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (f : (simpleFunc E p μ)) :
MemLp (⇑(toSimpleFunc f)) p μ

toSimpleFunc f satisfies the predicate MemLp.

theorem MeasureTheory.Lp.simpleFunc.toLp_toSimpleFunc {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (f : (simpleFunc E p μ)) :
toLp (toSimpleFunc f) = f
theorem MeasureTheory.Lp.simpleFunc.toSimpleFunc_toLp {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (f : SimpleFunc α E) (hfi : MemLp (⇑f) p μ) :
(toSimpleFunc (toLp f hfi)) =ᶠ[ae μ] f
theorem MeasureTheory.Lp.simpleFunc.add_toSimpleFunc {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (f g : (simpleFunc E p μ)) :
(toSimpleFunc (f + g)) =ᶠ[ae μ] (toSimpleFunc f) + (toSimpleFunc g)
theorem MeasureTheory.Lp.simpleFunc.neg_toSimpleFunc {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (f : (simpleFunc E p μ)) :
theorem MeasureTheory.Lp.simpleFunc.sub_toSimpleFunc {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (f g : (simpleFunc E p μ)) :
(toSimpleFunc (f - g)) =ᶠ[ae μ] (toSimpleFunc f) - (toSimpleFunc g)
theorem MeasureTheory.Lp.simpleFunc.smul_toSimpleFunc {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] (k : 𝕜) (f : (simpleFunc E p μ)) :
(toSimpleFunc (k f)) =ᶠ[ae μ] k (toSimpleFunc f)
theorem MeasureTheory.Lp.simpleFunc.norm_toSimpleFunc {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [Fact (1 p)] (f : (simpleFunc E p μ)) :
def MeasureTheory.Lp.simpleFunc.indicatorConst {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (p : ENNReal) {μ : Measure α} {s : Set α} (hs : MeasurableSet s) (hμs : μ s ) (c : E) :
(simpleFunc E p μ)

The characteristic function of a finite-measure measurable set s, as an Lp simple function.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem MeasureTheory.Lp.simpleFunc.coe_indicatorConst {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} {s : Set α} (hs : MeasurableSet s) (hμs : μ s ) (c : E) :
(indicatorConst p hs hμs c) = indicatorConstLp p hs hμs c
theorem MeasureTheory.Lp.simpleFunc.toSimpleFunc_indicatorConst {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} {s : Set α} (hs : MeasurableSet s) (hμs : μ s ) (c : E) :
theorem MeasureTheory.Lp.simpleFunc.induction {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (hp_pos : p 0) (hp_ne_top : p ) {P : (simpleFunc E p μ)Prop} (h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ), P (indicatorConst p hs c)) (h_add : ∀ ⦃f g : SimpleFunc α E⦄ (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ), Disjoint (Function.support f) (Function.support g)P (toLp f hf)P (toLp g hg)P (toLp f hf + toLp g hg)) (f : (simpleFunc E p μ)) :
P f

To prove something for an arbitrary Lp simple function, with 0 < p < ∞, it suffices to show that the property holds for (multiples of) characteristic functions of finite-measure measurable sets and is closed under addition (of functions with disjoint support).

@[deprecated MeasureTheory.Lp.simpleFunc.isUniformEmbedding (since := "2024-10-01")]

Alias of MeasureTheory.Lp.simpleFunc.isUniformEmbedding.

@[deprecated MeasureTheory.Lp.simpleFunc.isUniformInducing (since := "2024-10-05")]

Alias of MeasureTheory.Lp.simpleFunc.isUniformInducing.

@[deprecated MeasureTheory.Lp.simpleFunc.isDenseEmbedding (since := "2024-09-30")]

Alias of MeasureTheory.Lp.simpleFunc.isDenseEmbedding.

theorem MeasureTheory.Lp.simpleFunc.denseRange {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [Fact (1 p)] (hp_ne_top : p ) :
theorem MeasureTheory.Lp.simpleFunc.dense {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [Fact (1 p)] (hp_ne_top : p ) :
Dense (simpleFunc E p μ)
def MeasureTheory.Lp.simpleFunc.coeToLp (α : Type u_1) (E : Type u_4) (𝕜 : Type u_6) [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [Fact (1 p)] [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] :
(simpleFunc E p μ) →L[𝕜] (Lp E p μ)

The embedding of Lp simple functions into Lp functions, as a continuous linear map.

Equations
theorem MeasureTheory.Lp.simpleFunc.coeFn_le {α : Type u_1} [MeasurableSpace α] {p : ENNReal} {μ : Measure α} {G : Type u_7} [NormedLatticeAddCommGroup G] (f g : (simpleFunc G p μ)) :
f ≤ᶠ[ae μ] g f g
theorem MeasureTheory.Lp.simpleFunc.coeFn_zero {α : Type u_1} [MeasurableSpace α] (p : ENNReal) (μ : Measure α) (G : Type u_7) [NormedLatticeAddCommGroup G] :
0 =ᶠ[ae μ] 0
theorem MeasureTheory.Lp.simpleFunc.coeFn_nonneg {α : Type u_1} [MeasurableSpace α] {p : ENNReal} {μ : Measure α} {G : Type u_7} [NormedLatticeAddCommGroup G] (f : (simpleFunc G p μ)) :
0 ≤ᶠ[ae μ] f 0 f
theorem MeasureTheory.Lp.simpleFunc.exists_simpleFunc_nonneg_ae_eq {α : Type u_1} [MeasurableSpace α] {p : ENNReal} {μ : Measure α} {G : Type u_7} [NormedLatticeAddCommGroup G] {f : (simpleFunc G p μ)} (hf : 0 f) :
∃ (f' : SimpleFunc α G), 0 f' f =ᶠ[ae μ] f'
def MeasureTheory.Lp.simpleFunc.coeSimpleFuncNonnegToLpNonneg {α : Type u_1} [MeasurableSpace α] (p : ENNReal) (μ : Measure α) (G : Type u_7) [NormedLatticeAddCommGroup G] :
{ g : (simpleFunc G p μ) // 0 g }{ g : (Lp G p μ) // 0 g }

Coercion from nonnegative simple functions of Lp to nonnegative functions of Lp.

Equations
theorem MeasureTheory.Lp.induction {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [_i : Fact (1 p)] (hp_ne_top : p ) (P : (Lp E p μ)Prop) (h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ), P (simpleFunc.indicatorConst p hs c)) (h_add : ∀ ⦃f g : αE⦄ (hf : MemLp f p μ) (hg : MemLp g p μ), Disjoint (Function.support f) (Function.support g)P (MemLp.toLp f hf)P (MemLp.toLp g hg)P (MemLp.toLp f hf + MemLp.toLp g hg)) (h_closed : IsClosed {f : (Lp E p μ) | P f}) (f : (Lp E p μ)) :
P f

To prove something for an arbitrary Lp function in a second countable Borel normed group, it suffices to show that

  • the property holds for (multiples of) characteristic functions;
  • is closed under addition;
  • the set of functions in Lp for which the property holds is closed.
theorem MeasureTheory.MemLp.induction {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [_i : Fact (1 p)] (hp_ne_top : p ) (P : (αE)Prop) (h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet sμ s < P (s.indicator fun (x : α) => c)) (h_add : ∀ ⦃f g : αE⦄, Disjoint (Function.support f) (Function.support g)MemLp f p μMemLp g p μP fP gP (f + g)) (h_closed : IsClosed {f : (Lp E p μ) | P f}) (h_ae : ∀ ⦃f g : αE⦄, f =ᶠ[ae μ] gMemLp f p μP fP g) ⦃f : αE :
MemLp f p μP f

To prove something for an arbitrary MemLp function in a second countable Borel normed group, it suffices to show that

  • the property holds for (multiples of) characteristic functions;
  • is closed under addition;
  • the set of functions in the Lᵖ space for which the property holds is closed.
  • the property is closed under the almost-everywhere equal relation.

It is possible to make the hypotheses in the induction steps a bit stronger, and such conditions can be added once we need them (for example in h_add it is only necessary to consider the sum of a simple function with a multiple of a characteristic function and that the intersection of their images is a subset of {0}).

theorem MeasureTheory.MemLp.induction_dense {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (hp_ne_top : p ) (P : (αE)Prop) (h0P : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet sμ s < ∀ {ε : ENNReal}, ε 0∃ (g : αE), eLpNorm (g - s.indicator fun (x : α) => c) p μ ε P g) (h1P : ∀ (f g : αE), P fP gP (f + g)) (h2P : ∀ (f : αE), P fAEStronglyMeasurable f μ) {f : αE} (hf : MemLp f p μ) {ε : ENNReal} (hε : ε 0) :
∃ (g : αE), eLpNorm (f - g) p μ ε P g

If a set of ae strongly measurable functions is stable under addition and approximates characteristic functions in ℒp, then it is dense in ℒp.

Lp.simpleFunc is a subspace of Lp consisting of equivalence classes of an integrable simple function.

Equations
  • One or more equations did not get rendered due to their size.
theorem MeasureTheory.L1.SimpleFunc.toLp_one_eq_toL1 {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : Measure α} (f : SimpleFunc α E) (hf : Integrable (⇑f) μ) :
(Lp.simpleFunc.toLp f ) = Integrable.toL1 (⇑f) hf
theorem MeasureTheory.Integrable.induction {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : Measure α} (P : (αE)Prop) (h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet sμ s < P (s.indicator fun (x : α) => c)) (h_add : ∀ ⦃f g : αE⦄, Disjoint (Function.support f) (Function.support g)Integrable f μIntegrable g μP fP gP (f + g)) (h_closed : IsClosed {f : (Lp E 1 μ) | P f}) (h_ae : ∀ ⦃f g : αE⦄, f =ᶠ[ae μ] gIntegrable f μP fP g) ⦃f : αE :
Integrable f μP f

To prove something for an arbitrary integrable function in a normed group, it suffices to show that

  • the property holds for (multiples of) characteristic functions;
  • is closed under addition;
  • the set of functions in the space for which the property holds is closed.
  • the property is closed under the almost-everywhere equal relation.

It is possible to make the hypotheses in the induction steps a bit stronger, and such conditions can be added once we need them (for example in h_add it is only necessary to consider the sum of a simple function with a multiple of a characteristic function and that the intersection of their images is a subset of {0}).