mathlib documentation

measure_theory.function.simple_func_dense

Density of simple functions #

Show that each Borel measurable function can be approximated pointwise, and 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 #

Pointwise approximation by simple functions #

nearest_pt_ind e N x is the index k such that e k is the nearest point to x among the points e 0, ..., e N. If more than one point are at the same distance from x, then nearest_pt_ind e N x returns the least of their indexes.

Equations

nearest_pt e N x is the nearest point to x among the points e 0, ..., e N. If more than one point are at the same distance from x, then nearest_pt e N x returns the point with the least possible index.

Equations
theorem measure_theory.simple_func.nearest_pt_ind_succ {α : Type u_1} [measurable_space α] [emetric_space α] [opens_measurable_space α] (e : → α) (N : ) (x : α) :
(measure_theory.simple_func.nearest_pt_ind e (N + 1)) x = ite (∀ (k : ), k Nedist (e (N + 1)) x < edist (e k) x) (N + 1) ((measure_theory.simple_func.nearest_pt_ind e N) x)
theorem measure_theory.simple_func.edist_nearest_pt_le {α : Type u_1} [measurable_space α] [emetric_space α] [opens_measurable_space α] (e : → α) (x : α) {k N : } (hk : k N) :
def measure_theory.simple_func.approx_on {α : Type u_1} {β : Type u_2} [measurable_space α] [emetric_space α] [opens_measurable_space α] [measurable_space β] (f : β → α) (hf : measurable f) (s : set α) (y₀ : α) (h₀ : y₀ s) [topological_space.separable_space s] (n : ) :

Approximate a measurable function by a sequence of simple functions F n such that F n x ∈ s.

Equations
@[simp]
theorem measure_theory.simple_func.approx_on_zero {α : Type u_1} {β : Type u_2} [measurable_space α] [emetric_space α] [opens_measurable_space α] [measurable_space β] {f : β → α} (hf : measurable f) {s : set α} {y₀ : α} (h₀ : y₀ s) [topological_space.separable_space s] (x : β) :
(measure_theory.simple_func.approx_on f hf s y₀ h₀ 0) x = y₀
theorem measure_theory.simple_func.approx_on_mem {α : Type u_1} {β : Type u_2} [measurable_space α] [emetric_space α] [opens_measurable_space α] [measurable_space β] {f : β → α} (hf : measurable f) {s : set α} {y₀ : α} (h₀ : y₀ s) [topological_space.separable_space s] (n : ) (x : β) :
@[simp]
theorem measure_theory.simple_func.approx_on_comp {α : Type u_1} {β : Type u_2} [measurable_space α] [emetric_space α] [opens_measurable_space α] [measurable_space β] {γ : Type u_3} [measurable_space γ] {f : β → α} (hf : measurable f) {g : γ → β} (hg : measurable g) {s : set α} {y₀ : α} (h₀ : y₀ s) [topological_space.separable_space s] (n : ) :
theorem measure_theory.simple_func.tendsto_approx_on {α : Type u_1} {β : Type u_2} [measurable_space α] [emetric_space α] [opens_measurable_space α] [measurable_space β] {f : β → α} (hf : measurable f) {s : set α} {y₀ : α} (h₀ : y₀ s) [topological_space.separable_space s] {x : β} (hx : f x closure s) :
theorem measure_theory.simple_func.edist_approx_on_mono {α : Type u_1} {β : Type u_2} [measurable_space α] [emetric_space α] [opens_measurable_space α] [measurable_space β] {f : β → α} (hf : measurable f) {s : set α} {y₀ : α} (h₀ : y₀ s) [topological_space.separable_space s] (x : β) {m n : } (h : m n) :
edist ((measure_theory.simple_func.approx_on f hf s y₀ h₀ n) x) (f x) edist ((measure_theory.simple_func.approx_on f hf s y₀ h₀ m) x) (f x)
theorem measure_theory.simple_func.edist_approx_on_le {α : Type u_1} {β : Type u_2} [measurable_space α] [emetric_space α] [opens_measurable_space α] [measurable_space β] {f : β → α} (hf : measurable f) {s : set α} {y₀ : α} (h₀ : y₀ s) [topological_space.separable_space s] (x : β) (n : ) :
edist ((measure_theory.simple_func.approx_on f hf s y₀ h₀ n) x) (f x) edist y₀ (f x)
theorem measure_theory.simple_func.edist_approx_on_y0_le {α : Type u_1} {β : Type u_2} [measurable_space α] [emetric_space α] [opens_measurable_space α] [measurable_space β] {f : β → α} (hf : measurable f) {s : set α} {y₀ : α} (h₀ : y₀ s) [topological_space.separable_space s] (x : β) (n : ) :
edist y₀ ((measure_theory.simple_func.approx_on f hf s y₀ h₀ n) x) edist y₀ (f x) + edist y₀ (f x)

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_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_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.norm_approx_on_zero_le {β : Type u_2} {E : Type u_4} [measurable_space β] [measurable_space E] [normed_group E] [opens_measurable_space E] {f : β → E} (hf : measurable f) {s : set E} (h₀ : 0 s) [topological_space.separable_space s] (x : β) (n : ) :
theorem measure_theory.simple_func.tendsto_approx_on_Lp_snorm {β : Type u_2} {E : Type u_4} [measurable_space β] [measurable_space E] [normed_group E] {p : ℝ≥0∞} [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_group E] {p : ℝ≥0∞} [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 : ) :

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

theorem measure_theory.simple_func.exists_forall_norm_le {α : Type u_1} {F : Type u_5} [measurable_space α] [normed_group F] (f : measure_theory.simple_func α F) :
∃ (C : ), ∀ (x : α), f x C
theorem measure_theory.simple_func.snorm'_eq {α : Type u_1} {F : Type u_5} [measurable_space α] [normed_group F] {p : } (f : measure_theory.simple_func α F) (μ : measure_theory.measure α) :
measure_theory.snorm' f p μ = (∑ (y : F) in f.range, (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_group E] [measurable_space E] {μ : measure_theory.measure α} {p : ℝ≥0∞} (hp_pos : 0 < p) (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_group E] [measurable_space E] {μ : measure_theory.measure α} {p : ℝ≥0∞} {f : measure_theory.simple_func α E} (hp_pos : 0 < p) (hp_ne_top : p ) :
measure_theory.mem_ℒp f p μ ∀ (y : E), y 0μ (f ⁻¹' {y}) <
theorem measure_theory.simple_func.integrable_iff {α : Type u_1} {E : Type u_4} [measurable_space α] [normed_group E] [measurable_space E] {μ : measure_theory.measure α} {f : measure_theory.simple_func α E} :
measure_theory.integrable f μ ∀ (y : E), y 0μ (f ⁻¹' {y}) <
theorem measure_theory.simple_func.mem_ℒp_iff_fin_meas_supp {α : Type u_1} {E : Type u_4} [measurable_space α] [normed_group E] [measurable_space E] {μ : measure_theory.measure α} {p : ℝ≥0∞} {f : measure_theory.simple_func α E} (hp_pos : 0 < p) (hp_ne_top : p ) :
theorem measure_theory.simple_func.measure_support_lt_top {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [has_zero β] (f : measure_theory.simple_func α β) (hf : ∀ (y : β), y 0μ (f ⁻¹' {y}) < ) :
theorem measure_theory.simple_func.measure_support_lt_top_of_mem_ℒp {α : Type u_1} {E : Type u_4} [measurable_space α] [normed_group E] [measurable_space E] {μ : measure_theory.measure α} {p : ℝ≥0∞} (f : measure_theory.simple_func α E) (hf : measure_theory.mem_ℒp f p μ) (hp_ne_zero : p 0) (hp_ne_top : p ) :

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

Simple functions in Lp space form a normed_space.

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

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

Equations
@[simp]

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

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

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

Equations

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

Equations

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

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

Equations
theorem measure_theory.Lp.induction {α : Type u_1} {E : Type u_4} [measurable_space α] [normed_group E] [measurable_space E] [borel_space E] [topological_space.second_countable_topology E] {p : ℝ≥0∞} {μ : 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_group E] [measurable_space E] [borel_space E] [topological_space.second_countable_topology E] {p : ℝ≥0∞} {μ : 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 fP gP (f + g)) (h_closed : is_closed {f : (measure_theory.Lp E p μ) | P f}) (h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] gmeasure_theory.mem_ℒp f p μP fP 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.integrable.induction {α : Type u_1} {E : Type u_4} [measurable_space α] [normed_group E] [measurable_space E] [borel_space E] [topological_space.second_countable_topology 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 fP gP (f + g)) (h_closed : is_closed {f : (measure_theory.Lp E 1 μ) | P f}) (h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] gmeasure_theory.integrable f μP fP g) ⦃f : α → E⦄ (hf : measure_theory.integrable f μ) :
P f

To prove something for an arbitrary integrable 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 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}).