# 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 #

• MeasureTheory.Lp.simpleFunc, the type of Lp simple functions
• coeToLp, the embedding of Lp.simpleFunc E p μ into Lp E p μ

## Main results #

• tendsto_approxOn_Lp_snorm (Lᵖ convergence): If E is a NormedAddCommGroup and f is measurable and Memℒp (for p < ∞), then the simple functions SimpleFunc.approxOn f hf s 0 h₀ n may be considered as elements of Lp E p μ, and they tend in Lᵖ to f.
• Lp.simpleFunc.denseEmbedding: the embedding coeToLp of the Lp simple functions into Lp is dense.
• Lp.simpleFunc.induction, Lp.induction, Memℒp.induction, Integrable.induction: to prove a predicate for all elements of one of these classes of functions, it suffices to check that it behaves correctly on simple functions.

## TODO #

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

## Notations #

• α →ₛ β (local notation): the type of simple functions α → β.
• α →₁ₛ[μ] E: the type of L1 simple functions α → β.

### Lp approximation by simple functions #

theorem MeasureTheory.SimpleFunc.nnnorm_approxOn_le {β : Type u_2} {E : Type u_4} [] [] {f : βE} (hf : ) {s : Set E} {y₀ : E} (h₀ : y₀ s) (x : β) (n : ) :
(MeasureTheory.SimpleFunc.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} [] [] {f : βE} (hf : ) {s : Set E} {y₀ : E} (h₀ : y₀ s) (x : β) (n : ) :
(MeasureTheory.SimpleFunc.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} [] [] {f : βE} (hf : ) {s : Set E} (h₀ : 0 s) (x : β) (n : ) :
() x f x + f x
theorem MeasureTheory.SimpleFunc.tendsto_approxOn_Lp_snorm {β : Type u_2} {E : Type u_4} [] [] {p : ENNReal} {f : βE} (hf : ) {s : Set E} {y₀ : E} (h₀ : y₀ s) (hp_ne_top : p ) {μ : } (hμ : ∀ᵐ (x : β) ∂μ, f x ) (hi : MeasureTheory.snorm (fun (x : β) => f x - y₀) p μ < ) :
Filter.Tendsto (fun (n : ) => MeasureTheory.snorm ((MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) - f) p μ) Filter.atTop (nhds 0)
theorem MeasureTheory.SimpleFunc.memℒp_approxOn {β : Type u_2} {E : Type u_4} [] [] {p : ENNReal} [] {f : βE} {μ : } (fmeas : ) (hf : ) {s : Set E} {y₀ : E} (h₀ : y₀ s) (hi₀ : MeasureTheory.Memℒp (fun (x : β) => y₀) p μ) (n : ) :
theorem MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp_snorm {β : Type u_2} {E : Type u_4} [] [] {p : ENNReal} [] {f : βE} (hp_ne_top : p ) {μ : } (fmeas : ) [] (hf : < ) :
Filter.Tendsto (fun (n : ) => MeasureTheory.snorm ((MeasureTheory.SimpleFunc.approxOn f fmeas ( {0}) 0 n) - f) p μ) Filter.atTop (nhds 0)
theorem MeasureTheory.SimpleFunc.memℒp_approxOn_range {β : Type u_2} {E : Type u_4} [] [] {p : ENNReal} [] {f : βE} {μ : } (fmeas : ) [] (hf : ) (n : ) :
theorem MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp {β : Type u_2} {E : Type u_4} [] [] {p : ENNReal} [] {f : βE} [hp : Fact (1 p)] (hp_ne_top : p ) {μ : } (fmeas : ) [] (hf : ) :
Filter.Tendsto (fun (n : ) => MeasureTheory.Memℒp.toLp (MeasureTheory.SimpleFunc.approxOn f fmeas ( {0}) 0 n) ) Filter.atTop (nhds ())
theorem MeasureTheory.Memℒp.exists_simpleFunc_snorm_sub_lt {β : Type u_2} [] {p : ENNReal} {E : Type u_7} {f : βE} {μ : } (hf : ) (hp_ne_top : p ) {ε : ENNReal} (hε : ε 0) :
∃ (g : ), MeasureTheory.snorm (f - g) p μ < ε MeasureTheory.Memℒp (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_nnnorm {β : Type u_2} {E : Type u_4} [] [] {f : βE} (hf : ) {s : Set E} {y₀ : E} (h₀ : y₀ s) {μ : } (hμ : ∀ᵐ (x : β) ∂μ, f x ) (hi : MeasureTheory.HasFiniteIntegral (fun (x : β) => f x - y₀) μ) :
Filter.Tendsto (fun (n : ) => ∫⁻ (x : β), (MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x - f x‖₊μ) Filter.atTop (nhds 0)
theorem MeasureTheory.SimpleFunc.integrable_approxOn {β : Type u_2} {E : Type u_4} [] [] [] {f : βE} {μ : } (fmeas : ) (hf : ) {s : Set E} {y₀ : E} (h₀ : y₀ s) (hi₀ : MeasureTheory.Integrable (fun (x : β) => y₀) μ) (n : ) :
theorem MeasureTheory.SimpleFunc.tendsto_approxOn_range_L1_nnnorm {β : Type u_2} {E : Type u_4} [] [] {f : βE} {μ : } [] (fmeas : ) (hf : ) :
Filter.Tendsto (fun (n : ) => ∫⁻ (x : β), (MeasureTheory.SimpleFunc.approxOn f fmeas ( {0}) 0 n) x - f x‖₊μ) Filter.atTop (nhds 0)
theorem MeasureTheory.SimpleFunc.integrable_approxOn_range {β : Type u_2} {E : Type u_4} [] [] [] {f : βE} {μ : } (fmeas : ) [] (hf : ) (n : ) :

### Properties of simple functions in Lp spaces #

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

• Memℒp f 0 μ and Memℒp f ∞ μ, since f is a.e.-measurable and bounded,
• for 0 < p < ∞, Memℒp f p μ ↔ Integrable f μ ↔ f.FinMeasSupp μ ↔ ∀ y, y ≠ 0 → μ (f ⁻¹' {y}) < ∞.
theorem MeasureTheory.SimpleFunc.exists_forall_norm_le {α : Type u_1} {F : Type u_5} [] (f : ) :
∃ (C : ), ∀ (x : α), f x C
theorem MeasureTheory.SimpleFunc.memℒp_zero {α : Type u_1} {E : Type u_4} [] (f : ) (μ : ) :
theorem MeasureTheory.SimpleFunc.memℒp_top {α : Type u_1} {E : Type u_4} [] (f : ) (μ : ) :
theorem MeasureTheory.SimpleFunc.snorm'_eq {α : Type u_1} {F : Type u_5} [] {p : } (f : ) (μ : ) :
MeasureTheory.snorm' (f) p μ = (f.range.sum fun (y : F) => y‖₊ ^ p * μ (f ⁻¹' {y})) ^ (1 / p)
theorem MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_memℒp {α : Type u_1} {E : Type u_4} [] {μ : } {p : ENNReal} (hp_pos : p 0) (hp_ne_top : p ) (f : ) (hf : MeasureTheory.Memℒp (f) p μ) (y : E) (hy_ne : y 0) :
μ (f ⁻¹' {y}) <
theorem MeasureTheory.SimpleFunc.memℒp_of_finite_measure_preimage {α : Type u_1} {E : Type u_4} [] {μ : } (p : ENNReal) {f : } (hf : ∀ (y : E), y 0μ (f ⁻¹' {y}) < ) :
theorem MeasureTheory.SimpleFunc.memℒp_iff {α : Type u_1} {E : Type u_4} [] {μ : } {p : ENNReal} {f : } (hp_pos : p 0) (hp_ne_top : p ) :
MeasureTheory.Memℒp (f) p μ ∀ (y : E), y 0μ (f ⁻¹' {y}) <
theorem MeasureTheory.SimpleFunc.integrable_iff {α : Type u_1} {E : Type u_4} [] {μ : } {f : } :
∀ (y : E), y 0μ (f ⁻¹' {y}) <
theorem MeasureTheory.SimpleFunc.memℒp_iff_integrable {α : Type u_1} {E : Type u_4} [] {μ : } {p : ENNReal} {f : } (hp_pos : p 0) (hp_ne_top : p ) :
theorem MeasureTheory.SimpleFunc.memℒp_iff_finMeasSupp {α : Type u_1} {E : Type u_4} [] {μ : } {p : ENNReal} {f : } (hp_pos : p 0) (hp_ne_top : p ) :
MeasureTheory.Memℒp (f) p μ f.FinMeasSupp μ
theorem MeasureTheory.SimpleFunc.integrable_iff_finMeasSupp {α : Type u_1} {E : Type u_4} [] {μ : } {f : } :
f.FinMeasSupp μ
theorem MeasureTheory.SimpleFunc.FinMeasSupp.integrable {α : Type u_1} {E : Type u_4} [] {μ : } {f : } (h : f.FinMeasSupp μ) :
theorem MeasureTheory.SimpleFunc.integrable_pair {α : Type u_1} {E : Type u_4} {F : Type u_5} [] {μ : } {f : } {g : } :
MeasureTheory.Integrable ((f.pair g)) μ
theorem MeasureTheory.SimpleFunc.memℒp_of_isFiniteMeasure {α : Type u_1} {E : Type u_4} [] (f : ) (p : ENNReal) (μ : ) :
theorem MeasureTheory.SimpleFunc.integrable_of_isFiniteMeasure {α : Type u_1} {E : Type u_4} [] {μ : } (f : ) :
theorem MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_integrable {α : Type u_1} {E : Type u_4} [] {μ : } (f : ) (hf : ) {x : E} (hx : x 0) :
μ (f ⁻¹' {x}) <
theorem MeasureTheory.SimpleFunc.measure_support_lt_top {α : Type u_1} {β : Type u_2} [] {μ : } [Zero β] (f : ) (hf : ∀ (y : β), y 0μ (f ⁻¹' {y}) < ) :
μ () <
theorem MeasureTheory.SimpleFunc.measure_support_lt_top_of_memℒp {α : Type u_1} {E : Type u_4} [] {μ : } {p : ENNReal} (f : ) (hf : MeasureTheory.Memℒp (f) p μ) (hp_ne_zero : p 0) (hp_ne_top : p ) :
μ () <
theorem MeasureTheory.SimpleFunc.measure_support_lt_top_of_integrable {α : Type u_1} {E : Type u_4} [] {μ : } (f : ) (hf : ) :
μ () <
theorem MeasureTheory.SimpleFunc.measure_lt_top_of_memℒp_indicator {α : Type u_1} {E : Type u_4} [] {μ : } {p : ENNReal} (hp_pos : p 0) (hp_ne_top : p ) {c : E} (hc : c 0) {s : Set α} (hs : ) (hcs : ) :
μ 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) [] (p : ENNReal) (μ : ) :

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.
Instances For

Simple functions in Lp space form a NormedSpace.

theorem MeasureTheory.Lp.simpleFunc.eq' {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } {f : ()} {g : ()} :
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} [] {p : ENNReal} {μ : } [] [Module 𝕜 E] [] :
SMul 𝕜 ()

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
• MeasureTheory.Lp.simpleFunc.smul = { smul := fun (k : 𝕜) (f : ()) => k f, }
Instances For
@[simp]
theorem MeasureTheory.Lp.simpleFunc.coe_smul {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [] {p : ENNReal} {μ : } [] [Module 𝕜 E] [] (c : 𝕜) (f : ()) :
(c f) = c f
def MeasureTheory.Lp.simpleFunc.module {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [] {p : ENNReal} {μ : } [] [Module 𝕜 E] [] :
Module 𝕜 ()

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
• MeasureTheory.Lp.simpleFunc.module =
Instances For
theorem MeasureTheory.Lp.simpleFunc.boundedSMul {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [] {p : ENNReal} {μ : } [] [Module 𝕜 E] [] [Fact (1 p)] :
BoundedSMul 𝕜 ()

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} [] {p : ENNReal} {μ : } {𝕜 : Type u_7} [] [] [Fact (1 p)] :
NormedSpace 𝕜 ()

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
• MeasureTheory.Lp.simpleFunc.normedSpace =
Instances For
@[reducible, inline]
abbrev MeasureTheory.Lp.simpleFunc.toLp {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } (f : ) (hf : MeasureTheory.Memℒp (f) p μ) :
()

Construct the equivalence class [f] of a simple function f satisfying Memℒp.

Equations
Instances For
theorem MeasureTheory.Lp.simpleFunc.toLp_eq_toLp {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } (f : ) (hf : MeasureTheory.Memℒp (f) p μ) :
theorem MeasureTheory.Lp.simpleFunc.toLp_eq_mk {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } (f : ) (hf : MeasureTheory.Memℒp (f) p μ) :
theorem MeasureTheory.Lp.simpleFunc.toLp_zero {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } :
theorem MeasureTheory.Lp.simpleFunc.toLp_add {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } (f : ) (g : ) (hf : MeasureTheory.Memℒp (f) p μ) (hg : MeasureTheory.Memℒp (g) p μ) :
theorem MeasureTheory.Lp.simpleFunc.toLp_neg {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } (f : ) (hf : MeasureTheory.Memℒp (f) p μ) :
theorem MeasureTheory.Lp.simpleFunc.toLp_sub {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } (f : ) (g : ) (hf : MeasureTheory.Memℒp (f) p μ) (hg : MeasureTheory.Memℒp (g) p μ) :
theorem MeasureTheory.Lp.simpleFunc.toLp_smul {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [] {p : ENNReal} {μ : } [] [Module 𝕜 E] [] (f : ) (hf : MeasureTheory.Memℒp (f) p μ) (c : 𝕜) :
=
theorem MeasureTheory.Lp.simpleFunc.norm_toLp {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } [Fact (1 p)] (f : ) (hf : MeasureTheory.Memℒp (f) p μ) :
= (MeasureTheory.snorm (f) p μ).toReal
def MeasureTheory.Lp.simpleFunc.toSimpleFunc {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } (f : ()) :

Find a representative of a Lp.simpleFunc.

Equations
Instances For
theorem MeasureTheory.Lp.simpleFunc.measurable {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } [] (f : ()) :

(toSimpleFunc f) is measurable.

theorem MeasureTheory.Lp.simpleFunc.stronglyMeasurable {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } (f : ()) :
theorem MeasureTheory.Lp.simpleFunc.aemeasurable {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } [] (f : ()) :
theorem MeasureTheory.Lp.simpleFunc.aestronglyMeasurable {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } (f : ()) :
theorem MeasureTheory.Lp.simpleFunc.toSimpleFunc_eq_toFun {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } (f : ()) :
μ.ae.EventuallyEq f
theorem MeasureTheory.Lp.simpleFunc.memℒp {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } (f : ()) :

toSimpleFunc f satisfies the predicate Memℒp.

theorem MeasureTheory.Lp.simpleFunc.toLp_toSimpleFunc {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } (f : ()) :
theorem MeasureTheory.Lp.simpleFunc.toSimpleFunc_toLp {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } (f : ) (hfi : MeasureTheory.Memℒp (f) p μ) :
μ.ae.EventuallyEq f
theorem MeasureTheory.Lp.simpleFunc.zero_toSimpleFunc {α : Type u_1} (E : Type u_4) [] {p : ENNReal} (μ : ) :
μ.ae.EventuallyEq 0
theorem MeasureTheory.Lp.simpleFunc.add_toSimpleFunc {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } (f : ()) (g : ()) :
μ.ae.EventuallyEq ()
theorem MeasureTheory.Lp.simpleFunc.neg_toSimpleFunc {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } (f : ()) :
μ.ae.EventuallyEq
theorem MeasureTheory.Lp.simpleFunc.sub_toSimpleFunc {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } (f : ()) (g : ()) :
μ.ae.EventuallyEq ()
theorem MeasureTheory.Lp.simpleFunc.smul_toSimpleFunc {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [] {p : ENNReal} {μ : } [] [Module 𝕜 E] [] (k : 𝕜) (f : ()) :
μ.ae.EventuallyEq ()
theorem MeasureTheory.Lp.simpleFunc.norm_toSimpleFunc {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } [Fact (1 p)] (f : ()) :
f = .toReal
def MeasureTheory.Lp.simpleFunc.indicatorConst {α : Type u_1} {E : Type u_4} [] (p : ENNReal) {μ : } {s : Set α} (hs : ) (hμs : μ s ) (c : E) :
()

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.
Instances For
@[simp]
theorem MeasureTheory.Lp.simpleFunc.coe_indicatorConst {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } {s : Set α} (hs : ) (hμs : μ s ) (c : E) :
() =
theorem MeasureTheory.Lp.simpleFunc.toSimpleFunc_indicatorConst {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } {s : Set α} (hs : ) (hμs : μ s ) (c : E) :
μ.ae.EventuallyEq
theorem MeasureTheory.Lp.simpleFunc.induction {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } (hp_pos : p 0) (hp_ne_top : p ) {P : ()Prop} (h_ind : ∀ (c : E) {s : Set α} (hs : ) (hμs : μ s < ), P ()) (h_add : ∀ ⦃f g : ⦄ (hf : MeasureTheory.Memℒp (f) p μ) (hg : MeasureTheory.Memℒp (g) p μ), Disjoint () ()P P ) (f : ()) :
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).

theorem MeasureTheory.Lp.simpleFunc.uniformContinuous {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } [Fact (1 p)] :
UniformContinuous Subtype.val
theorem MeasureTheory.Lp.simpleFunc.uniformEmbedding {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } [Fact (1 p)] :
UniformEmbedding Subtype.val
theorem MeasureTheory.Lp.simpleFunc.uniformInducing {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } [Fact (1 p)] :
UniformInducing Subtype.val
theorem MeasureTheory.Lp.simpleFunc.denseEmbedding {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } [Fact (1 p)] (hp_ne_top : p ) :
DenseEmbedding Subtype.val
theorem MeasureTheory.Lp.simpleFunc.denseInducing {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } [Fact (1 p)] (hp_ne_top : p ) :
DenseInducing Subtype.val
theorem MeasureTheory.Lp.simpleFunc.denseRange {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } [Fact (1 p)] (hp_ne_top : p ) :
DenseRange Subtype.val
def MeasureTheory.Lp.simpleFunc.coeToLp (α : Type u_1) (E : Type u_4) (𝕜 : Type u_6) [] {p : ENNReal} {μ : } [Fact (1 p)] [] [Module 𝕜 E] [] :
() →L[𝕜] ()

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

Equations
• = let __src := ().subtype; { toFun := __src.toFun, map_add' := , map_smul' := , cont := }
Instances For
theorem MeasureTheory.Lp.simpleFunc.coeFn_le {α : Type u_1} [] {p : ENNReal} {μ : } {G : Type u_7} (f : ()) (g : ()) :
μ.ae.EventuallyLE f g f g
instance MeasureTheory.Lp.simpleFunc.instCovariantClassLE {α : Type u_1} [] {p : ENNReal} {μ : } {G : Type u_7} :
CovariantClass (()) (()) (fun (x x_1 : ()) => x + x_1) fun (x x_1 : ()) => x x_1
Equations
• =
theorem MeasureTheory.Lp.simpleFunc.coeFn_zero {α : Type u_1} [] (p : ENNReal) (μ : ) (G : Type u_7) :
μ.ae.EventuallyEq (0) 0
theorem MeasureTheory.Lp.simpleFunc.coeFn_nonneg {α : Type u_1} [] {p : ENNReal} {μ : } {G : Type u_7} (f : ()) :
μ.ae.EventuallyLE 0 f 0 f
theorem MeasureTheory.Lp.simpleFunc.exists_simpleFunc_nonneg_ae_eq {α : Type u_1} [] {p : ENNReal} {μ : } {G : Type u_7} {f : ()} (hf : 0 f) :
∃ (f' : ), 0 f' μ.ae.EventuallyEq f f'
def MeasureTheory.Lp.simpleFunc.coeSimpleFuncNonnegToLpNonneg {α : Type u_1} [] (p : ENNReal) (μ : ) (G : Type u_7) :
{ g : () // 0 g }{ g : () // 0 g }

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

Equations
• = g,
Instances For
theorem MeasureTheory.Lp.simpleFunc.denseRange_coeSimpleFuncNonnegToLpNonneg {α : Type u_1} [] (p : ENNReal) (μ : ) (G : Type u_7) [hp : Fact (1 p)] (hp_ne_top : p ) :
theorem MeasureTheory.Lp.induction {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } [_i : Fact (1 p)] (hp_ne_top : p ) (P : ()Prop) (h_ind : ∀ (c : E) {s : Set α} (hs : ) (hμs : μ s < ), P ()) (h_add : ∀ ⦃f g : αE⦄ (hf : ) (hg : ), P ()P ()P ()) (h_closed : IsClosed {f : () | P f}) (f : ()) :
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;
• the set of functions in Lp for which the property holds is closed.
theorem MeasureTheory.Memℒp.induction {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } [_i : Fact (1 p)] (hp_ne_top : p ) (P : (αE)Prop) (h_ind : ∀ (c : E) ⦃s : Set α⦄, μ s < P (s.indicator fun (x : α) => c)) (h_add : ∀ ⦃f g : αE⦄, P fP gP (f + g)) (h_closed : IsClosed {f : () | P f}) (h_ae : ∀ ⦃f g : αE⦄, μ.ae.EventuallyEq f gP fP g) ⦃f : αE :
P f

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

• the property holds for (multiples of) characteristic functions;
• 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.Memℒp.induction_dense {α : Type u_1} {E : Type u_4} [] {p : ENNReal} {μ : } (hp_ne_top : p ) (P : (αE)Prop) (h0P : ∀ (c : E) ⦃s : Set α⦄, μ s < ∀ {ε : ENNReal}, ε 0∃ (g : αE), MeasureTheory.snorm (g - s.indicator fun (x : α) => c) p μ ε P g) (h1P : ∀ (f g : αE), P fP gP (f + g)) (h2P : ∀ (f : αE), ) {f : αE} (hf : ) {ε : ENNReal} (hε : ε 0) :
∃ (g : αE), MeasureTheory.snorm (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.
Instances For
theorem MeasureTheory.L1.SimpleFunc.toLp_one_eq_toL1 {α : Type u_1} {E : Type u_4} [] {μ : } (f : ) (hf : ) :
theorem MeasureTheory.L1.SimpleFunc.integrable {α : Type u_1} {E : Type u_4} [] {μ : } (f : ()) :
theorem MeasureTheory.Integrable.induction {α : Type u_1} {E : Type u_4} [] {μ : } (P : (αE)Prop) (h_ind : ∀ (c : E) ⦃s : Set α⦄, μ s < P (s.indicator fun (x : α) => c)) (h_add : ∀ ⦃f g : αE⦄, P fP gP (f + g)) (h_closed : IsClosed {f : () | P f}) (h_ae : ∀ ⦃f g : αE⦄, μ.ae.EventuallyEq f gP fP g) ⦃f : αE :
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;
• the set of functions in the L¹ space for which the property holds is closed.
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}).