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. We also provide almost everywhere versions of these notions.

Almost everywhere strongly measurable functions form the largest class of functions that can be integrated using the Bochner integral.

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

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 #

We provide a solid API for strongly measurable functions, and for almost everywhere strongly measurable functions, as a basis for the Bochner integral.

References #

@[class]
structure second_countable_topology_either (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] :
Prop

The typeclass second_countable_topology_either α β registers the fact that at least one of the two spaces has second countable topology. This is the right assumption to ensure that continuous maps from α to β are strongly measurable.

Instances of this typeclass
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_strongly_measurable {α : Type u_1} {β : Type u_2} [topological_space β] {m0 : measurable_space α} (f : α → β) (μ : measure_theory.measure α) :
Prop

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

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 #

@[simp]
theorem measure_theory.strongly_measurable_of_is_empty {α : Type u_1} {β : Type u_2} [is_empty α] {m : measurable_space α} [topological_space β] (f : α → β) :
theorem measure_theory.strongly_measurable_const {α : Type u_1} {β : Type u_2} {m : measurable_space α} [topological_space β] {b : β} :
theorem measure_theory.strongly_measurable_const' {α : Type u_1} {β : Type u_2} {m : measurable_space α} [topological_space β] {f : α → β} (hf : ∀ (x y : α), f x = f y) :

A version of strongly_measurable_const that assumes f x = f y for all x, y. This version works for functions between empty types.

@[simp]
@[protected]
noncomputable def measure_theory.strongly_measurable.approx {α : Type u_1} {β : Type u_2} {f : α → β} [topological_space β] {m : measurable_space α} (hf : measure_theory.strongly_measurable f) :

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
@[protected]
theorem measure_theory.strongly_measurable.tendsto_approx {α : Type u_1} {β : Type u_2} {f : α → β} [topological_space β] {m : measurable_space α} (hf : measure_theory.strongly_measurable f) (x : α) :
filter.tendsto (λ (n : ), (hf.approx n) x) filter.at_top (nhds (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)) :
@[protected]

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

@[protected]

A strongly measurable function is measurable.

@[protected]

A strongly measurable function is almost everywhere measurable.

theorem continuous.comp_strongly_measurable {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} [topological_space β] [topological_space γ] {g : β → γ} {f : α → β} (hg : continuous g) (hf : measure_theory.strongly_measurable f) :
measure_theory.strongly_measurable (λ (x : α), g (f x))
@[protected]
theorem measure_theory.strongly_measurable.mono {α : Type u_1} {β : Type u_2} {f : α → β} {m m' : measurable_space α} [topological_space β] (hf : measure_theory.strongly_measurable f) (h_mono : m' m) :
@[protected]
theorem measure_theory.strongly_measurable.prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} [topological_space β] [topological_space γ] {f : α → β} {g : α → γ} (hf : measure_theory.strongly_measurable f) (hg : measure_theory.strongly_measurable g) :
measure_theory.strongly_measurable (λ (x : α), (f x, g x))
theorem measure_theory.strongly_measurable.comp_measurable {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space β] {m : measurable_space α} {m' : measurable_space γ} {f : α → β} {g : γ → α} (hf : measure_theory.strongly_measurable f) (hg : measurable g) :
theorem measure_theory.strongly_measurable.of_uncurry_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space β] {mα : measurable_space α} {mγ : measurable_space γ} {f : α → γ → β} (hf : measure_theory.strongly_measurable (function.uncurry f)) {x : α} :
theorem measure_theory.strongly_measurable.of_uncurry_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space β] {mα : measurable_space α} {mγ : measurable_space γ} {f : α → γ → β} (hf : measure_theory.strongly_measurable (function.uncurry f)) {y : γ} :
theorem measure_theory.strongly_measurable.mul_const {α : Type u_1} {β : Type u_2} {f : α → β} {mα : measurable_space α} [topological_space β] [has_mul β] [has_continuous_mul β] (hf : measure_theory.strongly_measurable f) (c : β) :
theorem measure_theory.strongly_measurable.add_const {α : Type u_1} {β : Type u_2} {f : α → β} {mα : measurable_space α} [topological_space β] [has_add β] [has_continuous_add β] (hf : measure_theory.strongly_measurable f) (c : β) :
theorem measure_theory.strongly_measurable.const_mul {α : Type u_1} {β : Type u_2} {f : α → β} {mα : measurable_space α} [topological_space β] [has_mul β] [has_continuous_mul β] (hf : measure_theory.strongly_measurable f) (c : β) :
theorem measure_theory.strongly_measurable.const_add {α : Type u_1} {β : Type u_2} {f : α → β} {mα : measurable_space α} [topological_space β] [has_add β] [has_continuous_add β] (hf : measure_theory.strongly_measurable f) (c : β) :
@[protected]
@[protected]
@[protected]
theorem measure_theory.strongly_measurable.vadd {α : Type u_1} {β : Type u_2} {mα : measurable_space α} [topological_space β] {𝕜 : Type u_3} [topological_space 𝕜] [has_vadd 𝕜 β] [has_continuous_vadd 𝕜 β] {f : α → 𝕜} {g : α → β} (hf : measure_theory.strongly_measurable f) (hg : measure_theory.strongly_measurable g) :
@[protected]
theorem measure_theory.strongly_measurable.smul {α : Type u_1} {β : Type u_2} {mα : measurable_space α} [topological_space β] {𝕜 : Type u_3} [topological_space 𝕜] [has_scalar 𝕜 β] [has_continuous_smul 𝕜 β] {f : α → 𝕜} {g : α → β} (hf : measure_theory.strongly_measurable f) (hg : measure_theory.strongly_measurable g) :
@[protected]
theorem measure_theory.strongly_measurable.const_smul {α : Type u_1} {β : Type u_2} {f : α → β} {mα : measurable_space α} [topological_space β] {𝕜 : Type u_3} [has_scalar 𝕜 β] [has_continuous_const_smul 𝕜 β] (hf : measure_theory.strongly_measurable f) (c : 𝕜) :
@[protected]
theorem measure_theory.strongly_measurable.const_smul' {α : Type u_1} {β : Type u_2} {f : α → β} {mα : measurable_space α} [topological_space β] {𝕜 : Type u_3} [has_scalar 𝕜 β] [has_continuous_const_smul 𝕜 β] (hf : measure_theory.strongly_measurable f) (c : 𝕜) :
@[protected]
theorem measure_theory.strongly_measurable.smul_const {α : Type u_1} {β : Type u_2} {mα : measurable_space α} [topological_space β] {𝕜 : Type u_3} [topological_space 𝕜] [has_scalar 𝕜 β] [has_continuous_smul 𝕜 β] {f : α → 𝕜} (hf : measure_theory.strongly_measurable f) (c : β) :
@[protected]
theorem measure_theory.strongly_measurable.vadd_const {α : Type u_1} {β : Type u_2} {mα : measurable_space α} [topological_space β] {𝕜 : Type u_3} [topological_space 𝕜] [has_vadd 𝕜 β] [has_continuous_vadd 𝕜 β] {f : α → 𝕜} (hf : measure_theory.strongly_measurable f) (c : β) :
theorem strongly_measurable_const_smul_iff {α : Type u_1} {β : Type u_2} {f : α → β} [topological_space β] {G : Type u_5} [group G] [mul_action G β] [has_continuous_const_smul G β] {m : measurable_space α} (c : G) :
theorem strongly_measurable_const_smul_iff₀ {α : Type u_1} {β : Type u_2} {f : α → β} [topological_space β] {G₀ : Type u_6} [group_with_zero G₀] [mul_action G₀ β] [has_continuous_const_smul G₀ β] {m : measurable_space α} {c : G₀} (hc : c 0) :

Big operators: and #

theorem list.strongly_measurable_sum' {α : Type u_1} {M : Type u_5} [add_monoid M] [topological_space M] [has_continuous_add M] {m : measurable_space α} (l : list (α → M)) (hl : ∀ (f : α → M), f lmeasure_theory.strongly_measurable f) :
theorem list.strongly_measurable_prod' {α : Type u_1} {M : Type u_5} [monoid M] [topological_space M] [has_continuous_mul M] {m : measurable_space α} (l : list (α → M)) (hl : ∀ (f : α → M), f lmeasure_theory.strongly_measurable f) :
theorem list.strongly_measurable_sum {α : Type u_1} {M : Type u_5} [add_monoid M] [topological_space M] [has_continuous_add M] {m : measurable_space α} (l : list (α → M)) (hl : ∀ (f : α → M), f lmeasure_theory.strongly_measurable f) :
measure_theory.strongly_measurable (λ (x : α), (list.map (λ (f : α → M), f x) l).sum)
theorem list.strongly_measurable_prod {α : Type u_1} {M : Type u_5} [monoid M] [topological_space M] [has_continuous_mul M] {m : measurable_space α} (l : list (α → M)) (hl : ∀ (f : α → M), f lmeasure_theory.strongly_measurable f) :
measure_theory.strongly_measurable (λ (x : α), (list.map (λ (f : α → M), f x) l).prod)
theorem multiset.strongly_measurable_sum' {α : Type u_1} {M : Type u_5} [add_comm_monoid M] [topological_space M] [has_continuous_add M] {m : measurable_space α} (l : multiset (α → M)) (hl : ∀ (f : α → M), f lmeasure_theory.strongly_measurable f) :
theorem multiset.strongly_measurable_prod' {α : Type u_1} {M : Type u_5} [comm_monoid M] [topological_space M] [has_continuous_mul M] {m : measurable_space α} (l : multiset (α → M)) (hl : ∀ (f : α → M), f lmeasure_theory.strongly_measurable f) :
theorem multiset.strongly_measurable_sum {α : Type u_1} {M : Type u_5} [add_comm_monoid M] [topological_space M] [has_continuous_add M] {m : measurable_space α} (s : multiset (α → M)) (hs : ∀ (f : α → M), f smeasure_theory.strongly_measurable f) :
measure_theory.strongly_measurable (λ (x : α), (multiset.map (λ (f : α → M), f x) s).sum)
theorem multiset.strongly_measurable_prod {α : Type u_1} {M : Type u_5} [comm_monoid M] [topological_space M] [has_continuous_mul M] {m : measurable_space α} (s : multiset (α → M)) (hs : ∀ (f : α → M), f smeasure_theory.strongly_measurable f) :
measure_theory.strongly_measurable (λ (x : α), (multiset.map (λ (f : α → M), f x) s).prod)
theorem finset.strongly_measurable_sum' {α : Type u_1} {M : Type u_5} [add_comm_monoid M] [topological_space M] [has_continuous_add M] {m : measurable_space α} {ι : Type u_2} {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i smeasure_theory.strongly_measurable (f i)) :
theorem finset.strongly_measurable_prod' {α : Type u_1} {M : Type u_5} [comm_monoid M] [topological_space M] [has_continuous_mul M] {m : measurable_space α} {ι : Type u_2} {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i smeasure_theory.strongly_measurable (f i)) :
theorem finset.strongly_measurable_prod {α : Type u_1} {M : Type u_5} [comm_monoid M] [topological_space M] [has_continuous_mul M] {m : measurable_space α} {ι : Type u_2} {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i smeasure_theory.strongly_measurable (f i)) :
measure_theory.strongly_measurable (λ (a : α), s.prod (λ (i : ι), f i a))
theorem finset.strongly_measurable_sum {α : Type u_1} {M : Type u_5} [add_comm_monoid M] [topological_space M] [has_continuous_add M] {m : measurable_space α} {ι : Type u_2} {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i smeasure_theory.strongly_measurable (f i)) :
measure_theory.strongly_measurable (λ (a : α), s.sum (λ (i : ι), f i a))

The range of a strongly measurable function is separable.

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

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

A function is strongly measurable if and only if it is measurable and has separable range.

A continuous function is strongly measurable when either the source space or the target space is second-countable.

If g is a topological embedding, then f is strongly measurable iff g ∘ f is.

theorem strongly_measurable_of_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space α} [topological_space β] [topological_space.pseudo_metrizable_space β] (u : filter ι) [u.ne_bot] [u.is_countably_generated] {f : ι → α → β} {g : α → β} (hf : ∀ (i : ι), measure_theory.strongly_measurable (f i)) (lim : filter.tendsto f u (nhds g)) :

A sequential limit of strongly measurable functions is strongly measurable.

@[protected]
theorem measure_theory.strongly_measurable.piecewise {α : Type u_1} {β : Type u_2} {f g : α → β} {m : measurable_space α} [topological_space β] {s : set α} {_x : decidable_pred (λ (_x : α), _x s)} (hs : measurable_set s) (hf : measure_theory.strongly_measurable f) (hg : measure_theory.strongly_measurable g) :
@[protected]
theorem measure_theory.strongly_measurable.ite {α : Type u_1} {β : Type u_2} {f g : α → β} {m : measurable_space α} [topological_space β] {p : α → Prop} {_x : decidable_pred p} (hp : measurable_set {a : α | p a}) (hf : measure_theory.strongly_measurable f) (hg : measure_theory.strongly_measurable g) :
measure_theory.strongly_measurable (λ (x : α), ite (p x) (f x) (g x))

this is slightly different from strongly_measurable.piecewise. It can be used to show strongly_measurable (ite (x=0) 0 1) by exact strongly_measurable.ite (measurable_set_singleton 0) strongly_measurable_const strongly_measurable_const, but replacing strongly_measurable.ite by strongly_measurable.piecewise in that example proof does not work.

theorem strongly_measurable_of_strongly_measurable_union_cover {α : Type u_1} {β : Type u_2} {m : measurable_space α} [topological_space β] {f : α → β} (s t : set α) (hs : measurable_set s) (ht : measurable_set t) (h : set.univ s t) (hc : measure_theory.strongly_measurable (λ (a : s), f a)) (hd : measure_theory.strongly_measurable (λ (a : t), f a)) :
@[protected]
theorem measure_theory.strongly_measurable.indicator {α : Type u_1} {β : Type u_2} {f : α → β} {m : measurable_space α} [topological_space β] [has_zero β] (hf : measure_theory.strongly_measurable f) {s : set α} (hs : measurable_set s) :
@[protected]
theorem measure_theory.strongly_measurable.dist {α : Type u_1} {m : measurable_space α} {β : Type u_2} [pseudo_metric_space β] {f g : α → β} (hf : measure_theory.strongly_measurable f) (hg : measure_theory.strongly_measurable g) :
@[protected]
theorem measure_theory.strongly_measurable.norm {α : Type u_1} {m : measurable_space α} {β : Type u_2} [normed_group β] {f : α → β} (hf : measure_theory.strongly_measurable f) :
@[protected]
theorem measure_theory.strongly_measurable.nnnorm {α : Type u_1} {m : measurable_space α} {β : Type u_2} [normed_group β] {f : α → β} (hf : measure_theory.strongly_measurable f) :
@[protected]
theorem measure_theory.strongly_measurable.ennnorm {α : Type u_1} {m : measurable_space α} {β : Type u_2} [normed_group β] {f : α → β} (hf : measure_theory.strongly_measurable f) :
measurable (λ (a : α), f a∥₊)
theorem measurable_embedding.strongly_measurable_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} {g' : γ → β} {mα : measurable_space α} {mγ : measurable_space γ} [topological_space β] (hg : measurable_embedding g) (hf : measure_theory.strongly_measurable f) (hg' : measure_theory.strongly_measurable g') :
theorem measurable_embedding.exists_strongly_measurable_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} {mα : measurable_space α} {mγ : measurable_space γ} [topological_space β] (hg : measurable_embedding g) (hf : measure_theory.strongly_measurable f) (hne : γ → nonempty β) :
∃ (f' : γ → β), measure_theory.strongly_measurable f' f' g = f
@[protected]
theorem measure_theory.strongly_measurable.inner {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {m : measurable_space α} {f g : α → E} (hf : measure_theory.strongly_measurable f) (hg : measure_theory.strongly_measurable g) :
theorem measure_theory.strongly_measurable.strongly_measurable_in_set {α : Type u_1} {β : Type u_2} {m : measurable_space α} [topological_space β] [has_zero β] {s : set α} {f : α → β} (hs : measurable_set s) (hf : measure_theory.strongly_measurable f) (hf_zero : ∀ (x : α), x sf x = 0) :
∃ (fs : measure_theory.simple_func α β), (∀ (x : α), filter.tendsto (λ (n : ), (fs n) x) filter.at_top (nhds (f x))) ∀ (x : α), x s∀ (n : ), (fs n) x = 0
theorem measure_theory.strongly_measurable.strongly_measurable_of_measurable_space_le_on {α : Type u_1} {E : Type u_2} {m m₂ : measurable_space α} [topological_space E] [has_zero E] {s : set α} {f : α → E} (hs_m : measurable_set s) (hs : ∀ (t : set α), measurable_set (s t)measurable_set (s t)) (hf : measure_theory.strongly_measurable f) (hf_zero : ∀ (x : α), x sf x = 0) :

If the restriction to a set s of a σ-algebra m is included in the restriction to s of another σ-algebra m₂ (hypothesis hs), the set s is m measurable and a function f supported on s is m-strongly-measurable, then f is also m₂-strongly-measurable.

Finitely strongly measurable functions #

@[protected]
noncomputable def measure_theory.fin_strongly_measurable.approx {α : Type u_1} {β : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [has_zero β] [topological_space β] (hf : measure_theory.fin_strongly_measurable f μ) :

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
@[protected]
theorem measure_theory.fin_strongly_measurable.fin_support_approx {α : Type u_1} {β : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [has_zero β] [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} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [has_zero β] [topological_space β] (hf : measure_theory.fin_strongly_measurable f μ) (x : α) :
filter.tendsto (λ (n : ), (hf.approx n) x) filter.at_top (nhds (f x))
theorem measure_theory.fin_strongly_measurable.exists_set_sigma_finite {α : Type u_1} {β : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [has_zero β] [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)
@[protected]

A finitely strongly measurable function is measurable.

@[protected]
theorem measure_theory.fin_strongly_measurable.const_smul {α : Type u_1} {β : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [topological_space β] {𝕜 : Type u_3} [topological_space 𝕜] [add_monoid β] [monoid 𝕜] [distrib_mul_action 𝕜 β] [has_continuous_smul 𝕜 β] (hf : measure_theory.fin_strongly_measurable f μ) (c : 𝕜) :

Almost everywhere strongly measurable functions #

theorem measure_theory.ae_strongly_measurable_const {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {b : β} :
@[simp]
@[simp]
@[simp]
theorem measure_theory.ae_measurable_zero_measure {α : Type u_1} {β : Type u_2} [measurable_space α] [topological_space β] (f : α → β) :
@[protected]
noncomputable def measure_theory.ae_strongly_measurable.mk {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] (f : α → β) (hf : measure_theory.ae_strongly_measurable f μ) :
α → β

A strongly_measurable function such that f =ᵐ[μ] hf.mk f. See lemmas strongly_measurable_mk and ae_eq_mk.

Equations
theorem measure_theory.ae_strongly_measurable.congr {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {f g : α → β} (hf : measure_theory.ae_strongly_measurable f μ) (h : f =ᵐ[μ] g) :
theorem ae_strongly_measurable_congr {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {f g : α → β} (h : f =ᵐ[μ] g) :
theorem measure_theory.ae_strongly_measurable.mono_set {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {f : α → β} {s t : set α} (h : s t) (ht : measure_theory.ae_strongly_measurable f (μ.restrict t)) :
@[protected]
theorem measure_theory.ae_strongly_measurable.ae_mem_imp_eq_mk {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {f : α → β} {s : set α} (h : measure_theory.ae_strongly_measurable f (μ.restrict s)) :
∀ᵐ (x : α) ∂μ, x sf x = measure_theory.ae_strongly_measurable.mk f h x
theorem continuous.comp_ae_strongly_measurable {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] [topological_space γ] {g : β → γ} {f : α → β} (hg : continuous g) (hf : measure_theory.ae_strongly_measurable f μ) :
measure_theory.ae_strongly_measurable (λ (x : α), g (f x)) μ

The composition of a continuous function and an ae strongly measurable function is ae strongly measurable.

A continuous function from α to β is ae strongly measurable when one of the two spaces is second countable.

@[protected]
theorem measure_theory.ae_strongly_measurable.prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] [topological_space γ] {f : α → β} {g : α → γ} (hf : measure_theory.ae_strongly_measurable f μ) (hg : measure_theory.ae_strongly_measurable g μ) :
measure_theory.ae_strongly_measurable (λ (x : α), (f x, g x)) μ

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

@[protected]
theorem measure_theory.ae_strongly_measurable.add_const {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {f : α → β} [has_add β] [has_continuous_add β] (hf : measure_theory.ae_strongly_measurable f μ) (c : β) :
@[protected]
theorem measure_theory.ae_strongly_measurable.mul_const {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {f : α → β} [has_mul β] [has_continuous_mul β] (hf : measure_theory.ae_strongly_measurable f μ) (c : β) :
@[protected]
theorem measure_theory.ae_strongly_measurable.const_mul {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {f : α → β} [has_mul β] [has_continuous_mul β] (hf : measure_theory.ae_strongly_measurable f μ) (c : β) :
@[protected]
theorem measure_theory.ae_strongly_measurable.const_add {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {f : α → β} [has_add β] [has_continuous_add β] (hf : measure_theory.ae_strongly_measurable f μ) (c : β) :
@[protected]
theorem measure_theory.ae_strongly_measurable.smul {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {𝕜 : Type u_3} [topological_space 𝕜] [has_scalar 𝕜 β] [has_continuous_smul 𝕜 β] {f : α → 𝕜} {g : α → β} (hf : measure_theory.ae_strongly_measurable f μ) (hg : measure_theory.ae_strongly_measurable g μ) :
measure_theory.ae_strongly_measurable (λ (x : α), f x g x) μ
@[protected]
theorem measure_theory.ae_strongly_measurable.vadd {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {𝕜 : Type u_3} [topological_space 𝕜] [has_vadd 𝕜 β] [has_continuous_vadd 𝕜 β] {f : α → 𝕜} {g : α → β} (hf : measure_theory.ae_strongly_measurable f μ) (hg : measure_theory.ae_strongly_measurable g μ) :
@[protected]
theorem measure_theory.ae_strongly_measurable.const_smul {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {f : α → β} {𝕜 : Type u_3} [has_scalar 𝕜 β] [has_continuous_const_smul 𝕜 β] (hf : measure_theory.ae_strongly_measurable f μ) (c : 𝕜) :
@[protected]
theorem measure_theory.ae_strongly_measurable.const_smul' {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {f : α → β} {𝕜 : Type u_3} [has_scalar 𝕜 β] [has_continuous_const_smul 𝕜 β] (hf : measure_theory.ae_strongly_measurable f μ) (c : 𝕜) :
@[protected]
theorem measure_theory.ae_strongly_measurable.vadd_const {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {𝕜 : Type u_3} [topological_space 𝕜] [has_vadd 𝕜 β] [has_continuous_vadd 𝕜 β] {f : α → 𝕜} (hf : measure_theory.ae_strongly_measurable f μ) (c : β) :
@[protected]
theorem measure_theory.ae_strongly_measurable.smul_const {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {𝕜 : Type u_3} [topological_space 𝕜] [has_scalar 𝕜 β] [has_continuous_smul 𝕜 β] {f : α → 𝕜} (hf : measure_theory.ae_strongly_measurable f μ) (c : β) :

Big operators: and #

theorem list.ae_strongly_measurable_prod' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {M : Type u_5} [monoid M] [topological_space M] [has_continuous_mul M] (l : list (α → M)) (hl : ∀ (f : α → M), f lmeasure_theory.ae_strongly_measurable f μ) :
theorem list.ae_strongly_measurable_sum' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {M : Type u_5} [add_monoid M] [topological_space M] [has_continuous_add M] (l : list (α → M)) (hl : ∀ (f : α → M), f lmeasure_theory.ae_strongly_measurable f μ) :
theorem list.ae_strongly_measurable_prod {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {M : Type u_5} [monoid M] [topological_space M] [has_continuous_mul M] (l : list (α → M)) (hl : ∀ (f : α → M), f lmeasure_theory.ae_strongly_measurable f μ) :
measure_theory.ae_strongly_measurable (λ (x : α), (list.map (λ (f : α → M), f x) l).prod) μ
theorem list.ae_strongly_measurable_sum {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {M : Type u_5} [add_monoid M] [topological_space M] [has_continuous_add M] (l : list (α → M)) (hl : ∀ (f : α → M), f lmeasure_theory.ae_strongly_measurable f μ) :
measure_theory.ae_strongly_measurable (λ (x : α), (list.map (λ (f : α → M), f x) l).sum) μ
theorem multiset.ae_strongly_measurable_prod' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {M : Type u_5} [comm_monoid M] [topological_space M] [has_continuous_mul M] (l : multiset (α → M)) (hl : ∀ (f : α → M), f lmeasure_theory.ae_strongly_measurable f μ) :
theorem multiset.ae_strongly_measurable_sum' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {M : Type u_5} [add_comm_monoid M] [topological_space M] [has_continuous_add M] (l : multiset (α → M)) (hl : ∀ (f : α → M), f lmeasure_theory.ae_strongly_measurable f μ) :
theorem multiset.ae_strongly_measurable_prod {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {M : Type u_5} [comm_monoid M] [topological_space M] [has_continuous_mul M] (s : multiset (α → M)) (hs : ∀ (f : α → M), f smeasure_theory.ae_strongly_measurable f μ) :
measure_theory.ae_strongly_measurable (λ (x : α), (multiset.map (λ (f : α → M), f x) s).prod) μ
theorem multiset.ae_strongly_measurable_sum {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {M : Type u_5} [add_comm_monoid M] [topological_space M] [has_continuous_add M] (s : multiset (α → M)) (hs : ∀ (f : α → M), f smeasure_theory.ae_strongly_measurable f μ) :
measure_theory.ae_strongly_measurable (λ (x : α), (multiset.map (λ (f : α → M), f x) s).sum) μ
theorem finset.ae_strongly_measurable_prod' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {M : Type u_5} [comm_monoid M] [topological_space M] [has_continuous_mul M] {ι : Type u_2} {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i smeasure_theory.ae_strongly_measurable (f i) μ) :
theorem finset.ae_strongly_measurable_sum' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {M : Type u_5} [add_comm_monoid M] [topological_space M] [has_continuous_add M] {ι : Type u_2} {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i smeasure_theory.ae_strongly_measurable (f i) μ) :
measure_theory.ae_strongly_measurable (s.sum (λ (i : ι), f i)) μ
theorem finset.ae_strongly_measurable_sum {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {M : Type u_5} [add_comm_monoid M] [topological_space M] [has_continuous_add M] {ι : Type u_2} {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i smeasure_theory.ae_strongly_measurable (f i) μ) :
measure_theory.ae_strongly_measurable (λ (a : α), s.sum (λ (i : ι), f i a)) μ
theorem finset.ae_strongly_measurable_prod {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {M : Type u_5} [comm_monoid M] [topological_space M] [has_continuous_mul M] {ι : Type u_2} {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i smeasure_theory.ae_strongly_measurable (f i) μ) :
measure_theory.ae_strongly_measurable (λ (a : α), s.prod (λ (i : ι), f i a)) μ

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

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

@[protected]
@[protected]
theorem measure_theory.ae_strongly_measurable.norm {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} [normed_group β] {f : α → β} (hf : measure_theory.ae_strongly_measurable f μ) :
@[protected]
theorem measure_theory.ae_strongly_measurable.nnnorm {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} [normed_group β] {f : α → β} (hf : measure_theory.ae_strongly_measurable f μ) :
@[protected]
theorem measure_theory.ae_strongly_measurable.ennnorm {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} [normed_group β] {f : α → β} (hf : measure_theory.ae_strongly_measurable f μ) :
ae_measurable (λ (a : α), f a∥₊) μ
@[protected]
theorem measure_theory.ae_strongly_measurable.edist {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} [normed_group β] {f g : α → β} (hf : measure_theory.ae_strongly_measurable f μ) (hg : measure_theory.ae_strongly_measurable g μ) :
ae_measurable (λ (a : α), has_edist.edist (f a) (g a)) μ
@[protected]
theorem measure_theory.ae_strongly_measurable.re {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [is_R_or_C 𝕜] {f : α → 𝕜} (hf : measure_theory.ae_strongly_measurable f μ) :
@[protected]
theorem measure_theory.ae_strongly_measurable.im {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [is_R_or_C 𝕜] {f : α → 𝕜} (hf : measure_theory.ae_strongly_measurable f μ) :
@[protected]
theorem measure_theory.ae_strongly_measurable.inner {α : Type u_1} {𝕜 : Type u_5} {E : Type u_6} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {m : measurable_space α} {μ : measure_theory.measure α} {f g : α → E} (hf : measure_theory.ae_strongly_measurable f μ) (hg : measure_theory.ae_strongly_measurable g μ) :
@[protected]
theorem ae_strongly_measurable_of_ae_strongly_measurable_trim {β : Type u_2} [topological_space β] {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) {f : α → β} (hf : measure_theory.ae_strongly_measurable f (μ.trim hm)) :
theorem measure_theory.ae_strongly_measurable.comp_ae_measurable {α : Type u_1} {β : Type u_2} [topological_space β] {g : α → β} {γ : Type u_3} {mγ : measurable_space γ} {mα : measurable_space α} {f : γ → α} {μ : measure_theory.measure γ} (hg : measure_theory.ae_strongly_measurable g (measure_theory.measure.map f μ)) (hf : ae_measurable f μ) :
theorem measure_theory.ae_strongly_measurable.comp_measurable {α : Type u_1} {β : Type u_2} [topological_space β] {g : α → β} {γ : Type u_3} {mγ : measurable_space γ} {mα : measurable_space α} {f : γ → α} {μ : measure_theory.measure γ} (hg : measure_theory.ae_strongly_measurable g (measure_theory.measure.map f μ)) (hf : measurable f) :
theorem measure_theory.ae_strongly_measurable.comp_measurable' {α : Type u_1} {β : Type u_2} [topological_space β] {g : α → β} {γ : Type u_3} {mγ : measurable_space γ} {mα : measurable_space α} {f : γ → α} {μ : measure_theory.measure γ} {ν : measure_theory.measure α} (hg : measure_theory.ae_strongly_measurable g ν) (hf : measurable f) (h : (measure_theory.measure.map f μ).absolutely_continuous ν) :
theorem measure_theory.ae_strongly_measurable.is_separable_ae_range {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {f : α → β} (hf : measure_theory.ae_strongly_measurable f μ) :
∃ (t : set β), topological_space.is_separable t ∀ᵐ (x : α) ∂μ, f x t

A function is almost everywhere strongly measurable if and only if it is almost everywhere measurable, and up to a zero measure set its range is contained in a separable set.

theorem measure_theory.measure_preserving.ae_strongly_measurable_comp_iff {α : Type u_1} {γ : Type u_3} [topological_space γ] {β : Type u_2} {f : α → β} {mα : measurable_space α} {μa : measure_theory.measure α} {mβ : measurable_space β} {μb : measure_theory.measure β} (hf : measure_theory.measure_preserving f μa μb) (h₂ : measurable_embedding f) {g : β → γ} :
theorem ae_strongly_measurable_of_tendsto_ae {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {ι : Type u_3} [topological_space.pseudo_metrizable_space β] (u : filter ι) [u.ne_bot] [u.is_countably_generated] {f : ι → α → β} {g : α → β} (hf : ∀ (i : ι), measure_theory.ae_strongly_measurable (f i) μ) (lim : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ι), f n x) u (nhds (g x))) :

An almost everywhere sequential limit of almost everywhere strongly measurable functions is almost everywhere strongly measurable.

theorem exists_strongly_measurable_limit_of_tendsto_ae {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] [topological_space.pseudo_metrizable_space β] {f : α → β} (hf : ∀ (n : ), measure_theory.ae_strongly_measurable (f n) μ) (h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), filter.tendsto (λ (n : ), f n x) filter.at_top (nhds l)) :
∃ (f_lim : α → β) (hf_lim_meas : measure_theory.strongly_measurable f_lim), ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ), f n x) filter.at_top (nhds (f_lim x))

If a sequence of almost everywhere strongly measurable functions converges almost everywhere, one can select a strongly measurable function as the almost everywhere limit.

@[protected]
theorem measure_theory.ae_strongly_measurable.Union {α : Type u_1} {β : Type u_2} {ι : Type u_4} [encodable ι] {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {f : α → β} [topological_space.pseudo_metrizable_space β] {s : ι → set α} (h : ∀ (i : ι), measure_theory.ae_strongly_measurable f (μ.restrict (s i))) :
@[simp]
theorem ae_strongly_measurable_Union_iff {α : Type u_1} {β : Type u_2} {ι : Type u_4} [encodable ι] {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {f : α → β} [topological_space.pseudo_metrizable_space β] {s : ι → set α} :
theorem ae_strongly_measurable_smul_const_iff {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [nondiscrete_normed_field 𝕜] [complete_space 𝕜] {E : Type u_6} [normed_group E] [normed_space 𝕜 E] {f : α → 𝕜} {c : E} (hc : c 0) :
theorem ae_strongly_measurable_const_smul_iff {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {f : α → β} {G : Type u_5} [group G] [mul_action G β] [has_continuous_const_smul G β] (c : G) :
theorem ae_strongly_measurable_const_smul_iff₀ {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {f : α → β} {G₀ : Type u_6} [group_with_zero G₀] [mul_action G₀ β] [has_continuous_const_smul G₀ β] {c : G₀} (hc : c 0) :
theorem strongly_measurable.apply_continuous_linear_map {α : Type u_1} {𝕜 : Type u_5} [nondiscrete_normed_field 𝕜] {E : Type u_6} [normed_group E] [normed_space 𝕜 E] {F : Type u_7} [normed_group F] [normed_space 𝕜 F] {m : measurable_space α} {φ : α → (F →L[𝕜] E)} (hφ : measure_theory.strongly_measurable φ) (v : F) :
theorem measure_theory.ae_strongly_measurable.apply_continuous_linear_map {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [nondiscrete_normed_field 𝕜] {E : Type u_6} [normed_group E] [normed_space 𝕜 E] {F : Type u_7} [normed_group F] [normed_space 𝕜 F] {φ : α → (F →L[𝕜] E)} (hφ : measure_theory.ae_strongly_measurable φ μ) (v : F) :
measure_theory.ae_strongly_measurable (λ (a : α), (φ a) v) μ
theorem continuous_linear_map.ae_strongly_measurable_comp₂ {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [nondiscrete_normed_field 𝕜] {E : Type u_6} [normed_group E] [normed_space 𝕜 E] {F : Type u_7} [normed_group F] [normed_space 𝕜 F] {G : Type u_8} [normed_group G] [normed_space 𝕜 G] (L : E →L[𝕜] F →L[𝕜] G) {f : α → E} {g : α → F} (hf : measure_theory.ae_strongly_measurable f μ) (hg : measure_theory.ae_strongly_measurable g μ) :
measure_theory.ae_strongly_measurable (λ (x : α), (L (f x)) (g x)) μ
theorem ae_strongly_measurable_with_density_iff {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_2} [normed_group E] [normed_space E] {f : α → nnreal} (hf : measurable f) {g : α → E} :

Almost everywhere finitely strongly measurable functions #

@[protected]
noncomputable def measure_theory.ae_fin_strongly_measurable.mk {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] [has_zero β] (f : α → β) (hf : measure_theory.ae_fin_strongly_measurable f μ) :
α → β

A fin_strongly_measurable function such that f =ᵐ[μ] hf.mk f. See lemmas fin_strongly_measurable_mk and ae_eq_mk.

Equations
@[protected]
theorem measure_theory.ae_fin_strongly_measurable.const_smul {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {f : α → β} {𝕜 : Type u_3} [topological_space 𝕜] [add_monoid β] [monoid 𝕜] [distrib_mul_action 𝕜 β] [has_continuous_smul 𝕜 β] (hf : measure_theory.ae_fin_strongly_measurable f μ) (c : 𝕜) :

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.

theorem measure_theory.measurable_uncurry_of_continuous_of_measurable {α : Type u_1} {β : Type u_2} {ι : Type u_3} [topological_space ι] [topological_space.metrizable_space ι] [measurable_space ι] [topological_space.second_countable_topology ι] [opens_measurable_space ι] {mβ : measurable_space β} [topological_space β] [topological_space.pseudo_metrizable_space β] [borel_space β] {m : measurable_space α} {u : ι → α → β} (hu_cont : ∀ (x : α), continuous (λ (i : ι), u i x)) (h : ∀ (i : ι), measurable (u i)) :