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 #
measure_theory.Lp.simple_func, the type ofLpsimple functionscoe_to_Lp, the embedding ofLp.simple_func E p μintoLp E p μ
Main results #
tendsto_approx_on_univ_Lp(Lᵖ convergence): IfEis anormed_add_comm_groupandfis measurable andmem_ℒp(forp < ∞), then the simple functionssimple_func.approx_on f hf s 0 h₀ nmay be considered as elements ofLp E p μ, and they tend in Lᵖ tof.Lp.simple_func.dense_embedding: the embeddingcoe_to_Lpof theLpsimple functions intoLpis dense.Lp.simple_func.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 ofL1simple functionsα → β.
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 : ℕ) :
theorem
measure_theory.simple_func.norm_approx_on_zero_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}
(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_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 μ < ⊤) :
filter.tendsto (λ (n : ℕ), measure_theory.snorm (⇑(measure_theory.simple_func.approx_on f hf s y₀ h₀ n) - f) p μ) filter.at_top (nhds 0)
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 : ℕ) :
measure_theory.mem_ℒp ⇑(measure_theory.simple_func.approx_on f fmeas s y₀ h₀ n) p μ
theorem
measure_theory.simple_func.tendsto_approx_on_range_Lp_snorm
{β : Type u_2}
{E : Type u_4}
[measurable_space β]
[measurable_space E]
[normed_add_comm_group E]
{p : ennreal}
[borel_space E]
{f : β → E}
(hp_ne_top : p ≠ ⊤)
{μ : measure_theory.measure β}
(fmeas : measurable f)
[topological_space.separable_space ↥(set.range f ∪ {0})]
(hf : measure_theory.snorm f p μ < ⊤) :
filter.tendsto (λ (n : ℕ), measure_theory.snorm (⇑(measure_theory.simple_func.approx_on f fmeas (set.range f ∪ {0}) 0 _ n) - f) p μ) filter.at_top (nhds 0)
theorem
measure_theory.simple_func.mem_ℒp_approx_on_range
{β : 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)
[topological_space.separable_space ↥(set.range f ∪ {0})]
(hf : measure_theory.mem_ℒp f p μ)
(n : ℕ) :
measure_theory.mem_ℒp ⇑(measure_theory.simple_func.approx_on f fmeas (set.range f ∪ {0}) 0 _ n) p μ
theorem
measure_theory.simple_func.tendsto_approx_on_range_Lp
{β : Type u_2}
{E : Type u_4}
[measurable_space β]
[measurable_space E]
[normed_add_comm_group E]
{p : ennreal}
[borel_space E]
{f : β → E}
[hp : fact (1 ≤ p)]
(hp_ne_top : p ≠ ⊤)
{μ : measure_theory.measure β}
(fmeas : measurable f)
[topological_space.separable_space ↥(set.range f ∪ {0})]
(hf : measure_theory.mem_ℒp f p μ) :
filter.tendsto (λ (n : ℕ), measure_theory.mem_ℒp.to_Lp ⇑(measure_theory.simple_func.approx_on f fmeas (set.range f ∪ {0}) 0 _ n) _) filter.at_top (nhds (measure_theory.mem_ℒp.to_Lp f hf))
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) :
∃ (g : measure_theory.simple_func β E), measure_theory.snorm (f - ⇑g) p μ < ε ∧ measure_theory.mem_ℒp ⇑g p μ
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₀) μ) :
filter.tendsto (λ (n : ℕ), ∫⁻ (x : β), ↑‖⇑(measure_theory.simple_func.approx_on f hf s y₀ h₀ n) x - f x‖₊ ∂μ) filter.at_top (nhds 0)
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 : ℕ) :
measure_theory.integrable ⇑(measure_theory.simple_func.approx_on f fmeas s y₀ h₀ n) μ
theorem
measure_theory.simple_func.tendsto_approx_on_range_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}
{μ : measure_theory.measure β}
[topological_space.separable_space ↥(set.range f ∪ {0})]
(fmeas : measurable f)
(hf : measure_theory.integrable f μ) :
filter.tendsto (λ (n : ℕ), ∫⁻ (x : β), ↑‖⇑(measure_theory.simple_func.approx_on f fmeas (set.range f ∪ {0}) 0 _ n) x - f x‖₊ ∂μ) filter.at_top (nhds 0)
theorem
measure_theory.simple_func.integrable_approx_on_range
{β : 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)
[topological_space.separable_space ↥(set.range f ∪ {0})]
(hf : measure_theory.integrable f μ)
(n : ℕ) :
measure_theory.integrable ⇑(measure_theory.simple_func.approx_on 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 μandmem_ℒp f ∞ μ, sincefis a.e.-measurable and bounded,- for
0 < p < ∞,mem_ℒp f p μ ↔ integrable f μ ↔ f.fin_meas_supp μ ↔ ∀ y ≠ 0, μ (f ⁻¹' {y}) < ∞.
theorem
measure_theory.simple_func.exists_forall_norm_le
{α : Type u_1}
{F : Type u_5}
[measurable_space α]
[normed_add_comm_group F]
(f : measure_theory.simple_func α F) :
theorem
measure_theory.simple_func.mem_ℒp_zero
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
(f : measure_theory.simple_func α E)
(μ : measure_theory.measure α) :
measure_theory.mem_ℒp ⇑f 0 μ
theorem
measure_theory.simple_func.mem_ℒp_top
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
(f : measure_theory.simple_func α E)
(μ : measure_theory.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 α) :
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) :
theorem
measure_theory.simple_func.mem_ℒp_of_finite_measure_preimage
{α : 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}
(hf : ∀ (y : E), y ≠ 0 → ⇑μ (⇑f ⁻¹' {y}) < ⊤) :
measure_theory.mem_ℒp ⇑f p μ
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 ≠ ⊤) :
theorem
measure_theory.simple_func.integrable_iff
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{μ : measure_theory.measure α}
{f : measure_theory.simple_func α E} :
theorem
measure_theory.simple_func.mem_ℒp_iff_integrable
{α : 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 ≠ ⊤) :
theorem
measure_theory.simple_func.mem_ℒp_iff_fin_meas_supp
{α : 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 μ ↔ f.fin_meas_supp μ
theorem
measure_theory.simple_func.integrable_iff_fin_meas_supp
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{μ : measure_theory.measure α}
{f : measure_theory.simple_func α E} :
measure_theory.integrable ⇑f μ ↔ f.fin_meas_supp μ
theorem
measure_theory.simple_func.fin_meas_supp.integrable
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{μ : measure_theory.measure α}
{f : measure_theory.simple_func α E}
(h : f.fin_meas_supp μ) :
theorem
measure_theory.simple_func.integrable_pair
{α : Type u_1}
{E : Type u_4}
{F : Type u_5}
[measurable_space α]
[normed_add_comm_group E]
[normed_add_comm_group F]
{μ : measure_theory.measure α}
{f : measure_theory.simple_func α E}
{g : measure_theory.simple_func α F} :
measure_theory.integrable ⇑f μ → measure_theory.integrable ⇑g μ → measure_theory.integrable ⇑(f.pair g) μ
theorem
measure_theory.simple_func.mem_ℒp_of_is_finite_measure
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
(f : measure_theory.simple_func α E)
(p : ennreal)
(μ : measure_theory.measure α)
[measure_theory.is_finite_measure μ] :
measure_theory.mem_ℒp ⇑f p μ
theorem
measure_theory.simple_func.integrable_of_is_finite_measure
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{μ : measure_theory.measure α}
[measure_theory.is_finite_measure μ]
(f : measure_theory.simple_func α E) :
theorem
measure_theory.simple_func.measure_preimage_lt_top_of_integrable
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{μ : measure_theory.measure α}
(f : measure_theory.simple_func α E)
(hf : measure_theory.integrable ⇑f μ)
{x : E}
(hx : x ≠ 0) :
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}) < ⊤) :
⇑μ (function.support ⇑f) < ⊤
theorem
measure_theory.simple_func.measure_support_lt_top_of_mem_ℒp
{α : 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)
(hf : measure_theory.mem_ℒp ⇑f p μ)
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤) :
⇑μ (function.support ⇑f) < ⊤
theorem
measure_theory.simple_func.measure_support_lt_top_of_integrable
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{μ : measure_theory.measure α}
(f : measure_theory.simple_func α E)
(hf : measure_theory.integrable ⇑f μ) :
⇑μ (function.support ⇑f) < ⊤
theorem
measure_theory.simple_func.measure_lt_top_of_mem_ℒp_indicator
{α : 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 ≠ ⊤)
{c : E}
(hc : c ≠ 0)
{s : set α}
(hs : measurable_set s)
(hcs : measure_theory.mem_ℒp ⇑(measure_theory.simple_func.piecewise s hs (measure_theory.simple_func.const α c) (measure_theory.simple_func.const α 0)) p μ) :
Construction of the space of Lp simple functions, and its dense embedding into Lp.
def
measure_theory.Lp.simple_func
{α : Type u_1}
(E : Type u_4)
[measurable_space α]
[normed_add_comm_group E]
(p : ennreal)
(μ : measure_theory.measure α) :
add_subgroup ↥(measure_theory.Lp E p μ)
Lp.simple_func is a subspace of Lp consisting of equivalence classes of an integrable simple
function.
Equations
- measure_theory.Lp.simple_func E p μ = {carrier := {f : ↥(measure_theory.Lp E p μ) | ∃ (s : measure_theory.simple_func α E), measure_theory.ae_eq_fun.mk ⇑s _ = ↑f}, add_mem' := _, zero_mem' := _, neg_mem' := _}
Instances for ↥measure_theory.Lp.simple_func
Simple functions in Lp space form a normed_space.
@[norm_cast]
theorem
measure_theory.Lp.simple_func.coe_coe
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
(f : ↥(measure_theory.Lp.simple_func E p μ)) :
@[protected]
theorem
measure_theory.Lp.simple_func.eq'
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
{f g : ↥(measure_theory.Lp.simple_func E p μ)} :
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]
def
measure_theory.Lp.simple_func.has_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] :
has_smul 𝕜 ↥(measure_theory.Lp.simple_func E p μ)
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
- measure_theory.Lp.simple_func.has_smul = {smul := λ (k : 𝕜) (f : ↥(measure_theory.Lp.simple_func E p μ)), ⟨k • ↑f, _⟩}
@[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 μ)) :
@[protected]
def
measure_theory.Lp.simple_func.module
{α : 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] :
module 𝕜 ↥(measure_theory.Lp.simple_func E p μ)
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
- measure_theory.Lp.simple_func.module = {to_distrib_mul_action := {to_mul_action := {to_has_smul := measure_theory.Lp.simple_func.has_smul _inst_6, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, add_smul := _, zero_smul := _}
@[protected]
theorem
measure_theory.Lp.simple_func.has_bounded_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]
[fact (1 ≤ p)] :
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]
def
measure_theory.Lp.simple_func.normed_space
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
{𝕜 : Type u_2}
[normed_field 𝕜]
[normed_space 𝕜 E]
[fact (1 ≤ p)] :
normed_space 𝕜 ↥(measure_theory.Lp.simple_func E p μ)
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
- measure_theory.Lp.simple_func.normed_space = {to_module := measure_theory.Lp.simple_func.module measure_theory.Lp.simple_func.normed_space._proof_1, norm_smul_le := _}
@[reducible]
def
measure_theory.Lp.simple_func.to_Lp
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
(f : measure_theory.simple_func α E)
(hf : measure_theory.mem_ℒp ⇑f p μ) :
↥(measure_theory.Lp.simple_func E p μ)
Construct the equivalence class [f] of a simple function f satisfying mem_ℒp.
Equations
theorem
measure_theory.Lp.simple_func.to_Lp_eq_to_Lp
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
(f : measure_theory.simple_func α E)
(hf : measure_theory.mem_ℒp ⇑f p μ) :
theorem
measure_theory.Lp.simple_func.to_Lp_eq_mk
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
(f : measure_theory.simple_func α E)
(hf : measure_theory.mem_ℒp ⇑f p μ) :
theorem
measure_theory.Lp.simple_func.to_Lp_zero
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α} :
theorem
measure_theory.Lp.simple_func.to_Lp_add
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
(f g : measure_theory.simple_func α E)
(hf : measure_theory.mem_ℒp ⇑f p μ)
(hg : measure_theory.mem_ℒp ⇑g p μ) :
theorem
measure_theory.Lp.simple_func.to_Lp_neg
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
(f : measure_theory.simple_func α E)
(hf : measure_theory.mem_ℒp ⇑f p μ) :
theorem
measure_theory.Lp.simple_func.to_Lp_sub
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
(f g : measure_theory.simple_func α E)
(hf : measure_theory.mem_ℒp ⇑f p μ)
(hg : measure_theory.mem_ℒp ⇑g p μ) :
theorem
measure_theory.Lp.simple_func.to_Lp_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]
(f : measure_theory.simple_func α E)
(hf : measure_theory.mem_ℒp ⇑f p μ)
(c : 𝕜) :
measure_theory.Lp.simple_func.to_Lp (c • f) _ = c • measure_theory.Lp.simple_func.to_Lp f hf
theorem
measure_theory.Lp.simple_func.norm_to_Lp
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
[fact (1 ≤ p)]
(f : measure_theory.simple_func α E)
(hf : measure_theory.mem_ℒp ⇑f p μ) :
noncomputable
def
measure_theory.Lp.simple_func.to_simple_func
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
(f : ↥(measure_theory.Lp.simple_func E p μ)) :
Find a representative of a Lp.simple_func.
Equations
@[protected, measurability]
theorem
measure_theory.Lp.simple_func.measurable
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
[measurable_space E]
(f : ↥(measure_theory.Lp.simple_func E p μ)) :
(to_simple_func f) is measurable.
@[protected]
theorem
measure_theory.Lp.simple_func.strongly_measurable
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
(f : ↥(measure_theory.Lp.simple_func E p μ)) :
@[protected, measurability]
theorem
measure_theory.Lp.simple_func.ae_measurable
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
[measurable_space E]
(f : ↥(measure_theory.Lp.simple_func E p μ)) :
@[protected]
theorem
measure_theory.Lp.simple_func.ae_strongly_measurable
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
(f : ↥(measure_theory.Lp.simple_func E p μ)) :
theorem
measure_theory.Lp.simple_func.to_simple_func_eq_to_fun
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
(f : ↥(measure_theory.Lp.simple_func E p μ)) :
@[protected]
theorem
measure_theory.Lp.simple_func.mem_ℒp
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
(f : ↥(measure_theory.Lp.simple_func E p μ)) :
to_simple_func f satisfies the predicate mem_ℒp.
theorem
measure_theory.Lp.simple_func.to_Lp_to_simple_func
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
(f : ↥(measure_theory.Lp.simple_func E p μ)) :
theorem
measure_theory.Lp.simple_func.to_simple_func_to_Lp
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
(f : measure_theory.simple_func α E)
(hfi : measure_theory.mem_ℒp ⇑f p μ) :
theorem
measure_theory.Lp.simple_func.zero_to_simple_func
{α : Type u_1}
(E : Type u_4)
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
(μ : measure_theory.measure α) :
theorem
measure_theory.Lp.simple_func.add_to_simple_func
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
(f g : ↥(measure_theory.Lp.simple_func E p μ)) :
theorem
measure_theory.Lp.simple_func.neg_to_simple_func
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
(f : ↥(measure_theory.Lp.simple_func E p μ)) :
theorem
measure_theory.Lp.simple_func.sub_to_simple_func
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
(f g : ↥(measure_theory.Lp.simple_func E p μ)) :
theorem
measure_theory.Lp.simple_func.smul_to_simple_func
{α : 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]
(k : 𝕜)
(f : ↥(measure_theory.Lp.simple_func E p μ)) :
theorem
measure_theory.Lp.simple_func.norm_to_simple_func
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
[fact (1 ≤ p)]
(f : ↥(measure_theory.Lp.simple_func E 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) :
↥(measure_theory.Lp.simple_func E p μ)
The characteristic function of a finite-measure measurable set s, as an Lp simple function.
Equations
@[simp]
theorem
measure_theory.Lp.simple_func.coe_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) :
↑(measure_theory.Lp.simple_func.indicator_const p hs hμs c) = measure_theory.indicator_const_Lp p hs hμs c
theorem
measure_theory.Lp.simple_func.to_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) :
@[protected]
theorem
measure_theory.Lp.simple_func.induction
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
(hp_pos : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
{P : ↥(measure_theory.Lp.simple_func 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 : measure_theory.simple_func α 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.Lp.simple_func.to_Lp f hf) → P (measure_theory.Lp.simple_func.to_Lp g hg) → P (measure_theory.Lp.simple_func.to_Lp f hf + measure_theory.Lp.simple_func.to_Lp g hg))
(f : ↥(measure_theory.Lp.simple_func 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).
@[protected]
theorem
measure_theory.Lp.simple_func.uniform_continuous
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
[fact (1 ≤ p)] :
@[protected]
theorem
measure_theory.Lp.simple_func.uniform_embedding
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
[fact (1 ≤ p)] :
@[protected]
theorem
measure_theory.Lp.simple_func.uniform_inducing
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
[fact (1 ≤ p)] :
@[protected]
theorem
measure_theory.Lp.simple_func.dense_embedding
{α : 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 ≠ ⊤) :
@[protected]
theorem
measure_theory.Lp.simple_func.dense_inducing
{α : 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 ≠ ⊤) :
@[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 ≠ ⊤) :
def
measure_theory.Lp.simple_func.coe_to_Lp
(α : Type u_1)
(E : Type u_4)
(𝕜 : Type u_6)
[measurable_space α]
[normed_add_comm_group E]
{p : ennreal}
{μ : measure_theory.measure α}
[fact (1 ≤ p)]
[normed_ring 𝕜]
[module 𝕜 E]
[has_bounded_smul 𝕜 E] :
↥(measure_theory.Lp.simple_func E p μ) →L[𝕜] ↥(measure_theory.Lp E p μ)
The embedding of Lp simple functions into Lp functions, as a continuous linear map.
Equations
- measure_theory.Lp.simple_func.coe_to_Lp α E 𝕜 = {to_linear_map := {to_fun := (measure_theory.Lp.simple_func E p μ).subtype.to_fun, map_add' := _, map_smul' := _}, cont := _}
theorem
measure_theory.Lp.simple_func.coe_fn_le
{α : Type u_1}
[measurable_space α]
{p : ennreal}
{μ : measure_theory.measure α}
{G : Type u_7}
[normed_lattice_add_comm_group G]
(f g : ↥(measure_theory.Lp.simple_func G p μ)) :
@[protected, instance]
def
measure_theory.Lp.simple_func.has_le.le.covariant_class
{α : Type u_1}
[measurable_space α]
{p : ennreal}
{μ : measure_theory.measure α}
{G : Type u_7}
[normed_lattice_add_comm_group G] :
theorem
measure_theory.Lp.simple_func.coe_fn_zero
{α : Type u_1}
[measurable_space α]
(p : ennreal)
(μ : measure_theory.measure α)
(G : Type u_7)
[normed_lattice_add_comm_group G] :
theorem
measure_theory.Lp.simple_func.coe_fn_nonneg
{α : Type u_1}
[measurable_space α]
{p : ennreal}
{μ : measure_theory.measure α}
{G : Type u_7}
[normed_lattice_add_comm_group G]
(f : ↥(measure_theory.Lp.simple_func G p μ)) :
theorem
measure_theory.Lp.simple_func.exists_simple_func_nonneg_ae_eq
{α : Type u_1}
[measurable_space α]
{p : ennreal}
{μ : measure_theory.measure α}
{G : Type u_7}
[normed_lattice_add_comm_group G]
{f : ↥(measure_theory.Lp.simple_func G p μ)}
(hf : 0 ≤ f) :
def
measure_theory.Lp.simple_func.coe_simple_func_nonneg_to_Lp_nonneg
{α : Type u_1}
[measurable_space α]
(p : ennreal)
(μ : measure_theory.measure α)
(G : Type u_7)
[normed_lattice_add_comm_group G] :
Coercion from nonnegative simple functions of Lp to nonnegative functions of Lp.
Equations
- measure_theory.Lp.simple_func.coe_simple_func_nonneg_to_Lp_nonneg p μ G = λ (g : {g // 0 ≤ g}), ⟨↑g, _⟩
theorem
measure_theory.Lp.simple_func.dense_range_coe_simple_func_nonneg_to_Lp_nonneg
{α : Type u_1}
[measurable_space α]
(p : ennreal)
(μ : measure_theory.measure α)
(G : Type u_7)
[normed_lattice_add_comm_group G]
[hp : fact (1 ≤ p)]
(hp_ne_top : p ≠ ⊤) :
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
Lpfor 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) :
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.L1.simple_func.to_Lp_one_eq_to_L1
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{μ : measure_theory.measure α}
(f : measure_theory.simple_func α E)
(hf : measure_theory.integrable ⇑f μ) :
@[protected]
theorem
measure_theory.L1.simple_func.integrable
{α : Type u_1}
{E : Type u_4}
[measurable_space α]
[normed_add_comm_group E]
{μ : measure_theory.measure α}
(f : ↥(measure_theory.Lp.simple_func E 1 μ)) :
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
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}).