# mathlibdocumentation

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 #

• `strongly_measurable f`: `f : α → β` is the limit of a sequence `fs : ℕ → simple_func α β`.

• `fin_strongly_measurable f μ`: `f : α → β` is the limit of a sequence `fs : ℕ → simple_func α β` such that for all `n ∈ ℕ`, the measure of the support of `fs n` is finite.

• `ae_strongly_measurable f μ`: `f` is almost everywhere equal to a `strongly_measurable` function.

• `ae_fin_strongly_measurable f μ`: `f` is almost everywhere equal to a `fin_strongly_measurable` function.

• `ae_fin_strongly_measurable.sigma_finite_set`: a measurable set `t` such that `f =ᵐ[μ.restrict tᶜ] 0` and `μ.restrict t` is sigma-finite.

## Main statements #

• `ae_fin_strongly_measurable.exists_set_sigma_finite`: there exists a measurable set `t` such that `f =ᵐ[μ.restrict tᶜ] 0` and `μ.restrict t` is sigma-finite.

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

## References #

• Hytönen, Tuomas, Jan Van Neerven, Mark Veraar, and Lutz Weis. Analysis in Banach spaces. Springer, 2016.
@[class]
structure second_countable_topology_either (α : Type u_1) (β : Type u_2)  :
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
@[protected, instance]
def second_countable_topology_either_of_left (α : Type u_1) (β : Type u_2)  :
@[protected, instance]
def second_countable_topology_either_of_right (α : Type u_1) (β : Type u_2)  :
def measure_theory.strongly_measurable {α : Type u_1} {β : Type u_2} (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} [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} {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
• = ∃ (g : α → β),
def measure_theory.ae_fin_strongly_measurable {α : Type u_1} {β : Type u_2} [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
• = ∃ (g : α → β),

## Strongly measurable functions #

theorem measure_theory.strongly_measurable.ae_strongly_measurable {α : Type u_1} {β : Type u_2} {m0 : measurable_space α} {f : α → β} {μ : measure_theory.measure α}  :
@[simp]
theorem measure_theory.subsingleton.strongly_measurable {α : Type u_1} {β : Type u_2} [subsingleton β] (f : α → β) :
theorem measure_theory.simple_func.strongly_measurable {α : Type u_1} {β : Type u_2} {m : measurable_space α} (f : β) :
theorem measure_theory.strongly_measurable_of_is_empty {α : Type u_1} {β : Type u_2} [is_empty α] {m : measurable_space α} (f : α → β) :
theorem measure_theory.strongly_measurable_const {α : Type u_1} {β : Type u_2} {m : measurable_space α} {b : β} :
theorem measure_theory.strongly_measurable_one {α : Type u_1} {β : Type u_2} {m : measurable_space α} [has_one β] :
theorem measure_theory.strongly_measurable_zero {α : Type u_1} {β : Type u_2} {m : measurable_space α} [has_zero β] :
theorem measure_theory.strongly_measurable_const' {α : Type u_1} {β : Type u_2} {m : measurable_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]
theorem measure_theory.subsingleton.strongly_measurable' {α : Type u_1} {β : Type u_2} [subsingleton α] (f : α → β) :
@[protected]
noncomputable def measure_theory.strongly_measurable.approx {α : Type u_1} {β : Type u_2} {f : α → β} {m : measurable_space α}  :

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 : α → β} {m : measurable_space α} (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 : α → β} [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]
theorem measure_theory.strongly_measurable.fin_strongly_measurable {α : Type u_1} {β : Type u_2} {f : α → β} [has_zero β] {m0 : measurable_space α} (μ : measure_theory.measure α)  :

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 : α → β} {m : measurable_space α} [borel_space β]  :

A strongly measurable function is measurable.

@[protected]
theorem measure_theory.strongly_measurable.ae_measurable {α : Type u_1} {β : Type u_2} {f : α → β} {m : measurable_space α} [borel_space β] {μ : measure_theory.measure α}  :

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 α} {g : β → γ} {f : α → β} (hg : continuous g)  :
measure_theory.strongly_measurable (λ (x : α), g (f x))
theorem measure_theory.strongly_measurable.measurable_set_mul_support {α : Type u_1} {β : Type u_2} {f : α → β} {m : measurable_space α} [has_one β]  :
theorem measure_theory.strongly_measurable.measurable_set_support {α : Type u_1} {β : Type u_2} {f : α → β} {m : measurable_space α} [has_zero β]  :
@[protected]
theorem measure_theory.strongly_measurable.mono {α : Type u_1} {β : Type u_2} {f : α → β} {m m' : measurable_space α} (h_mono : m' m) :
@[protected]
theorem measure_theory.strongly_measurable.prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {f : α → β} {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} {m : measurable_space α} {m' : measurable_space γ} {f : α → β} {g : γ → α} (hg : measurable g) :
theorem measure_theory.strongly_measurable.of_uncurry_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : measurable_space α} {mγ : measurable_space γ} {f : α → γ → β} {x : α} :
theorem measure_theory.strongly_measurable.of_uncurry_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : measurable_space α} {mγ : measurable_space γ} {f : α → γ → β} {y : γ} :
@[protected]
theorem measure_theory.strongly_measurable.mul {α : Type u_1} {β : Type u_2} {f g : α → β} {mα : measurable_space α} [has_mul β]  :
@[protected]
theorem measure_theory.strongly_measurable.add {α : Type u_1} {β : Type u_2} {f g : α → β} {mα : measurable_space α} [has_add β]  :
theorem measure_theory.strongly_measurable.mul_const {α : Type u_1} {β : Type u_2} {f : α → β} {mα : measurable_space α} [has_mul β] (c : β) :
theorem measure_theory.strongly_measurable.add_const {α : Type u_1} {β : Type u_2} {f : α → β} {mα : measurable_space α} [has_add β] (c : β) :
theorem measure_theory.strongly_measurable.const_mul {α : Type u_1} {β : Type u_2} {f : α → β} {mα : measurable_space α} [has_mul β] (c : β) :
theorem measure_theory.strongly_measurable.const_add {α : Type u_1} {β : Type u_2} {f : α → β} {mα : measurable_space α} [has_add β] (c : β) :
@[protected]
theorem measure_theory.strongly_measurable.inv {α : Type u_1} {β : Type u_2} {f : α → β} {mα : measurable_space α} [group β]  :
@[protected]
theorem measure_theory.strongly_measurable.neg {α : Type u_1} {β : Type u_2} {f : α → β} {mα : measurable_space α} [add_group β]  :
@[protected]
theorem measure_theory.strongly_measurable.div {α : Type u_1} {β : Type u_2} {f g : α → β} {mα : measurable_space α} [has_div β]  :
@[protected]
theorem measure_theory.strongly_measurable.sub {α : Type u_1} {β : Type u_2} {f g : α → β} {mα : measurable_space α} [has_sub β]  :
@[protected]
theorem measure_theory.strongly_measurable.vadd {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {𝕜 : Type u_3} [ β] [ β] {f : α → 𝕜} {g : α → β}  :
@[protected]
theorem measure_theory.strongly_measurable.smul {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {𝕜 : Type u_3} [ β] [ β] {f : α → 𝕜} {g : α → β}  :
@[protected]
theorem measure_theory.strongly_measurable.const_smul {α : Type u_1} {β : Type u_2} {f : α → β} {mα : measurable_space α} {𝕜 : Type u_3} [ β] (c : 𝕜) :
@[protected]
theorem measure_theory.strongly_measurable.const_smul' {α : Type u_1} {β : Type u_2} {f : α → β} {mα : measurable_space α} {𝕜 : Type u_3} [ β] (c : 𝕜) :
@[protected]
theorem measure_theory.strongly_measurable.smul_const {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {𝕜 : Type u_3} [ β] [ β] {f : α → 𝕜} (c : β) :
@[protected]
theorem measure_theory.strongly_measurable.vadd_const {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {𝕜 : Type u_3} [ β] [ β] {f : α → 𝕜} (c : β) :
theorem strongly_measurable_const_smul_iff {α : Type u_1} {β : Type u_2} {f : α → β} {G : Type u_5} [group G] [ β] {m : measurable_space α} (c : G) :
theorem strongly_measurable_const_smul_iff₀ {α : Type u_1} {β : Type u_2} {f : α → β} {G₀ : Type u_6} [group_with_zero G₀] [ β] {m : measurable_space α} {c : G₀} (hc : c 0) :
@[protected]
theorem measure_theory.strongly_measurable.sup {α : Type u_1} {β : Type u_2} {f g : α → β} [has_sup β]  :
@[protected]
theorem measure_theory.strongly_measurable.inf {α : Type u_1} {β : Type u_2} {f g : α → β} [has_inf β]  :

### Big operators: `∏` and `∑`#

theorem list.strongly_measurable_sum' {α : Type u_1} {M : Type u_5} [add_monoid M] {m : measurable_space α} (l : list (α → M)) (hl : ∀ (f : α → M), ) :
theorem list.strongly_measurable_prod' {α : Type u_1} {M : Type u_5} [monoid M] {m : measurable_space α} (l : list (α → M)) (hl : ∀ (f : α → M), ) :
theorem list.strongly_measurable_sum {α : Type u_1} {M : Type u_5} [add_monoid M] {m : measurable_space α} (l : list (α → M)) (hl : ∀ (f : α → M), ) :
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] {m : measurable_space α} (l : list (α → M)) (hl : ∀ (f : α → M), ) :
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} {m : measurable_space α} (l : multiset (α → M)) (hl : ∀ (f : α → M), ) :
theorem multiset.strongly_measurable_prod' {α : Type u_1} {M : Type u_5} [comm_monoid M] {m : measurable_space α} (l : multiset (α → M)) (hl : ∀ (f : α → M), ) :
theorem multiset.strongly_measurable_sum {α : Type u_1} {M : Type u_5} {m : measurable_space α} (s : multiset (α → M)) (hs : ∀ (f : α → M), ) :
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] {m : measurable_space α} (s : multiset (α → M)) (hs : ∀ (f : α → M), ) :
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} {m : measurable_space α} {ι : Type u_2} {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i s) :
theorem finset.strongly_measurable_prod' {α : Type u_1} {M : Type u_5} [comm_monoid M] {m : measurable_space α} {ι : Type u_2} {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i s) :
theorem finset.strongly_measurable_prod {α : Type u_1} {M : Type u_5} [comm_monoid M] {m : measurable_space α} {ι : Type u_2} {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i s) :
measure_theory.strongly_measurable (λ (a : α), s.prod (λ (i : ι), f i a))
theorem finset.strongly_measurable_sum {α : Type u_1} {M : Type u_5} {m : measurable_space α} {ι : Type u_2} {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i s) :
measure_theory.strongly_measurable (λ (a : α), s.sum (λ (i : ι), f i a))
theorem measure_theory.strongly_measurable.is_separable_range {α : Type u_1} {β : Type u_2} {f : α → β} {m : measurable_space α}  :

The range of a strongly measurable function is separable.

theorem measure_theory.strongly_measurable.separable_space_range_union_singleton {α : Type u_1} {β : Type u_2} {f : α → β} {m : measurable_space α} {b : β} :
theorem measurable.strongly_measurable {α : Type u_1} {β : Type u_2} {f : α → β} {mα : measurable_space α} (hf : measurable f) :

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

theorem strongly_measurable_iff_measurable {α : Type u_1} {β : Type u_2} {f : α → β} {mα : measurable_space α} [borel_space β]  :

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

theorem strongly_measurable_iff_measurable_separable {α : Type u_1} {β : Type u_2} {f : α → β} {m : measurable_space α} [borel_space β] :

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

theorem continuous.strongly_measurable {α : Type u_1} {β : Type u_2} [h : β] {f : α → β} (hf : continuous f) :

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

theorem embedding.comp_strongly_measurable_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {g : β → γ} {f : α → β} (hg : embedding g) :
measure_theory.strongly_measurable (λ (x : α), g (f x))

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 α} (u : filter ι) [u.ne_bot] {f : ι → α → β} {g : α → β} (hf : ∀ (i : ι), ) (lim : (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 α} {s : set α} {_x : decidable_pred (λ (_x : α), _x s)} (hs : measurable_set s)  :
@[protected]
theorem measure_theory.strongly_measurable.ite {α : Type u_1} {β : Type u_2} {f g : α → β} {m : measurable_space α} {p : α → Prop} {_x : decidable_pred p} (hp : measurable_set {a : α | p a})  :
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 α} {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)) :
theorem strongly_measurable_of_restrict_of_restrict_compl {α : Type u_1} {β : Type u_2} {m : measurable_space α} {f : α → β} {s : set α} (hs : measurable_set s) (h₁ : measure_theory.strongly_measurable (s.restrict f)) (h₂ : measure_theory.strongly_measurable (s.restrict f)) :
@[protected]
theorem measure_theory.strongly_measurable.indicator {α : Type u_1} {β : Type u_2} {f : α → β} {m : measurable_space α} [has_zero β] {s : set α} (hs : measurable_set s) :
@[protected]
theorem measure_theory.strongly_measurable.dist {α : Type u_1} {m : measurable_space α} {β : Type u_2} {f g : α → β}  :
@[protected]
theorem measure_theory.strongly_measurable.norm {α : Type u_1} {m : measurable_space α} {β : Type u_2} [normed_group β] {f : α → β}  :
@[protected]
theorem measure_theory.strongly_measurable.nnnorm {α : Type u_1} {m : measurable_space α} {β : Type u_2} [normed_group β] {f : α → β}  :
@[protected]
theorem measure_theory.strongly_measurable.ennnorm {α : Type u_1} {m : measurable_space α} {β : Type u_2} [normed_group β] {f : α → β}  :
measurable (λ (a : α), f a∥₊)
@[protected]
theorem measure_theory.strongly_measurable.real_to_nnreal {α : Type u_1} {m : measurable_space α} {f : α → }  :
theorem measurable_embedding.strongly_measurable_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} {g' : γ → β} {mα : measurable_space α} {mγ : measurable_space γ} (hg : measurable_embedding g) (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 γ} (hg : measurable_embedding g) (hne : γ → ) :
∃ (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 𝕜] [ E] {m : measurable_space α} {f g : α → E}  :
theorem measure_theory.strongly_measurable.measurable_set_eq_fun {α : Type u_1} {m : measurable_space α} {E : Type u_2} {f g : α → E}  :
measurable_set {x : α | f x = g x}
theorem measure_theory.strongly_measurable.measurable_set_lt {α : Type u_1} {β : Type u_2} {m : measurable_space α} [linear_order β] {f g : α → β}  :
measurable_set {a : α | f a < g a}
theorem measure_theory.strongly_measurable.measurable_set_le {α : Type u_1} {β : Type u_2} {m : measurable_space α} [preorder β] {f g : α → β}  :
measurable_set {a : α | f a g a}
theorem measure_theory.strongly_measurable.strongly_measurable_in_set {α : Type u_1} {β : Type u_2} {m : measurable_space α} [has_zero β] {s : set α} {f : α → β} (hs : measurable_set s) (hf_zero : ∀ (x : α), x sf x = 0) :
∃ (fs : , (∀ (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 α} [has_zero E] {s : set α} {f : α → E} (hs_m : measurable_set s) (hs : ∀ (t : set α), measurable_set (s t)measurable_set (s t)) (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 #

theorem measure_theory.fin_strongly_measurable_zero {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [has_zero β]  :
theorem measure_theory.fin_strongly_measurable.ae_fin_strongly_measurable {α : Type u_1} {β : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [has_zero β]  :
@[protected]
noncomputable def measure_theory.fin_strongly_measurable.approx {α : Type u_1} {β : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [has_zero β]  :

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 β] (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 β] (x : α) :
filter.tendsto (λ (n : ), (hf.approx n) x) filter.at_top (nhds (f x))
@[protected]
theorem measure_theory.fin_strongly_measurable.strongly_measurable {α : Type u_1} {β : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [has_zero β]  :
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 β] [t2_space β]  :
∃ (t : set α), (∀ (x : α), x tf x = 0)
@[protected]
theorem measure_theory.fin_strongly_measurable.measurable {α : Type u_1} {β : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [has_zero β] [borel_space β]  :

A finitely strongly measurable function is measurable.

@[protected]
theorem measure_theory.fin_strongly_measurable.mul {α : Type u_1} {β : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α → β}  :
@[protected]
theorem measure_theory.fin_strongly_measurable.add {α : Type u_1} {β : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α → β} [add_monoid β]  :
@[protected]
theorem measure_theory.fin_strongly_measurable.neg {α : Type u_1} {β : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [add_group β]  :
@[protected]
theorem measure_theory.fin_strongly_measurable.sub {α : Type u_1} {β : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α → β} [add_group β]  :
@[protected]
theorem measure_theory.fin_strongly_measurable.const_smul {α : Type u_1} {β : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → β} {𝕜 : Type u_3} [add_monoid β] [monoid 𝕜] [ β] [ β] (c : 𝕜) :
@[protected]
theorem measure_theory.fin_strongly_measurable.sup {α : Type u_1} {β : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α → β} [has_zero β]  :
@[protected]
theorem measure_theory.fin_strongly_measurable.inf {α : Type u_1} {β : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α → β} [has_zero β]  :
theorem measure_theory.fin_strongly_measurable_iff_strongly_measurable_and_exists_set_sigma_finite {α : Type u_1} {β : Type u_2} {f : α → β} [t2_space β] [has_zero β] {m : measurable_space α} {μ : measure_theory.measure α} :
∃ (t : set α), (∀ (x : α), x tf x = 0)
theorem measure_theory.ae_fin_strongly_measurable_zero {α : Type u_1} {β : Type u_2} {m : measurable_space α} (μ : measure_theory.measure α) [has_zero β]  :

## Almost everywhere strongly measurable functions #

theorem measure_theory.ae_strongly_measurable_const {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {b : β} :
theorem measure_theory.ae_strongly_measurable_zero {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [has_zero β] :
theorem measure_theory.ae_strongly_measurable_one {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [has_one β] :
@[simp]
theorem measure_theory.subsingleton.ae_strongly_measurable {α : Type u_1} {β : Type u_2} {m : measurable_space α} [subsingleton β] {μ : measure_theory.measure α} (f : α → β) :
@[simp]
theorem measure_theory.subsingleton.ae_strongly_measurable' {α : Type u_1} {β : Type u_2} {m : measurable_space α} [subsingleton α] {μ : measure_theory.measure α} (f : α → β) :
@[simp]
theorem measure_theory.ae_measurable_zero_measure {α : Type u_1} {β : Type u_2} (f : α → β) :
theorem measure_theory.simple_func.ae_strongly_measurable {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} (f : β) :
@[protected]
noncomputable def measure_theory.ae_strongly_measurable.mk {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} (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.strongly_measurable_mk {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β}  :
theorem measure_theory.ae_strongly_measurable.measurable_mk {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [borel_space β]  :
theorem measure_theory.ae_strongly_measurable.ae_eq_mk {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β}  :
@[protected]
theorem measure_theory.ae_strongly_measurable.ae_measurable {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} [borel_space β] {f : α → β}  :
theorem measure_theory.ae_strongly_measurable.congr {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α → β} (h : f =ᵐ[μ] g) :
theorem ae_strongly_measurable_congr {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α → β} (h : f =ᵐ[μ] g) :
theorem measure_theory.ae_strongly_measurable.mono_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} {ν : measure_theory.measure α} (h : ν μ) :
@[protected]
theorem measure_theory.ae_strongly_measurable.mono' {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} {ν : measure_theory.measure α} (h' : ν.absolutely_continuous μ) :
theorem measure_theory.ae_strongly_measurable.mono_set {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} {s t : set α} (h : s t) (ht : (μ.restrict t)) :
@[protected]
theorem measure_theory.ae_strongly_measurable.restrict {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} (hfm : μ) {s : set α} :
theorem measure_theory.ae_strongly_measurable.ae_mem_imp_eq_mk {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} {s : set α} (h : (μ.restrict s)) :
∀ᵐ (x : α) ∂μ, x s
theorem continuous.comp_ae_strongly_measurable {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} {g : β → γ} {f : α → β} (hg : continuous g)  :
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.

theorem continuous.ae_strongly_measurable {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} (hf : continuous f) :

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 α} {f : α → β} {g : α → γ}  :
measure_theory.ae_strongly_measurable (λ (x : α), (f x, g x)) μ
theorem measurable.ae_strongly_measurable {α : Type u_1} {β : Type u_2} {f : α → β} {m : measurable_space α} {μ : measure_theory.measure α} (hf : measurable f) :

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

@[protected]
theorem measure_theory.ae_strongly_measurable.add {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α → β} [has_add β]  :
@[protected]
theorem measure_theory.ae_strongly_measurable.mul {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α → β} [has_mul β]  :
@[protected]
theorem measure_theory.ae_strongly_measurable.add_const {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [has_add β] (c : β) :
@[protected]
theorem measure_theory.ae_strongly_measurable.mul_const {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [has_mul β] (c : β) :
@[protected]
theorem measure_theory.ae_strongly_measurable.const_mul {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [has_mul β] (c : β) :
@[protected]
theorem measure_theory.ae_strongly_measurable.const_add {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [has_add β] (c : β) :
@[protected]
theorem measure_theory.ae_strongly_measurable.neg {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [add_group β]  :
@[protected]
theorem measure_theory.ae_strongly_measurable.inv {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [group β]  :
@[protected]
theorem measure_theory.ae_strongly_measurable.sub {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α → β} [add_group β]  :
@[protected]
theorem measure_theory.ae_strongly_measurable.div {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α → β} [group β]  :
@[protected]
theorem measure_theory.ae_strongly_measurable.smul {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_3} [ β] [ β] {f : α → 𝕜} {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 α} {𝕜 : Type u_3} [ β] [ β] {f : α → 𝕜} {g : α → β}  :
@[protected]
theorem measure_theory.ae_strongly_measurable.const_smul {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} {𝕜 : Type u_3} [ β] (c : 𝕜) :
@[protected]
theorem measure_theory.ae_strongly_measurable.const_smul' {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} {𝕜 : Type u_3} [ β] (c : 𝕜) :
@[protected]
theorem measure_theory.ae_strongly_measurable.vadd_const {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_3} [ β] [ β] {f : α → 𝕜} (c : β) :
@[protected]
theorem measure_theory.ae_strongly_measurable.smul_const {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_3} [ β] [ β] {f : α → 𝕜} (c : β) :
@[protected]
theorem measure_theory.ae_strongly_measurable.sup {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α → β}  :
@[protected]
theorem measure_theory.ae_strongly_measurable.inf {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α → β}  :

### Big operators: `∏` and `∑`#

theorem list.ae_strongly_measurable_prod' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {M : Type u_5} [monoid M] (l : list (α → M)) (hl : ∀ (f : α → M), ) :
theorem list.ae_strongly_measurable_sum' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {M : Type u_5} [add_monoid M] (l : list (α → M)) (hl : ∀ (f : α → M), ) :
theorem list.ae_strongly_measurable_prod {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {M : Type u_5} [monoid M] (l : list (α → M)) (hl : ∀ (f : α → M), ) :
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] (l : list (α → M)) (hl : ∀ (f : α → M), ) :
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] (l : multiset (α → M)) (hl : ∀ (f : α → M), ) :
theorem multiset.ae_strongly_measurable_sum' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {M : Type u_5} (l : multiset (α → M)) (hl : ∀ (f : α → M), ) :
theorem multiset.ae_strongly_measurable_prod {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {M : Type u_5} [comm_monoid M] (s : multiset (α → M)) (hs : ∀ (f : α → M), ) :
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} (s : multiset (α → M)) (hs : ∀ (f : α → M), ) :
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] {ι : Type u_2} {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i s) :
theorem finset.ae_strongly_measurable_sum' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {M : Type u_5} {ι : Type u_2} {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i s) :
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} {ι : Type u_2} {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i s) :
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] {ι : Type u_2} {f : ι → α → M} (s : finset ι) (hf : ∀ (i : ι), i s) :
measure_theory.ae_strongly_measurable (λ (a : α), s.prod (λ (i : ι), f i a)) μ
theorem ae_measurable.ae_strongly_measurable {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} (hf : μ) :

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

theorem ae_strongly_measurable_id {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} :
theorem ae_strongly_measurable_iff_ae_measurable {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [borel_space β]  :

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

@[protected]
theorem measure_theory.ae_strongly_measurable.dist {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} {f g : α → β}  :
@[protected]
theorem measure_theory.ae_strongly_measurable.norm {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} [normed_group β] {f : α → β}  :
@[protected]
theorem measure_theory.ae_strongly_measurable.nnnorm {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} [normed_group β] {f : α → β}  :
@[protected]
theorem measure_theory.ae_strongly_measurable.ennnorm {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} [normed_group β] {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 : α → β}  :
ae_measurable (λ (a : α), has_edist.edist (f a) (g a)) μ
@[protected]
@[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 : α → 𝕜}  :
@[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 : α → 𝕜}  :
@[protected]
theorem measure_theory.ae_strongly_measurable.inner {α : Type u_1} {𝕜 : Type u_5} {E : Type u_6} [is_R_or_C 𝕜] [ E] {m : measurable_space α} {μ : measure_theory.measure α} {f g : α → E}  :
theorem ae_strongly_measurable_indicator_iff {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [has_zero β] {s : set α} (hs : measurable_set s) :
@[protected]
theorem measure_theory.ae_strongly_measurable.indicator {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [has_zero β] (hfm : μ) {s : set α} (hs : measurable_set s) :
theorem ae_strongly_measurable_of_ae_strongly_measurable_trim {β : Type u_2} {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) {f : α → β} (hf : (μ.trim hm)) :
theorem measure_theory.ae_strongly_measurable.comp_ae_measurable {α : Type u_1} {β : Type u_2} {g : α → β} {γ : Type u_3} {mγ : measurable_space γ} {mα : measurable_space α} {f : γ → α} {μ : measure_theory.measure γ} (hf : μ) :
theorem measure_theory.ae_strongly_measurable.comp_measurable {α : Type u_1} {β : Type u_2} {g : α → β} {γ : Type u_3} {mγ : measurable_space γ} {mα : measurable_space α} {f : γ → α} {μ : measure_theory.measure γ} (hf : measurable f) :
theorem measure_theory.ae_strongly_measurable.comp_measurable' {α : Type u_1} {β : Type u_2} {g : α → β} {γ : Type u_3} {mγ : measurable_space γ} {mα : measurable_space α} {f : γ → α} {μ : measure_theory.measure γ} {ν : measure_theory.measure α} (hf : measurable f) (h : ν) :
theorem measure_theory.ae_strongly_measurable.is_separable_ae_range {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β}  :
∃ (t : set β), ∀ᵐ (x : α) ∂μ, f x t
theorem ae_strongly_measurable_iff_ae_measurable_separable {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [borel_space β] :
∃ (t : set β), ∀ᵐ (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 measurable_embedding.ae_strongly_measurable_map_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mγ : measurable_space γ} {mα : measurable_space α} {f : γ → α} {μ : measure_theory.measure γ} (hf : measurable_embedding f) {g : α → β} :
theorem embedding.ae_strongly_measurable_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} {g : β → γ} {f : α → β} (hg : embedding g) :
measure_theory.ae_strongly_measurable (λ (x : α), g (f x)) μ
theorem measure_theory.measure_preserving.ae_strongly_measurable_comp_iff {α : Type u_1} {γ : Type u_3} {β : Type u_2} {f : α → β} {mα : measurable_space α} {μa : measure_theory.measure α} {mβ : measurable_space β} {μb : measure_theory.measure β} (hf : μ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 α} {ι : Type u_3} (u : filter ι) [u.ne_bot] {f : ι → α → β} {g : α → β} (hf : ∀ (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 α} {f : α → β} (hf : ∀ (n : ), ) (h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), filter.tendsto (λ (n : ), f n x) filter.at_top (nhds l)) :
∃ (f_lim : α → β) (hf_lim_meas : , ∀ᵐ (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.

theorem measure_theory.ae_strongly_measurable.sum_measure {α : Type u_1} {β : Type u_2} {ι : Type u_4} [encodable ι] {f : α → β} {m : measurable_space α} {μ : ι → } (h : ∀ (i : ι), ) :
@[simp]
theorem ae_strongly_measurable_sum_measure_iff {α : Type u_1} {β : Type u_2} {ι : Type u_4} [encodable ι] {f : α → β} {m : measurable_space α} {μ : ι → } :
∀ (i : ι),
@[simp]
theorem ae_strongly_measurable_add_measure_iff {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} {ν : measure_theory.measure α} :
theorem measure_theory.ae_strongly_measurable.add_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {ν : measure_theory.measure α} {f : α → β}  :
@[protected]
theorem measure_theory.ae_strongly_measurable.Union {α : Type u_1} {β : Type u_2} {ι : Type u_4} [encodable ι] {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} {s : ι → set α} (h : ∀ (i : ι), (μ.restrict (s i))) :
(μ.restrict (⋃ (i : ι), 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 α} {f : α → β} {s : ι → set α} :
(μ.restrict (⋃ (i : ι), s i)) ∀ (i : ι), (μ.restrict (s i))
@[simp]
theorem ae_strongly_measurable_union_iff {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} {s t : set α} :
theorem measure_theory.ae_strongly_measurable.smul_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} {R : Type u_3} [monoid R] (c : R) :
theorem ae_strongly_measurable_smul_const_iff {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} {E : Type u_6} [normed_group E] [ 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 α} {f : α → β} {G : Type u_5} [group G] [ β] (c : G) :
theorem ae_strongly_measurable_const_smul_iff₀ {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} {G₀ : Type u_6} [group_with_zero G₀] [ β] {c : G₀} (hc : c 0) :
theorem strongly_measurable.apply_continuous_linear_map {α : Type u_1} {𝕜 : Type u_5} {E : Type u_6} [normed_group E] [ E] {F : Type u_7} [normed_group F] [ F] {m : measurable_space α} {φ : α → (F →L[𝕜] E)} (v : F) :
theorem measure_theory.ae_strongly_measurable.apply_continuous_linear_map {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} {E : Type u_6} [normed_group E] [ E] {F : Type u_7} [normed_group F] [ F] {φ : α → (F →L[𝕜] E)} (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} {E : Type u_6} [normed_group E] [ E] {F : Type u_7} [normed_group F] [ F] {G : Type u_8} [normed_group G] [ G] (L : E →L[𝕜] F →L[𝕜] G) {f : α → E} {g : α → F}  :
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] [ E] {f : α → nnreal} (hf : measurable f) {g : α → E} :
(μ.with_density (λ (x : α), (f x))) measure_theory.ae_strongly_measurable (λ (x : α), (f x) g x) μ

## 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 α} [has_zero β] (f : α → β)  :
α → β

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

Equations
theorem measure_theory.ae_fin_strongly_measurable.fin_strongly_measurable_mk {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [has_zero β]  :
theorem measure_theory.ae_fin_strongly_measurable.ae_eq_mk {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [has_zero β]  :
@[protected]
theorem measure_theory.ae_fin_strongly_measurable.ae_measurable {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} [has_zero β] [borel_space β] {f : α → β}  :
@[protected]
theorem measure_theory.ae_fin_strongly_measurable.mul {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α → β}  :
@[protected]
theorem measure_theory.ae_fin_strongly_measurable.add {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α → β} [add_monoid β]  :
@[protected]
theorem measure_theory.ae_fin_strongly_measurable.neg {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [add_group β]  :
@[protected]
theorem measure_theory.ae_fin_strongly_measurable.sub {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α → β} [add_group β]  :
@[protected]
theorem measure_theory.ae_fin_strongly_measurable.const_smul {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} {𝕜 : Type u_3} [add_monoid β] [monoid 𝕜] [ β] [ β] (c : 𝕜) :
@[protected]
theorem measure_theory.ae_fin_strongly_measurable.sup {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α → β} [has_zero β]  :
@[protected]
theorem measure_theory.ae_fin_strongly_measurable.inf {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f g : α → β} [has_zero β]  :
theorem measure_theory.ae_fin_strongly_measurable.exists_set_sigma_finite {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [has_zero β] [t2_space β]  :
∃ (t : set α), f =ᵐ[μ.restrict t] 0
def measure_theory.ae_fin_strongly_measurable.sigma_finite_set {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [has_zero β] [t2_space β]  :
set α

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

Equations
@[protected]
theorem measure_theory.ae_fin_strongly_measurable.measurable_set {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [has_zero β] [t2_space β]  :
theorem measure_theory.ae_fin_strongly_measurable.ae_eq_zero_compl {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [has_zero β] [t2_space β]  :
f =ᵐ[] 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 α} {f : α → β} [has_zero β] [t2_space β]  :
theorem measure_theory.fin_strongly_measurable_iff_measurable {α : Type u_1} {G : Type u_5} [normed_group G] [borel_space G] {f : α → G} {m0 : measurable_space α} (μ : measure_theory.measure α)  :

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_5} [normed_group G] [borel_space G] {f : α → G} {m0 : measurable_space α} (μ : measure_theory.measure α)  :

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} {mβ : measurable_space β} [borel_space β] {m : measurable_space α} {u : ι → α → β} (hu_cont : ∀ (x : α), continuous (λ (i : ι), u i x)) (h : ∀ (i : ι), measurable (u i)) :
theorem measure_theory.strongly_measurable_uncurry_of_continuous_of_strongly_measurable {α : Type u_1} {β : Type u_2} {ι : Type u_3} {u : ι → α → β} (hu_cont : ∀ (x : α), continuous (λ (i : ι), u i x)) (h : ∀ (i : ι), ) :