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} [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 : ℕ) : ‖↑(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} [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 : ℕ) : ‖↑(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} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] [OpensMeasurableSpace E] {f : β → E} (hf : Measurable f) {s : Set E} (h₀ : 0 ∈ s) [TopologicalSpace.SeparableSpace ↑s] (x : β) (n : ℕ) : ‖↑(MeasureTheory.SimpleFunc.approxOn f hf s 0 h₀ n) x‖ ≤ ‖f x‖ + ‖f x‖

theorem MeasureTheory.SimpleFunc.tendsto_approxOn_Lp_snorm {β : 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 ≠ ⊤) {μ : MeasureTheory.Measure β} (hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s) (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} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] {p : ENNReal} [BorelSpace E] {f : β → E} {μ : MeasureTheory.Measure β} (fmeas : Measurable f) (hf : MeasureTheory.Memℒp f p μ) {s : Set E} {y₀ : E} (h₀ : y₀ ∈ s) [TopologicalSpace.SeparableSpace ↑s] (hi₀ : MeasureTheory.Memℒp (fun (x : β) => y₀) p μ) (n : ℕ) : MeasureTheory.Memℒp (↑(MeasureTheory.SimpleFunc.approxOn f fmeas s y₀ h₀ n)) p μ

theorem MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp_snorm {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] {p : ENNReal} [BorelSpace E] {f : β → E} (hp_ne_top : p ≠ ⊤) {μ : MeasureTheory.Measure β} (fmeas : Measurable f) [TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {0})] (hf : MeasureTheory.snorm f p μ < ⊤) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.snorm (↑(MeasureTheory.SimpleFunc.approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) - f) p μ) Filter.atTop (nhds 0)

theorem MeasureTheory.SimpleFunc.memℒp_approxOn_range {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] {p : ENNReal} [BorelSpace E] {f : β → E} {μ : MeasureTheory.Measure β} (fmeas : Measurable f) [TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {0})] (hf : MeasureTheory.Memℒp f p μ) (n : ℕ) : MeasureTheory.Memℒp (↑(MeasureTheory.SimpleFunc.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 ≠ ⊤) {μ : MeasureTheory.Measure β} (fmeas : Measurable f) [TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {0})] (hf : MeasureTheory.Memℒp f p μ) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.Memℒp.toLp ↑(MeasureTheory.SimpleFunc.approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) ⋯) Filter.atTop (nhds (MeasureTheory.Memℒp.toLp f hf))

theorem MeasureTheory.Memℒp.exists_simpleFunc_snorm_sub_lt {β : Type u_2} [MeasurableSpace β] {p : ENNReal} {E : Type u_7} [NormedAddCommGroup E] {f : β → E} {μ : MeasureTheory.Measure β} (hf : MeasureTheory.Memℒp f p μ) (hp_ne_top : p ≠ ⊤) {ε : ENNReal} (hε : ε ≠ 0) : ∃ (g : MeasureTheory.SimpleFunc β E), 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} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] [OpensMeasurableSpace E] {f : β → E} (hf : Measurable f) {s : Set E} {y₀ : E} (h₀ : y₀ ∈ s) [TopologicalSpace.SeparableSpace ↑s] {μ : MeasureTheory.Measure β} (hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s) (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} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] [BorelSpace E] {f : β → E} {μ : MeasureTheory.Measure β} (fmeas : Measurable f) (hf : MeasureTheory.Integrable f μ) {s : Set E} {y₀ : E} (h₀ : y₀ ∈ s) [TopologicalSpace.SeparableSpace ↑s] (hi₀ : MeasureTheory.Integrable (fun (x : β) => y₀) μ) (n : ℕ) : MeasureTheory.Integrable (↑(MeasureTheory.SimpleFunc.approxOn f fmeas s y₀ h₀ n)) μ

theorem MeasureTheory.SimpleFunc.tendsto_approxOn_range_L1_nnnorm {β : Type u_2} {E : Type u_4} [MeasurableSpace β] [MeasurableSpace E] [NormedAddCommGroup E] [OpensMeasurableSpace E] {f : β → E} {μ : MeasureTheory.Measure β} [TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {0})] (fmeas : Measurable f) (hf : MeasureTheory.Integrable f μ) : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (x : β), ↑‖↑(MeasureTheory.SimpleFunc.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} {μ : MeasureTheory.Measure β} (fmeas : Measurable f) [TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {0})] (hf : MeasureTheory.Integrable f μ) (n : ℕ) : MeasureTheory.Integrable (↑(MeasureTheory.SimpleFunc.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 μ:

• 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} [MeasurableSpace α] [NormedAddCommGroup F] (f : MeasureTheory.SimpleFunc α F) : ∃ (C : ℝ), ∀ (x : α), ‖↑f x‖ ≤ C

theorem MeasureTheory.SimpleFunc.memℒp_zero {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (f : MeasureTheory.SimpleFunc α E) (μ : MeasureTheory.Measure α) : MeasureTheory.Memℒp (↑f) 0 μ

theorem MeasureTheory.SimpleFunc.memℒp_top {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (f : MeasureTheory.SimpleFunc α E) (μ : MeasureTheory.Measure α) : MeasureTheory.Memℒp ↑f ⊤ μ

theorem MeasureTheory.SimpleFunc.snorm'_eq {α : Type u_1} {F : Type u_5} [MeasurableSpace α] [NormedAddCommGroup F] {p : ℝ} (f : MeasureTheory.SimpleFunc α F) (μ : MeasureTheory.Measure α) : MeasureTheory.snorm' (↑f) p μ = (Finset.sum (MeasureTheory.SimpleFunc.range f) 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} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} (hp_pos : p ≠ 0) (hp_ne_top : p ≠ ⊤) (f : MeasureTheory.SimpleFunc α E) (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} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} (p : ENNReal) {f : MeasureTheory.SimpleFunc α E} (hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤) : MeasureTheory.Memℒp (↑f) p μ

theorem MeasureTheory.SimpleFunc.memℒp_iff {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} {f : MeasureTheory.SimpleFunc α E} (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} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α E} : MeasureTheory.Integrable (↑f) μ ↔ ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤

theorem MeasureTheory.SimpleFunc.memℒp_iff_integrable {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} {f : MeasureTheory.SimpleFunc α E} (hp_pos : p ≠ 0) (hp_ne_top : p ≠ ⊤) : MeasureTheory.Memℒp (↑f) p μ ↔ MeasureTheory.Integrable (↑f) μ

theorem MeasureTheory.SimpleFunc.memℒp_iff_finMeasSupp {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} {f : MeasureTheory.SimpleFunc α E} (hp_pos : p ≠ 0) (hp_ne_top : p ≠ ⊤) : MeasureTheory.Memℒp (↑f) p μ ↔ MeasureTheory.SimpleFunc.FinMeasSupp f μ

theorem MeasureTheory.SimpleFunc.integrable_iff_finMeasSupp {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α E} : MeasureTheory.Integrable (↑f) μ ↔ MeasureTheory.SimpleFunc.FinMeasSupp f μ

theorem MeasureTheory.SimpleFunc.FinMeasSupp.integrable {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α E} (h : MeasureTheory.SimpleFunc.FinMeasSupp f μ) : MeasureTheory.Integrable (↑f) μ

theorem MeasureTheory.SimpleFunc.integrable_pair {α : Type u_1} {E : Type u_4} {F : Type u_5} [MeasurableSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α E} {g : MeasureTheory.SimpleFunc α F} : MeasureTheory.Integrable (↑f) μ → MeasureTheory.Integrable (↑g) μ → MeasureTheory.Integrable (↑(MeasureTheory.SimpleFunc.pair f g)) μ

theorem MeasureTheory.SimpleFunc.memℒp_of_isFiniteMeasure {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (f : MeasureTheory.SimpleFunc α E) (p : ENNReal) (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.Memℒp (↑f) p μ

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

theorem MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_integrable {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.Integrable (↑f) μ) {x : E} (hx : x ≠ 0) : ↑↑μ (↑f ⁻¹' {x}) < ⊤

theorem MeasureTheory.SimpleFunc.measure_support_lt_top {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [Zero β] (f : MeasureTheory.SimpleFunc α β) (hf : ∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤) : ↑↑μ (Function.support ↑f) < ⊤

theorem MeasureTheory.SimpleFunc.measure_support_lt_top_of_memℒp {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} (f : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.Memℒp (↑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] {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.Integrable (↑f) μ) : ↑↑μ (Function.support ↑f) < ⊤

theorem MeasureTheory.SimpleFunc.measure_lt_top_of_memℒp_indicator {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} (hp_pos : p ≠ 0) (hp_ne_top : p ≠ ⊤) {c : E} (hc : c ≠ 0) {s : Set α} (hs : MeasurableSet s) (hcs : MeasureTheory.Memℒp (↑(MeasureTheory.SimpleFunc.piecewise s hs (MeasureTheory.SimpleFunc.const α c) (MeasureTheory.SimpleFunc.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) (μ : MeasureTheory.Measure α) : AddSubgroup ↥(MeasureTheory.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} {μ : MeasureTheory.Measure α} {f : ↥(MeasureTheory.Lp.simpleFunc E p μ)} {g : ↥(MeasureTheory.Lp.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).

def MeasureTheory.Lp.simpleFunc.smul {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] : SMul 𝕜 ↥(MeasureTheory.Lp.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 μ)) => { val := k • ↑f, property := ⋯ } }

@[simp]

theorem MeasureTheory.Lp.simpleFunc.coe_smul {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] (c : 𝕜) (f : ↥(MeasureTheory.Lp.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} {μ : MeasureTheory.Measure α} [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] : Module 𝕜 ↥(MeasureTheory.Lp.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 = Module.mk ⋯ ⋯

theorem MeasureTheory.Lp.simpleFunc.boundedSMul {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] [Fact (1 ≤ p)] : BoundedSMul 𝕜 ↥(MeasureTheory.Lp.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} {μ : MeasureTheory.Measure α} {𝕜 : Type u_7} [NormedField 𝕜] [NormedSpace 𝕜 E] [Fact (1 ≤ p)] : NormedSpace 𝕜 ↥(MeasureTheory.Lp.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 = NormedSpace.mk ⋯

@[reducible]

def MeasureTheory.Lp.simpleFunc.toLp {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.Memℒp (↑f) p μ) : ↥(MeasureTheory.Lp.simpleFunc E p μ)

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

Equations

• MeasureTheory.Lp.simpleFunc.toLp f hf = { val := MeasureTheory.Memℒp.toLp (↑f) hf, property := ⋯ }

theorem MeasureTheory.Lp.simpleFunc.toLp_eq_toLp {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.Memℒp (↑f) p μ) : ↑(MeasureTheory.Lp.simpleFunc.toLp f hf) = MeasureTheory.Memℒp.toLp (↑f) hf

theorem MeasureTheory.Lp.simpleFunc.toLp_eq_mk {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.Memℒp (↑f) p μ) : ↑↑(MeasureTheory.Lp.simpleFunc.toLp f hf) = MeasureTheory.AEEqFun.mk ↑f ⋯

theorem MeasureTheory.Lp.simpleFunc.toLp_zero {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} : MeasureTheory.Lp.simpleFunc.toLp 0 ⋯ = 0

theorem MeasureTheory.Lp.simpleFunc.toLp_add {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α E) (g : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.Memℒp (↑f) p μ) (hg : MeasureTheory.Memℒp (↑g) p μ) : MeasureTheory.Lp.simpleFunc.toLp (f + g) ⋯ = MeasureTheory.Lp.simpleFunc.toLp f hf + MeasureTheory.Lp.simpleFunc.toLp g hg

theorem MeasureTheory.Lp.simpleFunc.toLp_neg {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.Memℒp (↑f) p μ) : MeasureTheory.Lp.simpleFunc.toLp (-f) ⋯ = -MeasureTheory.Lp.simpleFunc.toLp f hf

theorem MeasureTheory.Lp.simpleFunc.toLp_sub {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α E) (g : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.Memℒp (↑f) p μ) (hg : MeasureTheory.Memℒp (↑g) p μ) : MeasureTheory.Lp.simpleFunc.toLp (f - g) ⋯ = MeasureTheory.Lp.simpleFunc.toLp f hf - MeasureTheory.Lp.simpleFunc.toLp g hg

theorem MeasureTheory.Lp.simpleFunc.toLp_smul {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] (f : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.Memℒp (↑f) p μ) (c : 𝕜) : MeasureTheory.Lp.simpleFunc.toLp (c • f) ⋯ = c • MeasureTheory.Lp.simpleFunc.toLp f hf

theorem MeasureTheory.Lp.simpleFunc.norm_toLp {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} [Fact (1 ≤ p)] (f : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.Memℒp (↑f) p μ) : ‖MeasureTheory.Lp.simpleFunc.toLp f hf‖ = (MeasureTheory.snorm (↑f) p μ).toReal

def MeasureTheory.Lp.simpleFunc.toSimpleFunc {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)) : MeasureTheory.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} {μ : MeasureTheory.Measure α} [MeasurableSpace E] (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)) : Measurable ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)

(toSimpleFunc f) is measurable.

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

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

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

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

theorem MeasureTheory.Lp.simpleFunc.memℒp {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)) : MeasureTheory.Memℒp (↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)) p μ

toSimpleFunc f satisfies the predicate Memℒp.

theorem MeasureTheory.Lp.simpleFunc.toLp_toSimpleFunc {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)) : MeasureTheory.Lp.simpleFunc.toLp (MeasureTheory.Lp.simpleFunc.toSimpleFunc f) ⋯ = f

theorem MeasureTheory.Lp.simpleFunc.toSimpleFunc_toLp {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α E) (hfi : MeasureTheory.Memℒp (↑f) p μ) : ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc (MeasureTheory.Lp.simpleFunc.toLp f hfi)) =ᶠ[MeasureTheory.Measure.ae μ] ↑f

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

theorem MeasureTheory.Lp.simpleFunc.add_toSimpleFunc {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)) (g : ↥(MeasureTheory.Lp.simpleFunc E p μ)) : ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc (f + g)) =ᶠ[MeasureTheory.Measure.ae μ] ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f) + ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc g)

theorem MeasureTheory.Lp.simpleFunc.neg_toSimpleFunc {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)) : ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc (-f)) =ᶠ[MeasureTheory.Measure.ae μ] -↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)

theorem MeasureTheory.Lp.simpleFunc.sub_toSimpleFunc {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)) (g : ↥(MeasureTheory.Lp.simpleFunc E p μ)) : ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc (f - g)) =ᶠ[MeasureTheory.Measure.ae μ] ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f) - ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc g)

theorem MeasureTheory.Lp.simpleFunc.smul_toSimpleFunc {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] (k : 𝕜) (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)) : ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc (k • f)) =ᶠ[MeasureTheory.Measure.ae μ] k • ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)

theorem MeasureTheory.Lp.simpleFunc.norm_toSimpleFunc {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} [Fact (1 ≤ p)] (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)) : ‖f‖ = (MeasureTheory.snorm (↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)) p μ).toReal

def MeasureTheory.Lp.simpleFunc.indicatorConst {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (p : ENNReal) {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (c : E) : ↥(MeasureTheory.Lp.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} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (c : E) : ↑(MeasureTheory.Lp.simpleFunc.indicatorConst p hs hμs c) = MeasureTheory.indicatorConstLp p hs hμs c

theorem MeasureTheory.Lp.simpleFunc.toSimpleFunc_indicatorConst {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) (c : E) : ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc (MeasureTheory.Lp.simpleFunc.indicatorConst p hs hμs c)) =ᶠ[MeasureTheory.Measure.ae μ] ↑(MeasureTheory.SimpleFunc.piecewise s hs (MeasureTheory.SimpleFunc.const α c) (MeasureTheory.SimpleFunc.const α 0))

theorem MeasureTheory.Lp.simpleFunc.induction {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} (hp_pos : p ≠ 0) (hp_ne_top : p ≠ ⊤) {P : ↥(MeasureTheory.Lp.simpleFunc E p μ) → Prop} (h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (MeasureTheory.Lp.simpleFunc.indicatorConst p hs ⋯ c)) (h_add : ∀ ⦃f g : MeasureTheory.SimpleFunc α E⦄ (hf : MeasureTheory.Memℒp (↑f) p μ) (hg : MeasureTheory.Memℒp (↑g) p μ), Disjoint (Function.support ↑f) (Function.support ↑g) → P (MeasureTheory.Lp.simpleFunc.toLp f hf) → P (MeasureTheory.Lp.simpleFunc.toLp g hg) → P (MeasureTheory.Lp.simpleFunc.toLp f hf + MeasureTheory.Lp.simpleFunc.toLp g hg)) (f : ↥(MeasureTheory.Lp.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} {μ : MeasureTheory.Measure α} [Fact (1 ≤ p)] : UniformContinuous Subtype.val

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

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

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

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

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

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

Equations

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

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

instance MeasureTheory.Lp.simpleFunc.instCovariantClassLE {α : Type u_1} [MeasurableSpace α] {p : ENNReal} {μ : MeasureTheory.Measure α} {G : Type u_7} [NormedLatticeAddCommGroup G] : CovariantClass (↥(MeasureTheory.Lp.simpleFunc G p μ)) (↥(MeasureTheory.Lp.simpleFunc G p μ)) (fun (x x_1 : ↥(MeasureTheory.Lp.simpleFunc G p μ)) => x + x_1) fun (x x_1 : ↥(MeasureTheory.Lp.simpleFunc G p μ)) => x ≤ x_1

Equations

• ⋯ = ⋯

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

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

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

def MeasureTheory.Lp.simpleFunc.coeSimpleFuncNonnegToLpNonneg {α : Type u_1} [MeasurableSpace α] (p : ENNReal) (μ : MeasureTheory.Measure α) (G : Type u_7) [NormedLatticeAddCommGroup G] : { g : ↥(MeasureTheory.Lp.simpleFunc G p μ) // 0 ≤ g } → { g : ↥(MeasureTheory.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 = { val := ↑↑g, property := ⋯ }

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

theorem MeasureTheory.Lp.induction {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} [_i : Fact (1 ≤ p)] (hp_ne_top : p ≠ ⊤) (P : ↥(MeasureTheory.Lp E p μ) → Prop) (h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P ↑(MeasureTheory.Lp.simpleFunc.indicatorConst p hs ⋯ c)) (h_add : ∀ ⦃f g : α → E⦄ (hf : MeasureTheory.Memℒp f p μ) (hg : MeasureTheory.Memℒp g p μ), Disjoint (Function.support f) (Function.support g) → P (MeasureTheory.Memℒp.toLp f hf) → P (MeasureTheory.Memℒp.toLp g hg) → P (MeasureTheory.Memℒp.toLp f hf + MeasureTheory.Memℒp.toLp g hg)) (h_closed : IsClosed {f : ↥(MeasureTheory.Lp E p μ) | P f}) (f : ↥(MeasureTheory.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.Memℒp.induction {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} [_i : Fact (1 ≤ p)] (hp_ne_top : p ≠ ⊤) (P : (α → E) → Prop) (h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun (x : α) => c)) (h_add : ∀ ⦃f g : α → E⦄, Disjoint (Function.support f) (Function.support g) → MeasureTheory.Memℒp f p μ → MeasureTheory.Memℒp g p μ → P f → P g → P (f + g)) (h_closed : IsClosed {f : ↥(MeasureTheory.Lp E p μ) | P ↑↑f}) (h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[MeasureTheory.Measure.ae μ] g → MeasureTheory.Memℒp f p μ → P f → P g) ⦃f : α → E⦄ : MeasureTheory.Memℒp f p μ → 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;
• 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.Memℒp.induction_dense {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} (hp_ne_top : p ≠ ⊤) (P : (α → E) → Prop) (h0P : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ (g : α → E), MeasureTheory.snorm (g - Set.indicator s fun (x : α) => c) p μ ≤ ε ∧ P g) (h1P : ∀ (f g : α → E), P f → P g → P (f + g)) (h2P : ∀ (f : α → E), P f → MeasureTheory.AEStronglyMeasurable f μ) {f : α → E} (hf : MeasureTheory.Memℒp f p μ) {ε : 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.

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] {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.Integrable (↑f) μ) : ↑(MeasureTheory.Lp.simpleFunc.toLp f ⋯) = MeasureTheory.Integrable.toL1 (↑f) hf

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

theorem MeasureTheory.Integrable.induction {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} (P : (α → E) → Prop) (h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun (x : α) => c)) (h_add : ∀ ⦃f g : α → E⦄, Disjoint (Function.support f) (Function.support g) → MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → P f → P g → P (f + g)) (h_closed : IsClosed {f : ↥(MeasureTheory.Lp E 1 μ) | P ↑↑f}) (h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[MeasureTheory.Measure.ae μ] g → MeasureTheory.Integrable f μ → P f → P g) ⦃f : α → E⦄ : MeasureTheory.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}).