mathlib3 documentation

measure_theory.function.simple_func_dense_lp

Density of simple functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions #

Main results #

TODO #

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

Notations #

Lp approximation by simple functions #

theorem measure_theory.simple_func.nnnorm_approx_on_le {β : Type u_2} {E : Type u_4} [measurable_space β] [measurable_space E] [normed_add_comm_group E] [opens_measurable_space E] {f : β E} (hf : measurable f) {s : set E} {y₀ : E} (h₀ : y₀ s) [topological_space.separable_space s] (x : β) (n : ) :
theorem measure_theory.simple_func.norm_approx_on_y₀_le {β : Type u_2} {E : Type u_4} [measurable_space β] [measurable_space E] [normed_add_comm_group E] [opens_measurable_space E] {f : β E} (hf : measurable f) {s : set E} {y₀ : E} (h₀ : y₀ s) [topological_space.separable_space s] (x : β) (n : ) :
(measure_theory.simple_func.approx_on f hf s y₀ h₀ n) x - y₀ f x - y₀ + f x - y₀
theorem measure_theory.simple_func.tendsto_approx_on_Lp_snorm {β : Type u_2} {E : Type u_4} [measurable_space β] [measurable_space E] [normed_add_comm_group E] {p : ennreal} [opens_measurable_space E] {f : β E} (hf : measurable f) {s : set E} {y₀ : E} (h₀ : y₀ s) [topological_space.separable_space s] (hp_ne_top : p ) {μ : measure_theory.measure β} (hμ : ∀ᵐ (x : β) μ, f x closure s) (hi : measure_theory.snorm (λ (x : β), f x - y₀) p μ < ) :
theorem measure_theory.simple_func.mem_ℒp_approx_on {β : Type u_2} {E : Type u_4} [measurable_space β] [measurable_space E] [normed_add_comm_group E] {p : ennreal} [borel_space E] {f : β E} {μ : measure_theory.measure β} (fmeas : measurable f) (hf : measure_theory.mem_ℒp f p μ) {s : set E} {y₀ : E} (h₀ : y₀ s) [topological_space.separable_space s] (hi₀ : measure_theory.mem_ℒp (λ (x : β), y₀) p μ) (n : ) :
theorem measure_theory.mem_ℒp.exists_simple_func_snorm_sub_lt {β : Type u_2} [measurable_space β] {p : ennreal} {E : Type u_1} [normed_add_comm_group E] {f : β E} {μ : measure_theory.measure β} (hf : measure_theory.mem_ℒp f p μ) (hp_ne_top : p ) {ε : ennreal} (hε : ε 0) :

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

L1 approximation by simple functions #

theorem measure_theory.simple_func.tendsto_approx_on_L1_nnnorm {β : Type u_2} {E : Type u_4} [measurable_space β] [measurable_space E] [normed_add_comm_group E] [opens_measurable_space E] {f : β E} (hf : measurable f) {s : set E} {y₀ : E} (h₀ : y₀ s) [topological_space.separable_space s] {μ : measure_theory.measure β} (hμ : ∀ᵐ (x : β) μ, f x closure s) (hi : measure_theory.has_finite_integral (λ (x : β), f x - y₀) μ) :
theorem measure_theory.simple_func.integrable_approx_on {β : Type u_2} {E : Type u_4} [measurable_space β] [measurable_space E] [normed_add_comm_group E] [borel_space E] {f : β E} {μ : measure_theory.measure β} (fmeas : measurable f) (hf : measure_theory.integrable f μ) {s : set E} {y₀ : E} (h₀ : y₀ s) [topological_space.separable_space s] (hi₀ : measure_theory.integrable (λ (x : β), y₀) μ) (n : ) :

Properties of simple functions in Lp spaces #

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

@[protected]
theorem measure_theory.simple_func.snorm'_eq {α : Type u_1} {F : Type u_5} [measurable_space α] [normed_add_comm_group F] {p : } (f : measure_theory.simple_func α F) (μ : measure_theory.measure α) :
measure_theory.snorm' f p μ = f.range.sum (λ (y : F), y‖₊ ^ p * μ (f ⁻¹' {y})) ^ (1 / p)
theorem measure_theory.simple_func.measure_preimage_lt_top_of_mem_ℒp {α : Type u_1} {E : Type u_4} [measurable_space α] [normed_add_comm_group E] {μ : measure_theory.measure α} {p : ennreal} (hp_pos : p 0) (hp_ne_top : p ) (f : measure_theory.simple_func α E) (hf : measure_theory.mem_ℒp f p μ) (y : E) (hy_ne : y 0) :
μ (f ⁻¹' {y}) <
theorem measure_theory.simple_func.mem_ℒp_iff {α : Type u_1} {E : Type u_4} [measurable_space α] [normed_add_comm_group E] {μ : measure_theory.measure α} {p : ennreal} {f : measure_theory.simple_func α E} (hp_pos : p 0) (hp_ne_top : p ) :
measure_theory.mem_ℒp f p μ (y : E), y 0 μ (f ⁻¹' {y}) <

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

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

Equations
Instances for measure_theory.Lp.simple_func

Simple functions in Lp space form a normed_space.

@[protected]

Implementation note: If Lp.simple_func E p μ were defined as a 𝕜-submodule of Lp E p μ, then the next few lemmas, putting a normed 𝕜-group structure on Lp.simple_func E p μ, would be unnecessary. But instead, Lp.simple_func E p μ is defined as an add_subgroup 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).

@[protected]

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

Equations
@[simp, norm_cast]
theorem measure_theory.Lp.simple_func.coe_smul {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [measurable_space α] [normed_add_comm_group E] {p : ennreal} {μ : measure_theory.measure α} [normed_ring 𝕜] [module 𝕜 E] [has_bounded_smul 𝕜 E] (c : 𝕜) (f : (measure_theory.Lp.simple_func E p μ)) :
(c f) = c f
@[protected]

If E is a normed space, Lp.simple_func 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
@[protected]

If E is a normed space, Lp.simple_func 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.

@[protected]

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

Equations
@[reducible]

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

Equations
@[protected, measurability]

(to_simple_func f) is measurable.

@[protected]

to_simple_func f satisfies the predicate mem_ℒp.

noncomputable def measure_theory.Lp.simple_func.indicator_const {α : Type u_1} {E : Type u_4} [measurable_space α] [normed_add_comm_group E] (p : ennreal) {μ : measure_theory.measure α} {s : set α} (hs : measurable_set s) (hμs : μ s ) (c : E) :

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

Equations
@[protected]

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

@[protected]
@[protected]
@[protected]
theorem measure_theory.Lp.simple_func.dense_range {α : Type u_1} {E : Type u_4} [measurable_space α] [normed_add_comm_group E] {p : ennreal} {μ : measure_theory.measure α} [fact (1 p)] (hp_ne_top : p ) :

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

Equations

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

Equations
theorem measure_theory.Lp.induction {α : Type u_1} {E : Type u_4} [measurable_space α] [normed_add_comm_group E] {p : ennreal} {μ : measure_theory.measure α} [fact (1 p)] (hp_ne_top : p ) (P : (measure_theory.Lp E p μ) Prop) (h_ind : (c : E) {s : set α} (hs : measurable_set s) (hμs : μ s < ), P (measure_theory.Lp.simple_func.indicator_const p hs _ c)) (h_add : ⦃f g : α E⦄ (hf : measure_theory.mem_ℒp f p μ) (hg : measure_theory.mem_ℒp g p μ), disjoint (function.support f) (function.support g) P (measure_theory.mem_ℒp.to_Lp f hf) P (measure_theory.mem_ℒp.to_Lp g hg) P (measure_theory.mem_ℒp.to_Lp f hf + measure_theory.mem_ℒp.to_Lp g hg)) (h_closed : is_closed {f : (measure_theory.Lp E p μ) | P f}) (f : (measure_theory.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 measure_theory.mem_ℒp.induction {α : Type u_1} {E : Type u_4} [measurable_space α] [normed_add_comm_group E] {p : ennreal} {μ : measure_theory.measure α} [fact (1 p)] (hp_ne_top : p ) (P : E) Prop) (h_ind : (c : E) ⦃s : set α⦄, measurable_set s μ s < P (s.indicator (λ (_x : α), c))) (h_add : ⦃f g : α E⦄, disjoint (function.support f) (function.support g) measure_theory.mem_ℒp f p μ measure_theory.mem_ℒp g p μ P f P g P (f + g)) (h_closed : is_closed {f : (measure_theory.Lp E p μ) | P f}) (h_ae : ⦃f g : α E⦄, f =ᵐ[μ] g measure_theory.mem_ℒp f p μ P f P g) ⦃f : α E⦄ (hf : measure_theory.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 measure_theory.mem_ℒp.induction_dense {α : Type u_1} {E : Type u_4} [measurable_space α] [normed_add_comm_group E] {p : ennreal} {μ : measure_theory.measure α} (hp_ne_top : p ) (P : E) Prop) (h0P : (c : E) ⦃s : set α⦄, measurable_set s μ s < {ε : ennreal}, ε 0 ( (g : α E), measure_theory.snorm (g - s.indicator (λ (x : α), c)) p μ ε P g)) (h1P : (f g : α E), P f P g P (f + g)) (h2P : (f : α E), P f measure_theory.ae_strongly_measurable f μ) {f : α E} (hf : measure_theory.mem_ℒp f p μ) {ε : ennreal} (hε : ε 0) :
(g : α E), measure_theory.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.

theorem measure_theory.integrable.induction {α : Type u_1} {E : Type u_4} [measurable_space α] [normed_add_comm_group E] {μ : measure_theory.measure α} (P : E) Prop) (h_ind : (c : E) ⦃s : set α⦄, measurable_set s μ s < P (s.indicator (λ (_x : α), c))) (h_add : ⦃f g : α E⦄, disjoint (function.support f) (function.support g) measure_theory.integrable f μ measure_theory.integrable g μ P f P g P (f + g)) (h_closed : is_closed {f : (measure_theory.Lp E 1 μ) | P f}) (h_ae : ⦃f g : α E⦄, f =ᵐ[μ] g measure_theory.integrable f μ P f P g) ⦃f : α E⦄ (hf : measure_theory.integrable f μ) :
P f

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

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

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