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.

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₀ : Membership.mem s y₀) [TopologicalSpace.SeparableSpace s.Elem] (x : β) (n : Nat) : LE.le (NNNorm.nnnorm (HSub.hSub (DFunLike.coe (approxOn f hf s y₀ h₀ n) x) (f x))) (NNNorm.nnnorm (HSub.hSub (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₀ : Membership.mem s y₀) [TopologicalSpace.SeparableSpace s.Elem] (x : β) (n : Nat) : LE.le (Norm.norm (HSub.hSub (DFunLike.coe (approxOn f hf s y₀ h₀ n) x) y₀)) (HAdd.hAdd (Norm.norm (HSub.hSub (f x) y₀)) (Norm.norm (HSub.hSub (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₀ : Membership.mem s 0) [TopologicalSpace.SeparableSpace s.Elem] (x : β) (n : Nat) : LE.le (Norm.norm (DFunLike.coe (approxOn f hf s 0 h₀ n) x)) (HAdd.hAdd (Norm.norm (f x)) (Norm.norm (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₀ : Membership.mem s y₀) [TopologicalSpace.SeparableSpace s.Elem] (hp_ne_top : Ne p Top.top) {μ : Measure β} (hμ : Filter.Eventually (fun (x : β) => Membership.mem (closure s) (f x)) (ae μ)) (hi : LT.lt (eLpNorm (fun (x : β) => HSub.hSub (f x) y₀) p μ) Top.top) : Filter.Tendsto (fun (n : Nat) => eLpNorm (HSub.hSub (DFunLike.coe (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₀ : Membership.mem s y₀) [TopologicalSpace.SeparableSpace s.Elem] (hi₀ : MemLp (fun (x : β) => y₀) p μ) (n : Nat) : MemLp (DFunLike.coe (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 : Ne p Top.top) {μ : Measure β} (fmeas : Measurable f) [TopologicalSpace.SeparableSpace (Union.union (Set.range f) (Singleton.singleton 0)).Elem] (hf : LT.lt (eLpNorm f p μ) Top.top) : Filter.Tendsto (fun (n : Nat) => eLpNorm (HSub.hSub (DFunLike.coe (approxOn f fmeas (Union.union (Set.range f) (Singleton.singleton 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 (Union.union (Set.range f) (Singleton.singleton 0)).Elem] (hf : MemLp f p μ) (n : Nat) : MemLp (DFunLike.coe (approxOn f fmeas (Union.union (Set.range f) (Singleton.singleton 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 (LE.le 1 p)] (hp_ne_top : Ne p Top.top) {μ : Measure β} (fmeas : Measurable f) [TopologicalSpace.SeparableSpace (Union.union (Set.range f) (Singleton.singleton 0)).Elem] (hf : MemLp f p μ) : Filter.Tendsto (fun (n : Nat) => MemLp.toLp (DFunLike.coe (approxOn f fmeas (Union.union (Set.range f) (Singleton.singleton 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 : Ne p Top.top) {ε : ENNReal} (hε : Ne ε 0) : Exists fun (g : SimpleFunc β E) => And (LT.lt (eLpNorm (HSub.hSub f (DFunLike.coe g)) p μ) ε) (MemLp (DFunLike.coe 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₀ : Membership.mem s y₀) [TopologicalSpace.SeparableSpace s.Elem] {μ : Measure β} (hμ : Filter.Eventually (fun (x : β) => Membership.mem (closure s) (f x)) (ae μ)) (hi : HasFiniteIntegral (fun (x : β) => HSub.hSub (f x) y₀) μ) : Filter.Tendsto (fun (n : Nat) => MeasureTheory.lintegral μ fun (x : β) => ENorm.enorm (HSub.hSub (DFunLike.coe (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₀ : Membership.mem s y₀) [TopologicalSpace.SeparableSpace s.Elem] {μ : Measure β} (hμ : Filter.Eventually (fun (x : β) => Membership.mem (closure s) (f x)) (ae μ)) (hi : HasFiniteIntegral (fun (x : β) => HSub.hSub (f x) y₀) μ) : Filter.Tendsto (fun (n : Nat) => MeasureTheory.lintegral μ fun (x : β) => ENorm.enorm (HSub.hSub (DFunLike.coe (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₀ : Membership.mem s y₀) [TopologicalSpace.SeparableSpace s.Elem] (hi₀ : Integrable (fun (x : β) => y₀) μ) (n : Nat) : Integrable (DFunLike.coe (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 (Union.union (Set.range f) (Singleton.singleton 0)).Elem] (fmeas : Measurable f) (hf : Integrable f μ) : Filter.Tendsto (fun (n : Nat) => MeasureTheory.lintegral μ fun (x : β) => ENorm.enorm (HSub.hSub (DFunLike.coe (approxOn f fmeas (Union.union (Set.range f) (Singleton.singleton 0)) 0 ⋯ n) x) (f x))) Filter.atTop (nhds 0)

@[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 (Union.union (Set.range f) (Singleton.singleton 0)).Elem] (fmeas : Measurable f) (hf : Integrable f μ) : Filter.Tendsto (fun (n : Nat) => MeasureTheory.lintegral μ fun (x : β) => ENorm.enorm (HSub.hSub (DFunLike.coe (approxOn f fmeas (Union.union (Set.range f) (Singleton.singleton 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 (Union.union (Set.range f) (Singleton.singleton 0)).Elem] (hf : Integrable f μ) (n : Nat) : Integrable (DFunLike.coe (approxOn f fmeas (Union.union (Set.range f) (Singleton.singleton 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) : Exists fun (C : Real) => ∀ (x : α), LE.le (Norm.norm (DFunLike.coe f x)) C

theorem MeasureTheory.SimpleFunc.memLp_zero {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (f : SimpleFunc α E) (μ : Measure α) : MemLp (DFunLike.coe f) 0 μ

theorem MeasureTheory.SimpleFunc.memLp_top {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (f : SimpleFunc α E) (μ : Measure α) : MemLp (DFunLike.coe f) Top.top μ

theorem MeasureTheory.SimpleFunc.eLpNorm'_eq {α : Type u_1} {F : Type u_5} [MeasurableSpace α] [NormedAddCommGroup F] {p : Real} (f : SimpleFunc α F) (μ : Measure α) : Eq (eLpNorm' (DFunLike.coe f) p μ) (HPow.hPow (f.range.sum fun (y : F) => HMul.hMul (HPow.hPow (ENorm.enorm y) p) (DFunLike.coe μ (Set.preimage (DFunLike.coe f) (Singleton.singleton y)))) (HDiv.hDiv 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 : Ne p 0) (hp_ne_top : Ne p Top.top) (f : SimpleFunc α E) (hf : MemLp (DFunLike.coe f) p μ) (y : E) (hy_ne : Ne y 0) : LT.lt (DFunLike.coe μ (Set.preimage (DFunLike.coe f) (Singleton.singleton y))) Top.top

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), Ne y 0 → LT.lt (DFunLike.coe μ (Set.preimage (DFunLike.coe f) (Singleton.singleton y))) Top.top) : MemLp (DFunLike.coe 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 : Ne p 0) (hp_ne_top : Ne p Top.top) : Iff (MemLp (DFunLike.coe f) p μ) (∀ (y : E), Ne y 0 → LT.lt (DFunLike.coe μ (Set.preimage (DFunLike.coe f) (Singleton.singleton y))) Top.top)

theorem MeasureTheory.SimpleFunc.integrable_iff {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : Measure α} {f : SimpleFunc α E} : Iff (Integrable (DFunLike.coe f) μ) (∀ (y : E), Ne y 0 → LT.lt (DFunLike.coe μ (Set.preimage (DFunLike.coe f) (Singleton.singleton y))) Top.top)

theorem MeasureTheory.SimpleFunc.memLp_iff_integrable {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : Measure α} {p : ENNReal} {f : SimpleFunc α E} (hp_pos : Ne p 0) (hp_ne_top : Ne p Top.top) : Iff (MemLp (DFunLike.coe f) p μ) (Integrable (DFunLike.coe 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 : Ne p 0) (hp_ne_top : Ne p Top.top) : Iff (MemLp (DFunLike.coe f) p μ) (f.FinMeasSupp μ)

theorem MeasureTheory.SimpleFunc.integrable_iff_finMeasSupp {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : Measure α} {f : SimpleFunc α E} : Iff (Integrable (DFunLike.coe 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 (DFunLike.coe 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 (DFunLike.coe f) μ → Integrable (DFunLike.coe g) μ → Integrable (DFunLike.coe (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 (DFunLike.coe f) p μ

theorem MeasureTheory.SimpleFunc.integrable_of_isFiniteMeasure {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : Measure α} [IsFiniteMeasure μ] (f : SimpleFunc α E) : Integrable (DFunLike.coe 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 (DFunLike.coe f) μ) {x : E} (hx : Ne x 0) : LT.lt (DFunLike.coe μ (Set.preimage (DFunLike.coe f) (Singleton.singleton x))) Top.top

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 (DFunLike.coe f) p μ) (hp_ne_zero : Ne p 0) (hp_ne_top : Ne p Top.top) : LT.lt (DFunLike.coe μ (Function.support (DFunLike.coe f))) Top.top

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 (DFunLike.coe f) μ) : LT.lt (DFunLike.coe μ (Function.support (DFunLike.coe f))) Top.top

theorem MeasureTheory.SimpleFunc.measure_lt_top_of_memLp_indicator {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : Measure α} {p : ENNReal} (hp_pos : Ne p 0) (hp_ne_top : Ne p Top.top) {c : E} (hc : Ne c 0) {s : Set α} (hs : MeasurableSet s) (hcs : MemLp (DFunLike.coe (piecewise s hs (const α c) (const α 0))) p μ) : LT.lt (DFunLike.coe μ s) Top.top

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 (Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x)

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 : Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x} : Eq f.val.val g.val.val → Eq 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} {μ : Measure α} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] : SMul 𝕜 (Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x)

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

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

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 : Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x) : Eq (HSMul.hSMul c f).val (HSMul.hSMul c f.val)

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 𝕜 (Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x)

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

• Eq MeasureTheory.Lp.simpleFunc.module { toSMul := MeasureTheory.Lp.simpleFunc.smul, one_smul := ⋯, mul_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 (LE.le 1 p)] : IsBoundedSMul 𝕜 (Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x)

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.

@[deprecated MeasureTheory.Lp.simpleFunc.isBoundedSMul (since := "2025-03-10")]

theorem MeasureTheory.Lp.simpleFunc.boundedSMul {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [Fact (LE.le 1 p)] : IsBoundedSMul 𝕜 (Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x)

Alias of MeasureTheory.Lp.simpleFunc.isBoundedSMul.

---

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 (LE.le 1 p)] : NormedSpace 𝕜 (Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x)

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

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

@[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 (DFunLike.coe f) p μ) : Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x

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

Equations

• Eq (MeasureTheory.Lp.simpleFunc.toLp f hf) ⟨MeasureTheory.MemLp.toLp (DFunLike.coe 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 (DFunLike.coe f) p μ) : Eq (toLp f hf).val (MemLp.toLp (DFunLike.coe 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 (DFunLike.coe f) p μ) : Eq (toLp f hf).val.val (AEEqFun.mk (DFunLike.coe f) ⋯)

theorem MeasureTheory.Lp.simpleFunc.toLp_zero {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} : Eq (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 (DFunLike.coe f) p μ) (hg : MemLp (DFunLike.coe g) p μ) : Eq (toLp (HAdd.hAdd f g) ⋯) (HAdd.hAdd (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 (DFunLike.coe f) p μ) : Eq (toLp (Neg.neg f) ⋯) (Neg.neg (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 (DFunLike.coe f) p μ) (hg : MemLp (DFunLike.coe g) p μ) : Eq (toLp (HSub.hSub f g) ⋯) (HSub.hSub (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] [IsBoundedSMul 𝕜 E] (f : SimpleFunc α E) (hf : MemLp (DFunLike.coe f) p μ) (c : 𝕜) : Eq (toLp (HSMul.hSMul c f) ⋯) (HSMul.hSMul c (toLp f hf))

theorem MeasureTheory.Lp.simpleFunc.norm_toLp {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [Fact (LE.le 1 p)] (f : SimpleFunc α E) (hf : MemLp (DFunLike.coe f) p μ) : Eq (Norm.norm (toLp f hf)) (eLpNorm (DFunLike.coe f) p μ).toReal

def MeasureTheory.Lp.simpleFunc.toSimpleFunc {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (f : Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x) : SimpleFunc α E

Find a representative of a Lp.simpleFunc.

Equations

• Eq (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 : Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x) : Measurable (DFunLike.coe (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 : Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x) : StronglyMeasurable (DFunLike.coe (toSimpleFunc f))

theorem MeasureTheory.Lp.simpleFunc.aemeasurable {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [MeasurableSpace E] (f : Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x) : AEMeasurable (DFunLike.coe (toSimpleFunc f)) μ

theorem MeasureTheory.Lp.simpleFunc.aestronglyMeasurable {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (f : Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x) : AEStronglyMeasurable (DFunLike.coe (toSimpleFunc f)) μ

theorem MeasureTheory.Lp.simpleFunc.toSimpleFunc_eq_toFun {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (f : Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x) : (ae μ).EventuallyEq (DFunLike.coe (toSimpleFunc f)) f.val.val.cast

theorem MeasureTheory.Lp.simpleFunc.memLp {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (f : Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x) : MemLp (DFunLike.coe (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 : Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x) : Eq (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 (DFunLike.coe f) p μ) : (ae μ).EventuallyEq (DFunLike.coe (toSimpleFunc (toLp f hfi))) (DFunLike.coe f)

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

theorem MeasureTheory.Lp.simpleFunc.add_toSimpleFunc {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (f g : Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x) : (ae μ).EventuallyEq (DFunLike.coe (toSimpleFunc (HAdd.hAdd f g))) (HAdd.hAdd (DFunLike.coe (toSimpleFunc f)) (DFunLike.coe (toSimpleFunc g)))

theorem MeasureTheory.Lp.simpleFunc.neg_toSimpleFunc {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (f : Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x) : (ae μ).EventuallyEq (DFunLike.coe (toSimpleFunc (Neg.neg f))) (Neg.neg (DFunLike.coe (toSimpleFunc f)))

theorem MeasureTheory.Lp.simpleFunc.sub_toSimpleFunc {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} (f g : Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x) : (ae μ).EventuallyEq (DFunLike.coe (toSimpleFunc (HSub.hSub f g))) (HSub.hSub (DFunLike.coe (toSimpleFunc f)) (DFunLike.coe (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 : Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x) : (ae μ).EventuallyEq (DFunLike.coe (toSimpleFunc (HSMul.hSMul k f))) (HSMul.hSMul k (DFunLike.coe (toSimpleFunc f)))

theorem MeasureTheory.Lp.simpleFunc.norm_toSimpleFunc {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [Fact (LE.le 1 p)] (f : Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x) : Eq (Norm.norm f) (eLpNorm (DFunLike.coe (toSimpleFunc f)) p μ).toReal

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 : Ne (DFunLike.coe μ s) Top.top) (c : E) : Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x

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.

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 : Ne (DFunLike.coe μ s) Top.top) (c : E) : Eq (indicatorConst p hs hμs c).val (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 : Ne (DFunLike.coe μ s) Top.top) (c : E) : (ae μ).EventuallyEq (DFunLike.coe (toSimpleFunc (indicatorConst p hs hμs c))) (DFunLike.coe (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 : Ne p 0) (hp_ne_top : Ne p Top.top) {P : (Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x) → Prop} (indicatorConst : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (DFunLike.coe μ s) Top.top), P (indicatorConst p hs ⋯ c)) (add : ∀ ⦃f g : SimpleFunc α E⦄ (hf : MemLp (DFunLike.coe f) p μ) (hg : MemLp (DFunLike.coe g) p μ), Disjoint (Function.support (DFunLike.coe f)) (Function.support (DFunLike.coe g)) → P (toLp f hf) → P (toLp g hg) → P (HAdd.hAdd (toLp f hf) (toLp g hg))) (f : Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x) : 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 (LE.le 1 p)] : UniformContinuous Subtype.val

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

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

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

Alias of MeasureTheory.Lp.simpleFunc.isUniformEmbedding.

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

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

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

Alias of MeasureTheory.Lp.simpleFunc.isUniformInducing.

theorem MeasureTheory.Lp.simpleFunc.isDenseEmbedding {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [Fact (LE.le 1 p)] (hp_ne_top : Ne p Top.top) : IsDenseEmbedding Subtype.val

theorem MeasureTheory.Lp.simpleFunc.isDenseInducing {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [Fact (LE.le 1 p)] (hp_ne_top : Ne p Top.top) : IsDenseInducing Subtype.val

theorem MeasureTheory.Lp.simpleFunc.denseRange {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [Fact (LE.le 1 p)] (hp_ne_top : Ne p Top.top) : DenseRange Subtype.val

theorem MeasureTheory.Lp.simpleFunc.dense {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [Fact (LE.le 1 p)] (hp_ne_top : Ne p Top.top) : Dense (SetLike.coe (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 (LE.le 1 p)] [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] : ContinuousLinearMap (RingHom.id 𝕜) (Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => Membership.mem (simpleFunc E p μ) x) (Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x)

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

Equations

• Eq (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} [NormedLatticeAddCommGroup G] (f g : Subtype fun (x : Subtype fun (x : AEEqFun α G μ) => Membership.mem (Lp G p μ) x) => Membership.mem (simpleFunc G p μ) x) : Iff ((ae μ).EventuallyLE f.val.val.cast g.val.val.cast) (LE.le f g)

theorem MeasureTheory.Lp.simpleFunc.instAddLeftMono {α : Type u_1} [MeasurableSpace α] {p : ENNReal} {μ : Measure α} {G : Type u_7} [NormedLatticeAddCommGroup G] : AddLeftMono (Subtype fun (x : Subtype fun (x : AEEqFun α G μ) => Membership.mem (Lp G p μ) x) => Membership.mem (simpleFunc G p μ) x)

theorem MeasureTheory.Lp.simpleFunc.coeFn_zero {α : Type u_1} [MeasurableSpace α] (p : ENNReal) (μ : Measure α) (G : Type u_7) [NormedLatticeAddCommGroup G] : (ae μ).EventuallyEq (Subtype.val 0).val.cast 0

theorem MeasureTheory.Lp.simpleFunc.coeFn_nonneg {α : Type u_1} [MeasurableSpace α] {p : ENNReal} {μ : Measure α} {G : Type u_7} [NormedLatticeAddCommGroup G] (f : Subtype fun (x : Subtype fun (x : AEEqFun α G μ) => Membership.mem (Lp G p μ) x) => Membership.mem (simpleFunc G p μ) x) : Iff ((ae μ).EventuallyLE 0 f.val.val.cast) (LE.le 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 : Subtype fun (x : Subtype fun (x : AEEqFun α G μ) => Membership.mem (Lp G p μ) x) => Membership.mem (simpleFunc G p μ) x} (hf : LE.le 0 f) : Exists fun (f' : SimpleFunc α G) => And (LE.le 0 f') ((ae μ).EventuallyEq f.val.val.cast (DFunLike.coe f'))

def MeasureTheory.Lp.simpleFunc.coeSimpleFuncNonnegToLpNonneg {α : Type u_1} [MeasurableSpace α] (p : ENNReal) (μ : Measure α) (G : Type u_7) [NormedLatticeAddCommGroup G] : (Subtype fun (g : Subtype fun (x : Subtype fun (x : AEEqFun α G μ) => Membership.mem (Lp G p μ) x) => Membership.mem (simpleFunc G p μ) x) => LE.le 0 g) → Subtype fun (g : Subtype fun (x : AEEqFun α G μ) => Membership.mem (Lp G p μ) x) => LE.le 0 g

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

Equations

• Eq (MeasureTheory.Lp.simpleFunc.coeSimpleFuncNonnegToLpNonneg p μ G g) ⟨g.val.val, ⋯⟩

theorem MeasureTheory.Lp.simpleFunc.denseRange_coeSimpleFuncNonnegToLpNonneg {α : Type u_1} [MeasurableSpace α] (p : ENNReal) (μ : Measure α) (G : Type u_7) [NormedLatticeAddCommGroup G] [hp : Fact (LE.le 1 p)] (hp_ne_top : Ne p Top.top) : DenseRange (coeSimpleFuncNonnegToLpNonneg p μ G)

theorem MeasureTheory.Lp.induction {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} [_i : Fact (LE.le 1 p)] (hp_ne_top : Ne p Top.top) (motive : (Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) → Prop) (indicatorConst : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (DFunLike.coe μ s) Top.top), motive (simpleFunc.indicatorConst p hs ⋯ c).val) (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 (HAdd.hAdd (MemLp.toLp f hf) (MemLp.toLp g hg))) (isClosed : IsClosed (setOf fun (f : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => motive f)) (f : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) : 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 (LE.le 1 p)] (hp_ne_top : Ne p Top.top) (motive : (α → E) → Prop) (indicator : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → LT.lt (DFunLike.coe μ s) Top.top → 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 (HAdd.hAdd f g)) (closed : IsClosed (setOf fun (f : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E p μ) x) => motive f.val.cast)) (ae : ∀ ⦃f g : α → E⦄, (ae μ).EventuallyEq 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 : Ne p Top.top) (P : (α → E) → Prop) (h0P : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → LT.lt (DFunLike.coe μ s) Top.top → ∀ {ε : ENNReal}, Ne ε 0 → Exists fun (g : α → E) => And (LE.le (eLpNorm (HSub.hSub g (s.indicator fun (x : α) => c)) p μ) ε) (P g)) (h1P : ∀ (f g : α → E), P f → P g → P (HAdd.hAdd f g)) (h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ) {f : α → E} (hf : MemLp f p μ) {ε : ENNReal} (hε : Ne ε 0) : Exists fun (g : α → E) => And (LE.le (eLpNorm (HSub.hSub 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 (DFunLike.coe f) μ) : Eq (Lp.simpleFunc.toLp f ⋯).val (Integrable.toL1 (DFunLike.coe f) hf)

theorem MeasureTheory.L1.SimpleFunc.integrable {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {μ : Measure α} (f : Subtype fun (x : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E 1 μ) x) => Membership.mem (Lp.simpleFunc E 1 μ) x) : Integrable (DFunLike.coe (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 → LT.lt (DFunLike.coe μ s) Top.top → 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 (HAdd.hAdd f g)) (h_closed : IsClosed (setOf fun (f : Subtype fun (x : AEEqFun α E μ) => Membership.mem (Lp E 1 μ) x) => P f.val.cast)) (h_ae : ∀ ⦃f g : α → E⦄, (ae μ).EventuallyEq 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}).