mathlib documentation

measure_theory.function.strongly_measurable

Strongly measurable and finitely strongly measurable functions #

A function f is said to be strongly measurable if f is the sequential limit of simple functions. It is said to be finitely strongly measurable with respect to a measure μ if the supports of those simple functions have finite measure.

If the target space has a second countable topology, strongly measurable and measurable are equivalent.

Functions in Lp for 0 < p < ∞ are finitely strongly measurable. If the measure is sigma-finite, strongly measurable and finitely strongly measurable are equivalent.

The main property of finitely strongly measurable functions is fin_strongly_measurable.exists_set_sigma_finite: there exists a measurable set t such that the function is supported on t and μ.restrict t is sigma-finite. As a consequence, we can prove some results for those functions as if the measure was sigma-finite.

Main definitions #

Main statements #

References #

def measure_theory.strongly_measurable {α : Type u_1} {β : Type u_2} [topological_space β] [measurable_space α] (f : α → β) :
Prop

A function is strongly_measurable if it is the limit of simple functions.

Equations
def measure_theory.fin_strongly_measurable {α : Type u_1} {β : Type u_2} [topological_space β] [has_zero β] {m0 : measurable_space α} (f : α → β) (μ : measure_theory.measure α) :
Prop

A function is fin_strongly_measurable with respect to a measure if it is the limit of simple functions with support with finite measure.

Equations
def measure_theory.ae_fin_strongly_measurable {α : Type u_1} {β : Type u_2} [topological_space β] [has_zero β] {m0 : measurable_space α} (f : α → β) (μ : measure_theory.measure α) :
Prop

A function is ae_fin_strongly_measurable with respect to a measure if it is almost everywhere equal to the limit of a sequence of simple functions with support with finite measure.

Equations

Strongly measurable functions #

A sequence of simple functions such that ∀ x, tendsto (λ n, hf.approx n x) at_top (𝓝 (f x)). That property is given by strongly_measurable.tendsto_approx.

Equations
theorem measure_theory.strongly_measurable.tendsto_approx {α : Type u_1} {β : Type u_2} {f : α → β} [measurable_space α] [topological_space β] (hf : measure_theory.strongly_measurable f) (x : α) :
filter.tendsto (λ (n : ), (hf.approx n) x) filter.at_top (𝓝 (f x))
theorem measure_theory.strongly_measurable.fin_strongly_measurable_of_set_sigma_finite {α : Type u_1} {β : Type u_2} {f : α → β} [topological_space β] [has_zero β] {m : measurable_space α} {μ : measure_theory.measure α} (hf_meas : measure_theory.strongly_measurable f) {t : set α} (ht : measurable_set t) (hft_zero : ∀ (x : α), x tf x = 0) (htμ : measure_theory.sigma_finite (μ.restrict t)) :

If the measure is sigma-finite, all strongly measurable functions are fin_strongly_measurable.

theorem measure_theory.strongly_measurable.measurable {α : Type u_1} {β : Type u_2} {f : α → β} [measurable_space α] [metric_space β] [measurable_space β] [borel_space β] (hf : measure_theory.strongly_measurable f) :

A strongly measurable function is measurable.

In a space with second countable topology, measurable implies strongly measurable.

In a space with second countable topology, strongly measurable and measurable are equivalent.

Finitely strongly measurable functions #

A sequence of simple functions such that ∀ x, tendsto (λ n, hf.approx n x) at_top (𝓝 (f x)) and ∀ n, μ (support (hf.approx n)) < ∞. These properties are given by fin_strongly_measurable.tendsto_approx and fin_strongly_measurable.fin_support_approx.

Equations
theorem measure_theory.fin_strongly_measurable.tendsto_approx {α : Type u_1} {β : Type u_2} [has_zero β] {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [topological_space β] (hf : measure_theory.fin_strongly_measurable f μ) (x : α) :
filter.tendsto (λ (n : ), (hf.approx n) x) filter.at_top (𝓝 (f x))
theorem measure_theory.fin_strongly_measurable.exists_set_sigma_finite {α : Type u_1} {β : Type u_2} [has_zero β] {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [topological_space β] [t2_space β] (hf : measure_theory.fin_strongly_measurable f μ) :
∃ (t : set α), measurable_set t (∀ (x : α), x tf x = 0) measure_theory.sigma_finite (μ.restrict t)
theorem measure_theory.fin_strongly_measurable.measurable {α : Type u_1} {β : Type u_2} [has_zero β] {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [metric_space β] [measurable_space β] [borel_space β] (hf : measure_theory.fin_strongly_measurable f μ) :

A finitely strongly measurable function is measurable.

A measurable set t such that f =ᵐ[μ.restrict tᶜ] 0 and sigma_finite (μ.restrict t).

Equations

In a space with second countable topology and a sigma-finite measure, fin_strongly_measurable and measurable are equivalent.

In a space with second countable topology and a sigma-finite measure, ae_fin_strongly_measurable and ae_measurable are equivalent.