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_eLpNorm (Lᵖ convergence): If E is a NormedAddCommGroup and f is measurable and MemLp (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.isDenseEmbedding: the embedding coeToLp of the Lp simple functions into Lp is dense.
• Lp.simpleFunc.induction, Lp.induction, MemLp.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.

Notation

• α →ₛ β (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} [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)

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)) μ

theorem MeasureTheory.SimpleFunc.tendsto_approxOn_range_L1_enorm {β : 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)

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 μ:

• MemLp f 0 μ and MemLp f ∞ μ, since f is a.e.-measurable and bounded,
• for 0 < p < ∞, MemLp 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} [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 μ = (∑ y ∈ f.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.integrable_iff_finMeasSupp {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : Measure α} {f : SimpleFunc α E} : Integrable (⇑f) μ ↔ 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.memLp_of_isFiniteMeasure {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (f : SimpleFunc α E) (p : ENNReal) (μ : Measure α) [IsFiniteMeasure μ] : MemLp (⇑f) p μ

theorem MeasureTheory.SimpleFunc.integrable_of_isFiniteMeasure {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : Measure α} [IsFiniteMeasure μ] (f : SimpleFunc α E) : Integrable (⇑f) μ

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 ≠ ⊤) : μ (Function.support ⇑f) < ⊤

theorem MeasureTheory.SimpleFunc.measure_support_lt_top_of_integrable {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : Measure α} (f : SimpleFunc α E) (hf : Integrable (⇑f) μ) : μ (Function.support ⇑f) < ⊤

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 = ↑↑g → f = 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).

@[implicit_reducible]

def MeasureTheory.Lp.simpleFunc.smul {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 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

• MeasureTheory.Lp.simpleFunc.smul = { smul := fun (k : 𝕜) (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)) => ⟨k • ↑f, ⋯⟩ }

@[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] [IsBoundedSMul 𝕜 E] (c : 𝕜) (f : ↥(simpleFunc E p μ)) : ↑(c • f) = c • ↑f

@[implicit_reducible]

def MeasureTheory.Lp.simpleFunc.module {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 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

• MeasureTheory.Lp.simpleFunc.module = { toSMul := MeasureTheory.Lp.simpleFunc.smul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

theorem MeasureTheory.Lp.simpleFunc.isBoundedSMul {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [Fact (1 ≤ p)] : IsBoundedSMul 𝕜 ↥(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.

@[implicit_reducible]

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

• MeasureTheory.Lp.simpleFunc.normedSpace = { toModule := MeasureTheory.Lp.simpleFunc.module, norm_smul_le := ⋯ }

@[reducible, inline]

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

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

Equations

• f.toLp hf = ⟨MeasureTheory.MemLp.toLp (⇑f) hf, ⋯⟩

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 μ) : ↑(f.toLp 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 μ) : ↑↑(f.toLp hf) = AEEqFun.mk ⇑f ⋯

theorem MeasureTheory.Lp.simpleFunc.toLp_zero {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} : SimpleFunc.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 μ) : (f + g).toLp ⋯ = f.toLp hf + g.toLp 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 μ) : (-f).toLp ⋯ = -f.toLp 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 μ) : (f - g).toLp ⋯ = f.toLp hf - g.toLp 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] [IsBoundedSMul 𝕜 E] (f : SimpleFunc α E) (hf : MemLp (⇑f) p μ) (c : 𝕜) : (c • f).toLp ⋯ = c • f.toLp 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 μ) : ‖f.toLp hf‖ = (eLpNorm (⇑f) p μ).toReal

noncomputable def MeasureTheory.Lp.simpleFunc.toSimpleFunc {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (f : ↥(simpleFunc E p μ)) : SimpleFunc α E

Find a representative of a Lp.simpleFunc.

Equations

• MeasureTheory.Lp.simpleFunc.toSimpleFunc f = Classical.choose ⋯

theorem MeasureTheory.Lp.simpleFunc.measurable {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [MeasurableSpace E] (f : ↥(simpleFunc E p μ)) : Measurable ⇑(toSimpleFunc f)

(toSimpleFunc f) is measurable.

theorem MeasureTheory.Lp.simpleFunc.stronglyMeasurable {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (f : ↥(simpleFunc E p μ)) : StronglyMeasurable ⇑(toSimpleFunc f)

theorem MeasureTheory.Lp.simpleFunc.aemeasurable {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [MeasurableSpace E] (f : ↥(simpleFunc E p μ)) : AEMeasurable (⇑(toSimpleFunc f)) μ

theorem MeasureTheory.Lp.simpleFunc.aestronglyMeasurable {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (f : ↥(simpleFunc E p μ)) : AEStronglyMeasurable (⇑(toSimpleFunc f)) μ

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) =ᵐ[μ] ↑↑↑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 μ)) : (toSimpleFunc f).toLp ⋯ = 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 (f.toLp hfi)) =ᵐ[μ] ⇑f

theorem MeasureTheory.Lp.simpleFunc.zero_toSimpleFunc {α : Type u_1} (E : Type u_4) [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} (μ : Measure α) : ⇑(toSimpleFunc 0) =ᵐ[μ] 0

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)) =ᵐ[μ] ⇑(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 μ)) : ⇑(toSimpleFunc (-f)) =ᵐ[μ] -⇑(toSimpleFunc f)

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)) =ᵐ[μ] ⇑(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] [IsBoundedSMul 𝕜 E] (k : 𝕜) (f : ↥(simpleFunc E p μ)) : ⇑(toSimpleFunc (k • f)) =ᵐ[μ] 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 μ)) : ‖f‖ = (eLpNorm (⇑(toSimpleFunc f)) p μ).toReal

noncomputable 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

• MeasureTheory.Lp.simpleFunc.indicatorConst p hs hμs c = (MeasureTheory.SimpleFunc.piecewise s hs (MeasureTheory.SimpleFunc.const α c) (MeasureTheory.SimpleFunc.const α 0)).toLp ⋯

@[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) : ⇑(toSimpleFunc (indicatorConst p hs hμs c)) =ᵐ[μ] ⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))

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} (indicatorConst : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P (indicatorConst p hs ⋯ c)) (add : ∀ ⦃f g : SimpleFunc α E⦄ (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ), Disjoint (Function.support ⇑f) (Function.support ⇑g) → P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp 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).

theorem MeasureTheory.Lp.simpleFunc.uniformContinuous {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [Fact (1 ≤ p)] : UniformContinuous Subtype.val

theorem MeasureTheory.Lp.simpleFunc.isUniformEmbedding {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [Fact (1 ≤ p)] : IsUniformEmbedding Subtype.val

theorem MeasureTheory.Lp.simpleFunc.isUniformInducing {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [Fact (1 ≤ p)] : IsUniformInducing Subtype.val

theorem MeasureTheory.Lp.simpleFunc.isDenseEmbedding {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [Fact (1 ≤ p)] (hp_ne_top : p ≠ ⊤) : IsDenseEmbedding Subtype.val

theorem MeasureTheory.Lp.simpleFunc.isDenseInducing {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [Fact (1 ≤ p)] (hp_ne_top : p ≠ ⊤) : IsDenseInducing Subtype.val

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 ≠ ⊤) : DenseRange Subtype.val

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] [IsBoundedSMul 𝕜 E] : ↥(simpleFunc E p μ) →L[𝕜] ↥(Lp E p μ)

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

Equations

• MeasureTheory.Lp.simpleFunc.coeToLp α E 𝕜 = { toFun := (↑(MeasureTheory.Lp.simpleFunc E p μ).subtype).toFun, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

theorem MeasureTheory.Lp.simpleFunc.coeFn_le {α : Type u_1} [MeasurableSpace α] {p : ENNReal} {μ : Measure α} {G : Type u_7} [NormedAddCommGroup G] [PartialOrder G] (f g : ↥(simpleFunc G p μ)) : ↑↑↑f ≤ᵐ[μ] ↑↑↑g ↔ f ≤ g

theorem MeasureTheory.Lp.simpleFunc.coeFn_zero {α : Type u_1} [MeasurableSpace α] (p : ENNReal) (μ : Measure α) (G : Type u_7) [NormedAddCommGroup G] : ↑↑↑0 =ᵐ[μ] 0

theorem MeasureTheory.Lp.simpleFunc.coeFn_nonneg {α : Type u_1} [MeasurableSpace α] {p : ENNReal} {μ : Measure α} {G : Type u_7} [NormedAddCommGroup G] [PartialOrder G] (f : ↥(simpleFunc G p μ)) : 0 ≤ᵐ[μ] ↑↑↑f ↔ 0 ≤ f

theorem MeasureTheory.Lp.simpleFunc.exists_simpleFunc_nonneg_ae_eq {α : Type u_1} [MeasurableSpace α] {p : ENNReal} {μ : Measure α} {G : Type u_7} [NormedAddCommGroup G] [PartialOrder G] {f : ↥(simpleFunc G p μ)} (hf : 0 ≤ f) : ∃ (f' : SimpleFunc α G), 0 ≤ f' ∧ ↑↑↑f =ᵐ[μ] ⇑f'

def MeasureTheory.Lp.simpleFunc.coeSimpleFuncNonnegToLpNonneg {α : Type u_1} [MeasurableSpace α] (p : ENNReal) (μ : Measure α) (G : Type u_7) [NormedAddCommGroup G] [PartialOrder 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

• MeasureTheory.Lp.simpleFunc.coeSimpleFuncNonnegToLpNonneg p μ G g = ⟨↑↑g, ⋯⟩

theorem MeasureTheory.Lp.simpleFunc.denseRange_coeSimpleFuncNonnegToLpNonneg {α : Type u_1} [MeasurableSpace α] (p : ENNReal) (μ : Measure α) (G : Type u_7) [NormedAddCommGroup G] [PartialOrder G] [hp : Fact (1 ≤ p)] (hp_ne_top : p ≠ ⊤) : DenseRange (coeSimpleFuncNonnegToLpNonneg p μ G)

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 ≠ ⊤) (motive : ↥(Lp E p μ) → Prop) (indicatorConst : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), motive ↑(simpleFunc.indicatorConst p hs ⋯ c)) (add : ∀ ⦃f g : α → E⦄ (hf : MemLp f p μ) (hg : MemLp g p μ), Disjoint (Function.support f) (Function.support g) → motive (MemLp.toLp f hf) → motive (MemLp.toLp g hg) → motive (MemLp.toLp f hf + MemLp.toLp g hg)) (isClosed : IsClosed {f : ↥(Lp E p μ) | motive f}) (f : ↥(Lp E p μ)) : motive 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 ≠ ⊤) (motive : (α → E) → Prop) (indicator : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → motive (s.indicator fun (x : α) => c)) (add : ∀ ⦃f g : α → E⦄, Disjoint (Function.support f) (Function.support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)) (closed : IsClosed {f : ↥(Lp E p μ) | motive ↑↑f}) (ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g) ⦃f : α → E⦄ : MemLp f p μ → motive 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 f → P g → P (f + g)) (h2P : ∀ (f : α → E), P f → AEStronglyMeasurable 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.

def MeasureTheory.«term_→₁ₛ[_]_» : Lean.TrailingParserDescr

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) μ) : ↑(f.toLp ⋯) = Integrable.toL1 (⇑f) hf

theorem MeasureTheory.L1.SimpleFunc.integrable {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : Measure α} (f : ↥(α →₁ₛ[μ] E)) : Integrable (⇑(Lp.simpleFunc.toSimpleFunc f)) μ

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 f → P g → P (f + g)) (h_closed : IsClosed {f : ↥(Lp E 1 μ) | P ↑↑f}) (h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Integrable f μ → P f → P 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 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}).