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 #
-
strongly_measurable f:f : α → βis the limit of a sequencefs : ℕ → simple_func α β. -
fin_strongly_measurable f μ:f : α → βis the limit of a sequencefs : ℕ → simple_func α βsuch that for alln ∈ ℕ, the measure of the support offs nis finite. -
ae_fin_strongly_measurable f μ:fis almost everywhere equal to afin_strongly_measurablefunction. -
ae_fin_strongly_measurable.sigma_finite_set: a measurable settsuch thatf =ᵐ[μ.restrict tᶜ] 0andμ.restrict tis sigma-finite.
Main statements #
ae_fin_strongly_measurable.exists_set_sigma_finite: there exists a measurable settsuch thatf =ᵐ[μ.restrict tᶜ] 0andμ.restrict tis sigma-finite.mem_ℒp.ae_fin_strongly_measurable: ifmem_ℒp f p μwith0 < p < ∞, thenae_fin_strongly_measurable f μ.Lp.fin_strongly_measurable: for0 < p < ∞,Lpfunctions are finitely strongly measurable.
References #
- Hytönen, Tuomas, Jan Van Neerven, Mark Veraar, and Lutz Weis. Analysis in Banach spaces. Springer, 2016.
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
- measure_theory.strongly_measurable f = ∃ (fs : ℕ → measure_theory.simple_func α β), ∀ (x : α), filter.tendsto (λ (n : ℕ), ⇑(fs n) x) filter.at_top (𝓝 (f x))
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
- measure_theory.fin_strongly_measurable f μ = ∃ (fs : ℕ → measure_theory.simple_func α β), (∀ (n : ℕ), ⇑μ (function.support ⇑(fs n)) < ⊤) ∧ ∀ (x : α), filter.tendsto (λ (n : ℕ), ⇑(fs n) x) filter.at_top (𝓝 (f x))
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
- measure_theory.ae_fin_strongly_measurable f μ = ∃ (g : α → β), measure_theory.fin_strongly_measurable g μ ∧ f =ᵐ[μ] g
Strongly measurable functions #
theorem
measure_theory.subsingleton.strongly_measurable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[topological_space β]
[subsingleton β]
(f : α → β) :
@[protected]
noncomputable
def
measure_theory.strongly_measurable.approx
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[measurable_space α]
[topological_space β]
(hf : measure_theory.strongly_measurable f) :
ℕ → measure_theory.simple_func α β
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
- hf.approx = Exists.some hf
@[protected]
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 ∈ tᶜ → f x = 0)
(htμ : measure_theory.sigma_finite (μ.restrict t)) :
@[protected]
theorem
measure_theory.strongly_measurable.fin_strongly_measurable
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[topological_space β]
[has_zero β]
{m0 : measurable_space α}
(hf : measure_theory.strongly_measurable f)
(μ : measure_theory.measure α)
[measure_theory.sigma_finite μ] :
If the measure is sigma-finite, all strongly measurable functions are
fin_strongly_measurable.
@[protected]
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.
@[protected]
theorem
measure_theory.strongly_measurable.add
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
[measurable_space α]
[topological_space β]
[has_add β]
[has_continuous_add β]
(hf : measure_theory.strongly_measurable f)
(hg : measure_theory.strongly_measurable g) :
@[protected]
theorem
measure_theory.strongly_measurable.neg
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[measurable_space α]
[topological_space β]
[add_group β]
[topological_add_group β]
(hf : measure_theory.strongly_measurable f) :
@[protected]
theorem
measure_theory.strongly_measurable.sub
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
[measurable_space α]
[topological_space β]
[has_sub β]
[has_continuous_sub β]
(hf : measure_theory.strongly_measurable f)
(hg : measure_theory.strongly_measurable g) :
theorem
measurable.strongly_measurable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{f : α → β}
[emetric_space β]
[opens_measurable_space β]
[topological_space.second_countable_topology β]
(hf : measurable f) :
In a space with second countable topology, measurable implies strongly measurable.
theorem
measure_theory.strongly_measurable_iff_measurable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{f : α → β}
[metric_space β]
[borel_space β]
[topological_space.second_countable_topology β] :
In a space with second countable topology, strongly measurable and measurable are equivalent.
Finitely strongly measurable functions #
theorem
measure_theory.fin_strongly_measurable.ae_fin_strongly_measurable
{α : Type u_1}
{β : Type u_2}
[has_zero β]
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : α → β}
[topological_space β]
(hf : measure_theory.fin_strongly_measurable f μ) :
@[protected]
noncomputable
def
measure_theory.fin_strongly_measurable.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 μ) :
ℕ → measure_theory.simple_func α β
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
- hf.approx = Exists.some hf
@[protected]
theorem
measure_theory.fin_strongly_measurable.fin_support_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 μ)
(n : ℕ) :
@[protected]
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))
@[protected]
theorem
measure_theory.fin_strongly_measurable.strongly_measurable
{α : Type u_1}
{β : Type u_2}
[has_zero β]
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : α → β}
[topological_space β]
(hf : measure_theory.fin_strongly_measurable f μ) :
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 ∈ tᶜ → f x = 0) ∧ measure_theory.sigma_finite (μ.restrict t)
@[protected]
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.
@[protected]
theorem
measure_theory.fin_strongly_measurable.add
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{β : Type u_2}
[topological_space β]
[add_monoid β]
[has_continuous_add β]
{f g : α → β}
(hf : measure_theory.fin_strongly_measurable f μ)
(hg : measure_theory.fin_strongly_measurable g μ) :
@[protected]
theorem
measure_theory.fin_strongly_measurable.neg
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{β : Type u_2}
[topological_space β]
[add_group β]
[topological_add_group β]
{f : α → β}
(hf : measure_theory.fin_strongly_measurable f μ) :
@[protected]
theorem
measure_theory.fin_strongly_measurable.sub
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{β : Type u_2}
[topological_space β]
[add_group β]
[has_continuous_sub β]
{f g : α → β}
(hf : measure_theory.fin_strongly_measurable f μ)
(hg : measure_theory.fin_strongly_measurable g μ) :
theorem
measure_theory.fin_strongly_measurable_iff_strongly_measurable_and_exists_set_sigma_finite
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[topological_space β]
[t2_space β]
[has_zero β]
{m : measurable_space α}
{μ : measure_theory.measure α} :
measure_theory.fin_strongly_measurable f μ ↔ measure_theory.strongly_measurable f ∧ ∃ (t : set α), measurable_set t ∧ (∀ (x : α), x ∈ tᶜ → f x = 0) ∧ measure_theory.sigma_finite (μ.restrict t)
@[protected]
theorem
measure_theory.ae_fin_strongly_measurable.add
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f g : α → β}
[add_monoid β]
[has_continuous_add β]
(hf : measure_theory.ae_fin_strongly_measurable f μ)
(hg : measure_theory.ae_fin_strongly_measurable g μ) :
@[protected]
theorem
measure_theory.ae_fin_strongly_measurable.neg
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
[add_group β]
[topological_add_group β]
(hf : measure_theory.ae_fin_strongly_measurable f μ) :
@[protected]
theorem
measure_theory.ae_fin_strongly_measurable.sub
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f g : α → β}
[add_group β]
[has_continuous_sub β]
(hf : measure_theory.ae_fin_strongly_measurable f μ)
(hg : measure_theory.ae_fin_strongly_measurable g μ) :
theorem
measure_theory.ae_fin_strongly_measurable.exists_set_sigma_finite
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
[has_zero β]
[t2_space β]
(hf : measure_theory.ae_fin_strongly_measurable f μ) :
∃ (t : set α), measurable_set t ∧ f =ᵐ[μ.restrict tᶜ] 0 ∧ measure_theory.sigma_finite (μ.restrict t)
def
measure_theory.ae_fin_strongly_measurable.sigma_finite_set
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
[has_zero β]
[t2_space β]
(hf : measure_theory.ae_fin_strongly_measurable f μ) :
set α
A measurable set t such that f =ᵐ[μ.restrict tᶜ] 0 and sigma_finite (μ.restrict t).
Equations
- hf.sigma_finite_set = _.some
@[protected]
theorem
measure_theory.ae_fin_strongly_measurable.measurable_set
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
[has_zero β]
[t2_space β]
(hf : measure_theory.ae_fin_strongly_measurable f μ) :
theorem
measure_theory.ae_fin_strongly_measurable.ae_eq_zero_compl
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
[has_zero β]
[t2_space β]
(hf : measure_theory.ae_fin_strongly_measurable f μ) :
f =ᵐ[μ.restrict hf.sigma_finite_setᶜ] 0
@[protected, instance]
def
measure_theory.ae_fin_strongly_measurable.sigma_finite_restrict
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
[has_zero β]
[t2_space β]
(hf : measure_theory.ae_fin_strongly_measurable f μ) :
theorem
measure_theory.fin_strongly_measurable_iff_measurable
{α : Type u_1}
{G : Type u_2}
[normed_group G]
[measurable_space G]
[borel_space G]
[topological_space.second_countable_topology G]
{f : α → G}
{m0 : measurable_space α}
(μ : measure_theory.measure α)
[measure_theory.sigma_finite μ] :
In a space with second countable topology and a sigma-finite measure, fin_strongly_measurable
and measurable are equivalent.
theorem
measure_theory.ae_fin_strongly_measurable_iff_ae_measurable
{α : Type u_1}
{G : Type u_2}
[normed_group G]
[measurable_space G]
[borel_space G]
[topological_space.second_countable_topology G]
{f : α → G}
{m0 : measurable_space α}
(μ : measure_theory.measure α)
[measure_theory.sigma_finite μ] :
In a space with second countable topology and a sigma-finite measure,
ae_fin_strongly_measurable and ae_measurable are equivalent.
theorem
measure_theory.mem_ℒp.fin_strongly_measurable_of_measurable
{α : Type u_1}
{G : Type u_2}
{p : ℝ≥0∞}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_group G]
[measurable_space G]
[borel_space G]
[topological_space.second_countable_topology G]
{f : α → G}
(hf : measure_theory.mem_ℒp f p μ)
(hf_meas : measurable f)
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤) :
theorem
measure_theory.mem_ℒp.ae_fin_strongly_measurable
{α : Type u_1}
{G : Type u_2}
{p : ℝ≥0∞}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_group G]
[measurable_space G]
[borel_space G]
[topological_space.second_countable_topology G]
{f : α → G}
(hf : measure_theory.mem_ℒp f p μ)
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤) :
theorem
measure_theory.integrable.ae_fin_strongly_measurable
{α : Type u_1}
{G : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_group G]
[measurable_space G]
[borel_space G]
[topological_space.second_countable_topology G]
{f : α → G}
(hf : measure_theory.integrable f μ) :
theorem
measure_theory.Lp.fin_strongly_measurable
{α : Type u_1}
{G : Type u_2}
{p : ℝ≥0∞}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_group G]
[measurable_space G]
[borel_space G]
[topological_space.second_countable_topology G]
(f : ↥(measure_theory.Lp G p μ))
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤) :