Strongly measurable and finitely strongly measurable functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 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_strongly_measurable f μ:fis almost everywhere equal to astrongly_measurablefunction. -
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.
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)
[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
@[protected, instance]
def
second_countable_topology_either_of_left
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[topological_space β]
[topological_space.second_countable_topology α] :
@[protected, instance]
def
second_countable_topology_either_of_right
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[topological_space β]
[topological_space.second_countable_topology β] :
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 (nhds (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 (nhds (f x))
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
- measure_theory.ae_strongly_measurable f μ = ∃ (g : α → β), measure_theory.strongly_measurable g ∧ f =ᵐ[μ] g
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 #
@[protected]
theorem
measure_theory.strongly_measurable.ae_strongly_measurable
{α : Type u_1}
{β : Type u_2}
{m0 : measurable_space α}
[topological_space β]
{f : α → β}
{μ : measure_theory.measure α}
(hf : measure_theory.strongly_measurable f) :
@[simp]
theorem
measure_theory.subsingleton.strongly_measurable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[topological_space β]
[subsingleton β]
(f : α → β) :
theorem
measure_theory.simple_func.strongly_measurable
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
[topological_space β]
(f : measure_theory.simple_func α β) :
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 : β} :
measure_theory.strongly_measurable (λ (a : α), b)
theorem
measure_theory.strongly_measurable_one
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
[topological_space β]
[has_one β] :
theorem
measure_theory.strongly_measurable_zero
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
[topological_space β]
[has_zero β] :
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]
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 : α → β}
[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
- hf.approx = Exists.some hf
@[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))
noncomputable
def
measure_theory.strongly_measurable.approx_bounded
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[topological_space β]
{m : measurable_space α}
[has_norm β]
[has_smul ℝ β]
(hf : measure_theory.strongly_measurable f)
(c : ℝ) :
Similar to strongly_measurable.approx, but enforces that the norm of every function in the
sequence is less than c everywhere. If ‖f x‖ ≤ c this sequence of simple functions verifies
tendsto (λ n, hf.approx_bounded n x) at_top (𝓝 (f x)).
Equations
- hf.approx_bounded c = λ (n : ℕ), measure_theory.simple_func.map (λ (x : β), linear_order.min 1 (c / ‖x‖) • x) (hf.approx n)
theorem
measure_theory.strongly_measurable.tendsto_approx_bounded_of_norm_le
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[normed_add_comm_group β]
[normed_space ℝ β]
{m : measurable_space α}
(hf : measure_theory.strongly_measurable f)
{c : ℝ}
{x : α}
(hfx : ‖f x‖ ≤ c) :
filter.tendsto (λ (n : ℕ), ⇑(hf.approx_bounded c n) x) filter.at_top (nhds (f x))
theorem
measure_theory.strongly_measurable.tendsto_approx_bounded_ae
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[normed_add_comm_group β]
[normed_space ℝ β]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hf : measure_theory.strongly_measurable f)
{c : ℝ}
(hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c) :
∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ℕ), ⇑(hf.approx_bounded c n) x) filter.at_top (nhds (f x))
theorem
measure_theory.strongly_measurable.norm_approx_bounded_le
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[seminormed_add_comm_group β]
[normed_space ℝ β]
{m : measurable_space α}
{c : ℝ}
(hf : measure_theory.strongly_measurable f)
(hc : 0 ≤ c)
(n : ℕ)
(x : α) :
‖⇑(hf.approx_bounded c n) x‖ ≤ c
theorem
strongly_measurable_bot_iff
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[topological_space β]
[nonempty β]
[t2_space β] :
measure_theory.strongly_measurable f ↔ ∃ (c : β), f = λ (_x : α), c
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 : α → β}
{m : measurable_space α}
[topological_space β]
[topological_space.pseudo_metrizable_space β]
[measurable_space β]
[borel_space β]
(hf : measure_theory.strongly_measurable f) :
A strongly measurable function is measurable.
@[protected]
theorem
measure_theory.strongly_measurable.ae_measurable
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{m : measurable_space α}
[topological_space β]
[topological_space.pseudo_metrizable_space β]
[measurable_space β]
[borel_space β]
{μ : measure_theory.measure α}
(hf : measure_theory.strongly_measurable f) :
ae_measurable f μ
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))
theorem
measure_theory.strongly_measurable.measurable_set_mul_support
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{m : measurable_space α}
[has_one β]
[topological_space β]
[topological_space.metrizable_space β]
(hf : measure_theory.strongly_measurable f) :
theorem
measure_theory.strongly_measurable.measurable_set_support
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{m : measurable_space α}
[has_zero β]
[topological_space β]
[topological_space.metrizable_space β]
(hf : measure_theory.strongly_measurable f) :
@[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 : γ} :
measure_theory.strongly_measurable (λ (x : α), f x y)
@[protected]
theorem
measure_theory.strongly_measurable.mul
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{mα : measurable_space α}
[topological_space β]
[has_mul β]
[has_continuous_mul β]
(hf : measure_theory.strongly_measurable f)
(hg : measure_theory.strongly_measurable g) :
@[protected]
theorem
measure_theory.strongly_measurable.add
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{mα : measurable_space α}
[topological_space β]
[has_add β]
[has_continuous_add β]
(hf : measure_theory.strongly_measurable f)
(hg : measure_theory.strongly_measurable g) :
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 : β) :
measure_theory.strongly_measurable (λ (x : α), f x * 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 : β) :
measure_theory.strongly_measurable (λ (x : α), f x + 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 : β) :
measure_theory.strongly_measurable (λ (x : α), c * f x)
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 : β) :
measure_theory.strongly_measurable (λ (x : α), c + f x)
@[protected]
theorem
measure_theory.strongly_measurable.inv
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{mα : measurable_space α}
[topological_space β]
[group β]
[topological_group β]
(hf : measure_theory.strongly_measurable f) :
@[protected]
theorem
measure_theory.strongly_measurable.neg
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{mα : measurable_space α}
[topological_space β]
[add_group β]
[topological_add_group β]
(hf : measure_theory.strongly_measurable f) :
@[protected]
theorem
measure_theory.strongly_measurable.div
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{mα : measurable_space α}
[topological_space β]
[has_div β]
[has_continuous_div β]
(hf : measure_theory.strongly_measurable f)
(hg : measure_theory.strongly_measurable g) :
@[protected]
theorem
measure_theory.strongly_measurable.sub
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{mα : measurable_space α}
[topological_space β]
[has_sub β]
[has_continuous_sub β]
(hf : measure_theory.strongly_measurable f)
(hg : measure_theory.strongly_measurable g) :
@[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) :
measure_theory.strongly_measurable (λ (x : α), f x +ᵥ g x)
@[protected]
theorem
measure_theory.strongly_measurable.smul
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
[topological_space β]
{𝕜 : Type u_3}
[topological_space 𝕜]
[has_smul 𝕜 β]
[has_continuous_smul 𝕜 β]
{f : α → 𝕜}
{g : α → β}
(hf : measure_theory.strongly_measurable f)
(hg : measure_theory.strongly_measurable g) :
measure_theory.strongly_measurable (λ (x : α), f x • g x)
@[protected]
theorem
measure_theory.strongly_measurable.const_smul
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{mα : measurable_space α}
[topological_space β]
{𝕜 : Type u_3}
[has_smul 𝕜 β]
[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_smul 𝕜 β]
[has_continuous_const_smul 𝕜 β]
(hf : measure_theory.strongly_measurable f)
(c : 𝕜) :
measure_theory.strongly_measurable (λ (x : α), c • f x)
@[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_smul 𝕜 β]
[has_continuous_smul 𝕜 β]
{f : α → 𝕜}
(hf : measure_theory.strongly_measurable f)
(c : β) :
measure_theory.strongly_measurable (λ (x : α), f x • 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 : β) :
measure_theory.strongly_measurable (λ (x : α), f x +ᵥ c)
theorem
strongly_measurable_const_smul_iff
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{G : Type u_6}
[topological_space β]
[group G]
[mul_action G β]
[has_continuous_const_smul G β]
{m : measurable_space α}
(c : G) :
measure_theory.strongly_measurable (λ (x : α), c • f x) ↔ measure_theory.strongly_measurable f
theorem
is_unit.strongly_measurable_const_smul_iff
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{M : Type u_5}
[topological_space β]
[monoid M]
[mul_action M β]
[has_continuous_const_smul M β]
{m : measurable_space α}
{c : M}
(hc : is_unit c) :
measure_theory.strongly_measurable (λ (x : α), c • f x) ↔ measure_theory.strongly_measurable f
theorem
strongly_measurable_const_smul_iff₀
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{G₀ : Type u_7}
[topological_space β]
[group_with_zero G₀]
[mul_action G₀ β]
[has_continuous_const_smul G₀ β]
{m : measurable_space α}
{c : G₀}
(hc : c ≠ 0) :
measure_theory.strongly_measurable (λ (x : α), c • f x) ↔ measure_theory.strongly_measurable f
@[protected]
theorem
measure_theory.strongly_measurable.sup
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
[measurable_space α]
[topological_space β]
[has_sup β]
[has_continuous_sup β]
(hf : measure_theory.strongly_measurable f)
(hg : measure_theory.strongly_measurable g) :
@[protected]
theorem
measure_theory.strongly_measurable.inf
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
[measurable_space α]
[topological_space β]
[has_inf β]
[has_continuous_inf β]
(hf : measure_theory.strongly_measurable f)
(hg : measure_theory.strongly_measurable g) :
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 ∈ l → measure_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 ∈ l → measure_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 ∈ l → measure_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 ∈ l → measure_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 ∈ l → measure_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 ∈ l → measure_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 ∈ s → measure_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 ∈ s → measure_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 ∈ s → measure_theory.strongly_measurable (f i)) :
measure_theory.strongly_measurable (s.sum (λ (i : ι), 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 ∈ s → measure_theory.strongly_measurable (f i)) :
measure_theory.strongly_measurable (s.prod (λ (i : ι), 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 ∈ s → measure_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 ∈ s → measure_theory.strongly_measurable (f i)) :
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 α}
[topological_space β]
(hf : measure_theory.strongly_measurable f) :
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 α}
[topological_space β]
[topological_space.pseudo_metrizable_space β]
(hf : measure_theory.strongly_measurable f)
{b : β} :
theorem
measurable.strongly_measurable
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{mα : measurable_space α}
[measurable_space β]
[topological_space β]
[topological_space.pseudo_metrizable_space β]
[topological_space.second_countable_topology β]
[opens_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 α}
[measurable_space β]
[topological_space β]
[topological_space.metrizable_space β]
[borel_space β]
[topological_space.second_countable_topology β] :
In a space with second countable topology, strongly measurable and measurable are equivalent.
theorem
strongly_measurable_id
{α : Type u_1}
{mα : measurable_space α}
[topological_space α]
[topological_space.pseudo_metrizable_space α]
[opens_measurable_space α]
[topological_space.second_countable_topology α] :
theorem
strongly_measurable_iff_measurable_separable
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{m : measurable_space α}
[topological_space β]
[topological_space.pseudo_metrizable_space β]
[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}
[measurable_space α]
[topological_space α]
[opens_measurable_space α]
{β : Type u_2}
[topological_space β]
[topological_space.pseudo_metrizable_space β]
[h : second_countable_topology_either α β]
{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 α}
[topological_space β]
[topological_space.pseudo_metrizable_space β]
[topological_space γ]
[topological_space.pseudo_metrizable_space γ]
{g : β → γ}
{f : α → β}
(hg : embedding g) :
measure_theory.strongly_measurable (λ (x : α), g (f x)) ↔ measure_theory.strongly_measurable f
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)) :
theorem
strongly_measurable_of_restrict_of_restrict_compl
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
[topological_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 α}
[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) :
measure_theory.strongly_measurable (λ (x : α), has_dist.dist (f x) (g x))
@[protected]
theorem
measure_theory.strongly_measurable.norm
{α : Type u_1}
{m : measurable_space α}
{β : Type u_2}
[seminormed_add_comm_group β]
{f : α → β}
(hf : measure_theory.strongly_measurable f) :
measure_theory.strongly_measurable (λ (x : α), ‖f x‖)
@[protected]
theorem
measure_theory.strongly_measurable.nnnorm
{α : Type u_1}
{m : measurable_space α}
{β : Type u_2}
[seminormed_add_comm_group β]
{f : α → β}
(hf : measure_theory.strongly_measurable f) :
measure_theory.strongly_measurable (λ (x : α), ‖f x‖₊)
@[protected]
theorem
measure_theory.strongly_measurable.ennnorm
{α : Type u_1}
{m : measurable_space α}
{β : Type u_2}
[seminormed_add_comm_group β]
{f : α → β}
(hf : measure_theory.strongly_measurable f) :
measurable (λ (a : α), ↑‖f a‖₊)
@[protected]
theorem
measure_theory.strongly_measurable.real_to_nnreal
{α : Type u_1}
{m : measurable_space α}
{f : α → ℝ}
(hf : measure_theory.strongly_measurable f) :
measure_theory.strongly_measurable (λ (x : α), (f x).to_nnreal)
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 β) :
theorem
measure_theory.strongly_measurable.measurable_set_eq_fun
{α : Type u_1}
{m : measurable_space α}
{E : Type u_2}
[topological_space E]
[topological_space.metrizable_space E]
{f g : α → E}
(hf : measure_theory.strongly_measurable f)
(hg : measure_theory.strongly_measurable g) :
measurable_set {x : α | f x = g x}
theorem
measure_theory.strongly_measurable.measurable_set_lt
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
[topological_space β]
[linear_order β]
[order_closed_topology β]
[topological_space.pseudo_metrizable_space β]
{f g : α → β}
(hf : measure_theory.strongly_measurable f)
(hg : measure_theory.strongly_measurable 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 α}
[topological_space β]
[preorder β]
[order_closed_topology β]
[topological_space.pseudo_metrizable_space β]
{f g : α → β}
(hf : measure_theory.strongly_measurable f)
(hg : measure_theory.strongly_measurable 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 α}
[topological_space β]
[has_zero β]
{s : set α}
{f : α → β}
(hs : measurable_set s)
(hf : measure_theory.strongly_measurable f)
(hf_zero : ∀ (x : α), x ∉ s → f 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 ∉ s → f 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.
theorem
measure_theory.strongly_measurable.exists_spanning_measurable_set_norm_le
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[seminormed_add_comm_group β]
{m m0 : measurable_space α}
(hm : m ≤ m0)
(hf : measure_theory.strongly_measurable f)
(μ : measure_theory.measure α)
[measure_theory.sigma_finite (μ.trim hm)] :
If a function f is strongly measurable w.r.t. a sub-σ-algebra m and the measure is σ-finite
on m, then there exists spanning measurable sets with finite measure on which f has bounded
norm. In particular, f is integrable on each of those sets.
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 β]
[topological_space β] :
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 β]
[topological_space β]
(hf : measure_theory.fin_strongly_measurable f μ) :
@[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
- hf.approx = Exists.some hf
@[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))
@[protected]
theorem
measure_theory.fin_strongly_measurable.strongly_measurable
{α : Type u_1}
{β : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : α → β}
[has_zero β]
[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}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : α → β}
[has_zero β]
[topological_space β]
[t2_space β]
(hf : measure_theory.fin_strongly_measurable f μ) :
@[protected]
theorem
measure_theory.fin_strongly_measurable.measurable
{α : Type u_1}
{β : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : α → β}
[has_zero β]
[topological_space β]
[topological_space.pseudo_metrizable_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.mul
{α : Type u_1}
{β : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → β}
[topological_space β]
[monoid_with_zero β]
[has_continuous_mul β]
(hf : measure_theory.fin_strongly_measurable f μ)
(hg : measure_theory.fin_strongly_measurable g μ) :
@[protected]
theorem
measure_theory.fin_strongly_measurable.add
{α : Type u_1}
{β : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → β}
[topological_space β]
[add_monoid β]
[has_continuous_add β]
(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}
{β : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : α → β}
[topological_space β]
[add_group β]
[topological_add_group β]
(hf : measure_theory.fin_strongly_measurable f μ) :
@[protected]
theorem
measure_theory.fin_strongly_measurable.sub
{α : Type u_1}
{β : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → β}
[topological_space β]
[add_group β]
[has_continuous_sub β]
(hf : measure_theory.fin_strongly_measurable f μ)
(hg : measure_theory.fin_strongly_measurable g μ) :
@[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 : 𝕜) :
@[protected]
theorem
measure_theory.fin_strongly_measurable.sup
{α : Type u_1}
{β : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → β}
[topological_space β]
[has_zero β]
[semilattice_sup β]
[has_continuous_sup β]
(hf : measure_theory.fin_strongly_measurable f μ)
(hg : measure_theory.fin_strongly_measurable g μ) :
@[protected]
theorem
measure_theory.fin_strongly_measurable.inf
{α : Type u_1}
{β : Type u_2}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → β}
[topological_space β]
[has_zero β]
[semilattice_inf β]
[has_continuous_inf β]
(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)
theorem
measure_theory.ae_fin_strongly_measurable_zero
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
(μ : measure_theory.measure α)
[has_zero β]
[topological_space β] :
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 : β} :
measure_theory.ae_strongly_measurable (λ (a : α), b) μ
theorem
measure_theory.ae_strongly_measurable_zero
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
[has_zero β] :
theorem
measure_theory.ae_strongly_measurable_one
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
[has_one β] :
@[simp]
theorem
measure_theory.subsingleton.ae_strongly_measurable
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
[topological_space β]
[subsingleton β]
{μ : measure_theory.measure α}
(f : α → β) :
@[simp]
theorem
measure_theory.subsingleton.ae_strongly_measurable'
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
[topological_space β]
[subsingleton α]
{μ : measure_theory.measure α}
(f : α → β) :
@[simp]
theorem
measure_theory.ae_strongly_measurable_zero_measure
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[topological_space β]
(f : α → β) :
theorem
measure_theory.simple_func.ae_strongly_measurable
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
(f : measure_theory.simple_func α β) :
@[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.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 μ) :
theorem
measure_theory.ae_strongly_measurable.measurable_mk
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
[topological_space.pseudo_metrizable_space β]
[measurable_space β]
[borel_space β]
(hf : measure_theory.ae_strongly_measurable f μ) :
theorem
measure_theory.ae_strongly_measurable.ae_eq_mk
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
(hf : measure_theory.ae_strongly_measurable f μ) :
@[protected]
theorem
measure_theory.ae_strongly_measurable.ae_measurable
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{β : Type u_2}
[measurable_space β]
[topological_space β]
[topological_space.pseudo_metrizable_space β]
[borel_space β]
{f : α → β}
(hf : measure_theory.ae_strongly_measurable f μ) :
ae_measurable f μ
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_measure
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
{ν : measure_theory.measure α}
(hf : measure_theory.ae_strongly_measurable f μ)
(h : ν ≤ μ) :
@[protected]
theorem
measure_theory.ae_strongly_measurable.mono'
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
{ν : measure_theory.measure α}
(h : measure_theory.ae_strongly_measurable f μ)
(h' : ν.absolutely_continuous μ) :
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.restrict
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
(hfm : measure_theory.ae_strongly_measurable f μ)
{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 α}
[topological_space β]
{f : α → β}
{s : set α}
(h : measure_theory.ae_strongly_measurable f (μ.restrict s)) :
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.
theorem
continuous.ae_strongly_measurable
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
[topological_space α]
[opens_measurable_space α]
[topological_space.pseudo_metrizable_space β]
[second_countable_topology_either α β]
(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 α}
[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)) μ
theorem
measurable.ae_strongly_measurable
{α : Type u_1}
{β : Type u_2}
[topological_space β]
{f : α → β}
{m : measurable_space α}
{μ : measure_theory.measure α}
[measurable_space β]
[topological_space.pseudo_metrizable_space β]
[topological_space.second_countable_topology β]
[opens_measurable_space β]
(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 α}
[topological_space β]
{f g : α → β}
[has_add β]
[has_continuous_add β]
(hf : measure_theory.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable g μ) :
@[protected]
theorem
measure_theory.ae_strongly_measurable.mul
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f g : α → β}
[has_mul β]
[has_continuous_mul β]
(hf : measure_theory.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable g μ) :
@[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 : β) :
measure_theory.ae_strongly_measurable (λ (x : α), f x + 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 : β) :
measure_theory.ae_strongly_measurable (λ (x : α), f x * 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 : β) :
measure_theory.ae_strongly_measurable (λ (x : α), c * f x) μ
@[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 : β) :
measure_theory.ae_strongly_measurable (λ (x : α), c + f x) μ
@[protected]
theorem
measure_theory.ae_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_strongly_measurable f μ) :
@[protected]
theorem
measure_theory.ae_strongly_measurable.inv
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
[group β]
[topological_group β]
(hf : measure_theory.ae_strongly_measurable f μ) :
@[protected]
theorem
measure_theory.ae_strongly_measurable.sub
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f g : α → β}
[add_group β]
[topological_add_group β]
(hf : measure_theory.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable g μ) :
@[protected]
theorem
measure_theory.ae_strongly_measurable.div
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f g : α → β}
[group β]
[topological_group β]
(hf : measure_theory.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable g μ) :
@[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_smul 𝕜 β]
[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 μ) :
measure_theory.ae_strongly_measurable (λ (x : α), f x +ᵥ g x) μ
@[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_smul 𝕜 β]
[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_smul 𝕜 β]
[has_continuous_const_smul 𝕜 β]
(hf : measure_theory.ae_strongly_measurable f μ)
(c : 𝕜) :
measure_theory.ae_strongly_measurable (λ (x : α), c • f x) μ
@[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 : β) :
measure_theory.ae_strongly_measurable (λ (x : α), f x +ᵥ 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_smul 𝕜 β]
[has_continuous_smul 𝕜 β]
{f : α → 𝕜}
(hf : measure_theory.ae_strongly_measurable f μ)
(c : β) :
measure_theory.ae_strongly_measurable (λ (x : α), f x • c) μ
@[protected]
theorem
measure_theory.ae_strongly_measurable.sup
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f g : α → β}
[semilattice_sup β]
[has_continuous_sup β]
(hf : measure_theory.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable g μ) :
@[protected]
theorem
measure_theory.ae_strongly_measurable.inf
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f g : α → β}
[semilattice_inf β]
[has_continuous_inf β]
(hf : measure_theory.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable 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]
[topological_space M]
[has_continuous_mul M]
(l : list (α → M))
(hl : ∀ (f : α → M), f ∈ l → measure_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 ∈ l → measure_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 ∈ l → measure_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 ∈ l → measure_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 ∈ l → measure_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 ∈ l → measure_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 ∈ s → measure_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 ∈ s → measure_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 ∈ s → measure_theory.ae_strongly_measurable (f i) μ) :
measure_theory.ae_strongly_measurable (s.prod (λ (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 ∈ s → measure_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 ∈ s → measure_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 ∈ s → measure_theory.ae_strongly_measurable (f i) μ) :
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 α}
[topological_space β]
{f : α → β}
[measurable_space β]
[topological_space.pseudo_metrizable_space β]
[opens_measurable_space β]
[topological_space.second_countable_topology β]
(hf : ae_measurable f μ) :
In a space with second countable topology, measurable implies strongly measurable.
theorem
ae_strongly_measurable_id
{α : Type u_1}
[topological_space α]
[topological_space.pseudo_metrizable_space α]
{m : measurable_space α}
[opens_measurable_space α]
[topological_space.second_countable_topology α]
{μ : measure_theory.measure α} :
theorem
ae_strongly_measurable_iff_ae_measurable
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
[measurable_space β]
[topological_space.pseudo_metrizable_space β]
[borel_space β]
[topological_space.second_countable_topology β] :
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}
[pseudo_metric_space β]
{f g : α → β}
(hf : measure_theory.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable g μ) :
measure_theory.ae_strongly_measurable (λ (x : α), has_dist.dist (f x) (g x)) μ
@[protected]
theorem
measure_theory.ae_strongly_measurable.norm
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{β : Type u_2}
[seminormed_add_comm_group β]
{f : α → β}
(hf : measure_theory.ae_strongly_measurable f μ) :
measure_theory.ae_strongly_measurable (λ (x : α), ‖f x‖) μ
@[protected]
theorem
measure_theory.ae_strongly_measurable.nnnorm
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{β : Type u_2}
[seminormed_add_comm_group β]
{f : α → β}
(hf : measure_theory.ae_strongly_measurable f μ) :
measure_theory.ae_strongly_measurable (λ (x : α), ‖f x‖₊) μ
@[protected]
theorem
measure_theory.ae_strongly_measurable.ennnorm
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{β : Type u_2}
[seminormed_add_comm_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}
[seminormed_add_comm_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.real_to_nnreal
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ}
(hf : measure_theory.ae_strongly_measurable f μ) :
measure_theory.ae_strongly_measurable (λ (x : α), (f x).to_nnreal) μ
theorem
ae_strongly_measurable_indicator_iff
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{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 α}
[topological_space β]
{f : α → β}
[has_zero β]
(hfm : measure_theory.ae_strongly_measurable f μ)
{s : set α}
(hs : measurable_set s) :
theorem
measure_theory.ae_strongly_measurable.null_measurable_set_eq_fun
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{E : Type u_2}
[topological_space E]
[topological_space.metrizable_space E]
{f g : α → E}
(hf : measure_theory.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable g μ) :
measure_theory.null_measurable_set {x : α | f x = g x} μ
theorem
measure_theory.ae_strongly_measurable.null_measurable_set_lt
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
[linear_order β]
[order_closed_topology β]
[topological_space.pseudo_metrizable_space β]
{f g : α → β}
(hf : measure_theory.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable g μ) :
measure_theory.null_measurable_set {a : α | f a < g a} μ
theorem
measure_theory.ae_strongly_measurable.null_measurable_set_le
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
[preorder β]
[order_closed_topology β]
[topological_space.pseudo_metrizable_space β]
{f g : α → β}
(hf : measure_theory.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable g μ) :
measure_theory.null_measurable_set {a : α | f a ≤ g a} μ
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_quasi_measure_preserving
{α : 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 : measure_theory.measure.quasi_measure_preserving f μ ν) :
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 μ) :
theorem
ae_strongly_measurable_iff_ae_measurable_separable
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
[topological_space.pseudo_metrizable_space β]
[measurable_space β]
[borel_space β] :
measure_theory.ae_strongly_measurable f μ ↔ ae_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
measurable_embedding.ae_strongly_measurable_map_iff
{α : Type u_1}
{β : Type u_2}
[topological_space β]
{γ : 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 α}
[topological_space β]
[topological_space γ]
[topological_space.pseudo_metrizable_space β]
[topological_space.pseudo_metrizable_space γ]
{g : β → γ}
{f : α → β}
(hg : embedding g) :
measure_theory.ae_strongly_measurable (λ (x : α), g (f x)) μ ↔ measure_theory.ae_strongly_measurable f μ
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.
theorem
measure_theory.ae_strongly_measurable.sum_measure
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[countable ι]
[topological_space β]
{f : α → β}
[topological_space.pseudo_metrizable_space β]
{m : measurable_space α}
{μ : ι → measure_theory.measure α}
(h : ∀ (i : ι), measure_theory.ae_strongly_measurable f (μ i)) :
@[simp]
theorem
ae_strongly_measurable_sum_measure_iff
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[countable ι]
[topological_space β]
{f : α → β}
[topological_space.pseudo_metrizable_space β]
{m : measurable_space α}
{μ : ι → measure_theory.measure α} :
measure_theory.ae_strongly_measurable f (measure_theory.measure.sum μ) ↔ ∀ (i : ι), measure_theory.ae_strongly_measurable f (μ i)
@[simp]
theorem
ae_strongly_measurable_add_measure_iff
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
[topological_space.pseudo_metrizable_space β]
{ν : measure_theory.measure α} :
theorem
measure_theory.ae_strongly_measurable.add_measure
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
[topological_space.pseudo_metrizable_space β]
{ν : measure_theory.measure α}
{f : α → β}
(hμ : measure_theory.ae_strongly_measurable f μ)
(hν : measure_theory.ae_strongly_measurable f ν) :
@[protected]
theorem
measure_theory.ae_strongly_measurable.Union
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[countable ι]
{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))) :
measure_theory.ae_strongly_measurable f (μ.restrict (⋃ (i : ι), s i))
@[simp]
theorem
ae_strongly_measurable_Union_iff
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[countable ι]
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
[topological_space.pseudo_metrizable_space β]
{s : ι → set α} :
measure_theory.ae_strongly_measurable f (μ.restrict (⋃ (i : ι), s i)) ↔ ∀ (i : ι), measure_theory.ae_strongly_measurable f (μ.restrict (s i))
@[simp]
theorem
ae_strongly_measurable_union_iff
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
[topological_space.pseudo_metrizable_space β]
{s t : set α} :
measure_theory.ae_strongly_measurable f (μ.restrict (s ∪ t)) ↔ measure_theory.ae_strongly_measurable f (μ.restrict s) ∧ measure_theory.ae_strongly_measurable f (μ.restrict t)
theorem
measure_theory.ae_strongly_measurable.ae_strongly_measurable_uIoc_iff
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
[linear_order α]
[topological_space.pseudo_metrizable_space β]
{f : α → β}
{a b : α} :
measure_theory.ae_strongly_measurable f (μ.restrict (set.uIoc a b)) ↔ measure_theory.ae_strongly_measurable f (μ.restrict (set.Ioc a b)) ∧ measure_theory.ae_strongly_measurable f (μ.restrict (set.Ioc b a))
theorem
measure_theory.ae_strongly_measurable.smul_measure
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
{R : Type u_3}
[monoid R]
[distrib_mul_action R ennreal]
[is_scalar_tower R ennreal ennreal]
(h : measure_theory.ae_strongly_measurable f μ)
(c : R) :
theorem
ae_strongly_measurable_smul_const_iff
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{𝕜 : Type u_5}
[nontrivially_normed_field 𝕜]
[complete_space 𝕜]
{E : Type u_6}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{f : α → 𝕜}
{c : E}
(hc : c ≠ 0) :
measure_theory.ae_strongly_measurable (λ (x : α), f x • c) μ ↔ measure_theory.ae_strongly_measurable f μ
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 G]
[mul_action G β]
[has_continuous_const_smul G β]
(c : G) :
measure_theory.ae_strongly_measurable (λ (x : α), c • f x) μ ↔ measure_theory.ae_strongly_measurable f μ
theorem
is_unit.ae_strongly_measurable_const_smul_iff
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
{M : Type u_5}
[monoid M]
[mul_action M β]
[has_continuous_const_smul M β]
{c : M}
(hc : is_unit c) :
measure_theory.ae_strongly_measurable (λ (x : α), c • f x) μ ↔ measure_theory.ae_strongly_measurable f μ
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_7}
[group_with_zero G₀]
[mul_action G₀ β]
[has_continuous_const_smul G₀ β]
{c : G₀}
(hc : c ≠ 0) :
measure_theory.ae_strongly_measurable (λ (x : α), c • f x) μ ↔ measure_theory.ae_strongly_measurable f μ
theorem
strongly_measurable.apply_continuous_linear_map
{α : Type u_1}
{𝕜 : Type u_5}
[nontrivially_normed_field 𝕜]
{E : Type u_6}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_7}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m : measurable_space α}
{φ : α → (F →L[𝕜] E)}
(hφ : measure_theory.strongly_measurable φ)
(v : F) :
measure_theory.strongly_measurable (λ (a : α), ⇑(φ a) v)
theorem
measure_theory.ae_strongly_measurable.apply_continuous_linear_map
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{𝕜 : Type u_5}
[nontrivially_normed_field 𝕜]
{E : Type u_6}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_7}
[normed_add_comm_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}
[nontrivially_normed_field 𝕜]
{E : Type u_6}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_7}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_8}
[normed_add_comm_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_add_comm_group E]
[normed_space ℝ E]
{f : α → nnreal}
(hf : measurable f)
{g : α → E} :
measure_theory.ae_strongly_measurable g (μ.with_density (λ (x : α), ↑(f x))) ↔ measure_theory.ae_strongly_measurable (λ (x : α), ↑(f x) • g x) μ
theorem
measure_theory.ae_strongly_measurable_of_absolutely_continuous
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[topological_space β]
{μ ν : measure_theory.measure α}
(h : ν.absolutely_continuous μ)
(g : α → β)
(hμ : measure_theory.ae_strongly_measurable g μ) :
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
theorem
measure_theory.ae_fin_strongly_measurable.fin_strongly_measurable_mk
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
[has_zero β]
(hf : measure_theory.ae_fin_strongly_measurable f μ) :
theorem
measure_theory.ae_fin_strongly_measurable.ae_eq_mk
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
[has_zero β]
(hf : measure_theory.ae_fin_strongly_measurable f μ) :
@[protected]
theorem
measure_theory.ae_fin_strongly_measurable.ae_measurable
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{β : Type u_2}
[has_zero β]
[measurable_space β]
[topological_space β]
[topological_space.pseudo_metrizable_space β]
[borel_space β]
{f : α → β}
(hf : measure_theory.ae_fin_strongly_measurable f μ) :
ae_measurable f μ
@[protected]
theorem
measure_theory.ae_fin_strongly_measurable.mul
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f g : α → β}
[monoid_with_zero β]
[has_continuous_mul β]
(hf : measure_theory.ae_fin_strongly_measurable f μ)
(hg : measure_theory.ae_fin_strongly_measurable g μ) :
@[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 μ) :
@[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 : 𝕜) :
@[protected]
theorem
measure_theory.ae_fin_strongly_measurable.sup
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f g : α → β}
[has_zero β]
[semilattice_sup β]
[has_continuous_sup β]
(hf : measure_theory.ae_fin_strongly_measurable f μ)
(hg : measure_theory.ae_fin_strongly_measurable g μ) :
@[protected]
theorem
measure_theory.ae_fin_strongly_measurable.inf
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f g : α → β}
[has_zero β]
[semilattice_inf β]
[has_continuous_inf β]
(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 μ) :
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_5}
[seminormed_add_comm_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_5}
[seminormed_add_comm_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.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)) :
theorem
measure_theory.strongly_measurable_uncurry_of_continuous_of_strongly_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 ι]
[topological_space β]
[topological_space.pseudo_metrizable_space β]
[measurable_space α]
{u : ι → α → β}
(hu_cont : ∀ (x : α), continuous (λ (i : ι), u i x))
(h : ∀ (i : ι), measure_theory.strongly_measurable (u i)) :