# mathlibdocumentation

measure_theory.constructions.borel_space

# Borel (measurable) space #

## Main definitions #

• `borel α` : the least `σ`-algebra that contains all open sets;
• `class borel_space` : a space with `topological_space` and `measurable_space` structures such that `‹measurable_space α› = borel α`;
• `class opens_measurable_space` : a space with `topological_space` and `measurable_space` structures such that all open sets are measurable; equivalently, `borel α ≤ ‹measurable_space α›`.
• `borel_space` instances on `empty`, `unit`, `bool`, `nat`, `int`, `rat`;
• `measurable` and `borel_space` instances on `ℝ`, `ℝ≥0`, `ℝ≥0∞`.

## Main statements #

• `is_open.measurable_set`, `is_closed.measurable_set`: open and closed sets are measurable;
• `continuous.measurable` : a continuous function is measurable;
• `continuous.measurable2` : if `f : α → β` and `g : α → γ` are measurable and `op : β × γ → δ` is continuous, then `λ x, op (f x, g y)` is measurable;
• `measurable.add` etc : dot notation for arithmetic operations on `measurable` predicates, and similarly for `dist` and `edist`;
• `ae_measurable.add` : similar dot notation for almost everywhere measurable functions;
• `measurable.ennreal*` : special cases for arithmetic operations on `ℝ≥0∞`.
def borel (α : Type u)  :

`measurable_space` structure generated by `topological_space`.

Equations
theorem borel_eq_top_of_discrete {α : Type u_1}  :
theorem borel_eq_top_of_countable {α : Type u_1} [t1_space α] [countable α] :
theorem borel_eq_generate_from_of_subbasis {α : Type u_1} {s : set (set α)} [t : topological_space α] (hs : t = ) :
theorem is_pi_system_is_open {α : Type u_1}  :
theorem borel_eq_generate_from_Iio (α : Type u_1) [linear_order α]  :
theorem borel_eq_generate_from_Ioi (α : Type u_1) [linear_order α]  :
theorem borel_comap {α : Type u_1} {β : Type u_2} {f : α β} {t : topological_space β} :
=
theorem continuous.borel_measurable {α : Type u_1} {β : Type u_2} {f : α β} (hf : continuous f) :
@[class]
structure opens_measurable_space (α : Type u_6) [h : measurable_space α] :
Prop
• borel_le : h

A space with `measurable_space` and `topological_space` structures such that all open sets are measurable.

Instances of this typeclass
@[class]
structure borel_space (α : Type u_6)  :
Prop
• measurable_eq : _inst_2 =

A space with `measurable_space` and `topological_space` structures such that the `σ`-algebra of measurable sets is exactly the `σ`-algebra generated by open sets.

Instances of this typeclass
meta def tactic.add_borel_instance (α : expr) :

Add instances `borel α : measurable_space α` and `⟨rfl⟩ : borel_space α`.

meta def tactic.borel_to_refl (α i : expr) :

Given a type `α`, an assumption `i : measurable_space α`, and an instance `[borel_space α]`, replace `i` with `borel α`.

meta def tactic.borelize (α : expr) :

Given a type `α`, if there is an assumption `[i : measurable_space α]`, then try to prove `[borel_space α]` and replace `i` with `borel α`. Otherwise, add instances `borel α : measurable_space α` and `⟨rfl⟩ : borel_space α`.

The behaviour of `borelize α` depends on the existing assumptions on `α`.

• if `α` is a topological space with instances `[measurable_space α] [borel_space α]`, then `borelize α` replaces the former instance by `borel α`;
• otherwise, `borelize α` adds instances `borel α : measurable_space α` and `⟨rfl⟩ : borel_space α`.

Finally, `borelize [α, β, γ]` runs `borelize α, borelize β, borelize γ`.

The behaviour of `borelize α` depends on the existing assumptions on `α`.

• if `α` is a topological space with instances `[measurable_space α] [borel_space α]`, then `borelize α` replaces the former instance by `borel α`;
• otherwise, `borelize α` adds instances `borel α : measurable_space α` and `⟨rfl⟩ : borel_space α`.

Finally, `borelize [α, β, γ]` runs `borelize α, borelize β, borelize γ`.

@[protected, instance]
@[protected, instance]
def order_dual.borel_space {α : Type u_1} [h : borel_space α] :
@[protected, instance]

In a `borel_space` all open sets are measurable.

@[protected, instance]
def subtype.borel_space {α : Type u_1} [hα : borel_space α] (s : set α) :
@[protected, instance]
def subtype.opens_measurable_space {α : Type u_1} [h : opens_measurable_space α] (s : set α) :
theorem measurable_set.induction_on_open {α : Type u_1} [borel_space α] {C : set α Prop} (h_open : (U : set α), C U) (h_compl : (t : set α), C t C t) (h_union : (f : set α), pairwise (disjoint on f) ( (i : ), measurable_set (f i)) ( (i : ), C (f i)) C ( (i : ), f i)) ⦃t : set α⦄ :
C t
theorem is_open.measurable_set {α : Type u_1} {s : set α} (h : is_open s) :
@[measurability]
theorem measurable_set_interior {α : Type u_1} {s : set α}  :
theorem is_Gδ.measurable_set {α : Type u_1} {s : set α} (h : is_Gδ s) :
theorem measurable_set_of_continuous_at {α : Type u_1} {β : Type u_2} (f : α β) :
measurable_set {x : α | x}
theorem is_closed.measurable_set {α : Type u_1} {s : set α} (h : is_closed s) :
theorem is_compact.measurable_set {α : Type u_1} {s : set α} [t2_space α] (h : is_compact s) :
@[measurability]
theorem measurable_set_closure {α : Type u_1} {s : set α}  :
theorem measurable_of_is_open {γ : Type u_3} {δ : Type u_5} [borel_space γ] {f : δ γ} (hf : (s : set γ), measurable_set (f ⁻¹' s)) :
theorem measurable_of_is_closed {γ : Type u_3} {δ : Type u_5} [borel_space γ] {f : δ γ} (hf : (s : set γ), measurable_set (f ⁻¹' s)) :
theorem measurable_of_is_closed' {γ : Type u_3} {δ : Type u_5} [borel_space γ] {f : δ γ} (hf : (s : set γ), s.nonempty measurable_set (f ⁻¹' s)) :
@[protected, instance]
def nhds_is_measurably_generated {α : Type u_1} (a : α) :
theorem measurable_set.nhds_within_is_measurably_generated {α : Type u_1} {s : set α} (hs : measurable_set s) (a : α) :

If `s` is a measurable set, then `𝓝[s] a` is a measurably generated filter for each `a`. This cannot be an `instance` because it depends on a non-instance `hs : measurable_set s`.

@[protected, instance]
@[protected, instance]
def pi.opens_measurable_space {ι : Type u_1} {π : ι Type u_2} [countable ι] [t' : Π (i : ι), topological_space (π i)] [Π (i : ι), measurable_space (π i)] [ (i : ι), ] [ (i : ι), ] :
opens_measurable_space (Π (i : ι), π i)
@[protected, instance]
theorem interior_ae_eq_of_null_frontier {α' : Type u_6} [measurable_space α'] {μ : measure_theory.measure α'} {s : set α'} (h : μ (frontier s) = 0) :
=ᵐ[μ] s
theorem measure_interior_of_null_frontier {α' : Type u_6} [measurable_space α'] {μ : measure_theory.measure α'} {s : set α'} (h : μ (frontier s) = 0) :
μ (interior s) = μ s
theorem null_measurable_set_of_null_frontier {α : Type u_1} {s : set α} {μ : measure_theory.measure α} (h : μ (frontier s) = 0) :
theorem closure_ae_eq_of_null_frontier {α' : Type u_6} [measurable_space α'] {μ : measure_theory.measure α'} {s : set α'} (h : μ (frontier s) = 0) :
=ᵐ[μ] s
theorem measure_closure_of_null_frontier {α' : Type u_6} [measurable_space α'] {μ : measure_theory.measure α'} {s : set α'} (h : μ (frontier s) = 0) :
μ (closure s) = μ s
@[simp, measurability]
theorem measurable_set_Ici {α : Type u_1} [preorder α] {a : α} :
@[simp, measurability]
theorem measurable_set_Iic {α : Type u_1} [preorder α] {a : α} :
@[simp, measurability]
theorem measurable_set_Icc {α : Type u_1} [preorder α] {a b : α} :
@[protected, instance]
def nhds_within_Ici_is_measurably_generated {α : Type u_1} [preorder α] {a b : α} :
@[protected, instance]
def nhds_within_Iic_is_measurably_generated {α : Type u_1} [preorder α] {a b : α} :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[measurability]
theorem measurable_set_le' {α : Type u_1}  :
measurable_set {p : α × α | p.fst p.snd}
@[measurability]
theorem measurable_set_le {α : Type u_1} {δ : Type u_5} {f g : δ α} (hf : measurable f) (hg : measurable g) :
measurable_set {a : δ | f a g a}
@[simp, measurability]
theorem measurable_set_Iio {α : Type u_1} [linear_order α] {a : α} :
@[simp, measurability]
theorem measurable_set_Ioi {α : Type u_1} [linear_order α] {a : α} :
@[simp, measurability]
theorem measurable_set_Ioo {α : Type u_1} [linear_order α] {a b : α} :
@[simp, measurability]
theorem measurable_set_Ioc {α : Type u_1} [linear_order α] {a b : α} :
@[simp, measurability]
theorem measurable_set_Ico {α : Type u_1} [linear_order α] {a b : α} :
@[protected, instance]
def nhds_within_Ioi_is_measurably_generated {α : Type u_1} [linear_order α] {a b : α} :
@[protected, instance]
def nhds_within_Iio_is_measurably_generated {α : Type u_1} [linear_order α] {a b : α} :
@[protected, instance]
@[measurability]
theorem measurable_set_lt' {α : Type u_1} [linear_order α]  :
measurable_set {p : α × α | p.fst < p.snd}
@[measurability]
theorem measurable_set_lt {α : Type u_1} {δ : Type u_5} [linear_order α] {f g : δ α} (hf : measurable f) (hg : measurable g) :
measurable_set {a : δ | f a < g a}
theorem null_measurable_set_lt {α : Type u_1} {δ : Type u_5} [linear_order α] {μ : measure_theory.measure δ} {f g : δ α} (hf : μ) (hg : μ) :
theorem set.ord_connected.measurable_set {α : Type u_1} {s : set α} [linear_order α] (h : s.ord_connected) :
theorem is_preconnected.measurable_set {α : Type u_1} {s : set α} [linear_order α] (h : is_preconnected s) :
theorem generate_from_Ico_mem_le_borel {α : Type u_1} [linear_order α] (s t : set α) :
measurable_space.generate_from {S : set α | (l : α) (H : l s) (u : α) (H : u t) (h : l < u), u = S}
theorem dense.borel_eq_generate_from_Ico_mem_aux {α : Type u_1} [linear_order α] {s : set α} (hd : dense s) (hbot : (x : α), x s) (hIoo : (x y : α), x < y y = y s) :
= measurable_space.generate_from {S : set α | (l : α) (H : l s) (u : α) (H : u s) (h : l < u), u = S}
theorem dense.borel_eq_generate_from_Ico_mem {α : Type u_1} [linear_order α] [no_min_order α] {s : set α} (hd : dense s) :
= measurable_space.generate_from {S : set α | (l : α) (H : l s) (u : α) (H : u s) (h : l < u), u = S}
theorem borel_eq_generate_from_Ico (α : Type u_1) [linear_order α]  :
= measurable_space.generate_from {S : set α | (l u : α) (h : l < u), u = S}
theorem dense.borel_eq_generate_from_Ioc_mem_aux {α : Type u_1} [linear_order α] {s : set α} (hd : dense s) (hbot : (x : α), x s) (hIoo : (x y : α), x < y y = x s) :
= measurable_space.generate_from {S : set α | (l : α) (H : l s) (u : α) (H : u s) (h : l < u), u = S}
theorem dense.borel_eq_generate_from_Ioc_mem {α : Type u_1} [linear_order α] [no_max_order α] {s : set α} (hd : dense s) :
= measurable_space.generate_from {S : set α | (l : α) (H : l s) (u : α) (H : u s) (h : l < u), u = S}
theorem borel_eq_generate_from_Ioc (α : Type u_1) [linear_order α]  :
= measurable_space.generate_from {S : set α | (l u : α) (h : l < u), u = S}
theorem measure_theory.measure.ext_of_Ico_finite {α : Type u_1} {m : measurable_space α} [linear_order α] [borel_space α] (μ ν : measure_theory.measure α) (hμν : = ) (h : ⦃a b : α⦄, a < b μ (set.Ico a b) = ν (set.Ico a b)) :
μ = ν

Two finite measures on a Borel space are equal if they agree on all closed-open intervals. If `α` is a conditionally complete linear order with no top element, `measure_theory.measure..ext_of_Ico` is an extensionality lemma with weaker assumptions on `μ` and `ν`.

theorem measure_theory.measure.ext_of_Ioc_finite {α : Type u_1} {m : measurable_space α} [linear_order α] [borel_space α] (μ ν : measure_theory.measure α) (hμν : = ) (h : ⦃a b : α⦄, a < b μ (set.Ioc a b) = ν (set.Ioc a b)) :
μ = ν

Two finite measures on a Borel space are equal if they agree on all open-closed intervals. If `α` is a conditionally complete linear order with no top element, `measure_theory.measure..ext_of_Ioc` is an extensionality lemma with weaker assumptions on `μ` and `ν`.

theorem measure_theory.measure.ext_of_Ico' {α : Type u_1} {m : measurable_space α} [linear_order α] [borel_space α] [no_max_order α] (μ ν : measure_theory.measure α) (hμ : ⦃a b : α⦄, a < b μ (set.Ico a b) ) (h : ⦃a b : α⦄, a < b μ (set.Ico a b) = ν (set.Ico a b)) :
μ = ν

Two measures which are finite on closed-open intervals are equal if the agree on all closed-open intervals.

theorem measure_theory.measure.ext_of_Ioc' {α : Type u_1} {m : measurable_space α} [linear_order α] [borel_space α] [no_min_order α] (μ ν : measure_theory.measure α) (hμ : ⦃a b : α⦄, a < b μ (set.Ioc a b) ) (h : ⦃a b : α⦄, a < b μ (set.Ioc a b) = ν (set.Ioc a b)) :
μ = ν

Two measures which are finite on closed-open intervals are equal if the agree on all open-closed intervals.

theorem measure_theory.measure.ext_of_Ico {α : Type u_1} {m : measurable_space α} [borel_space α] [no_max_order α] (μ ν : measure_theory.measure α) (h : ⦃a b : α⦄, a < b μ (set.Ico a b) = ν (set.Ico a b)) :
μ = ν

Two measures which are finite on closed-open intervals are equal if the agree on all closed-open intervals.

theorem measure_theory.measure.ext_of_Ioc {α : Type u_1} {m : measurable_space α} [borel_space α] [no_min_order α] (μ ν : measure_theory.measure α) (h : ⦃a b : α⦄, a < b μ (set.Ioc a b) = ν (set.Ioc a b)) :
μ = ν

Two measures which are finite on closed-open intervals are equal if the agree on all open-closed intervals.

theorem measure_theory.measure.ext_of_Iic {α : Type u_1} {m : measurable_space α} [linear_order α] [borel_space α] (μ ν : measure_theory.measure α) (h : (a : α), μ (set.Iic a) = ν (set.Iic a)) :
μ = ν

Two finite measures on a Borel space are equal if they agree on all left-infinite right-closed intervals.

theorem measure_theory.measure.ext_of_Ici {α : Type u_1} {m : measurable_space α} [linear_order α] [borel_space α] (μ ν : measure_theory.measure α) (h : (a : α), μ (set.Ici a) = ν (set.Ici a)) :
μ = ν

Two finite measures on a Borel space are equal if they agree on all left-closed right-infinite intervals.

@[measurability]
theorem measurable_set_uIcc {α : Type u_1} [linear_order α] {a b : α} :
@[measurability]
theorem measurable_set_uIoc {α : Type u_1} [linear_order α] {a b : α} :
@[measurability]
theorem measurable.max {α : Type u_1} {δ : Type u_5} [linear_order α] {f g : δ α} (hf : measurable f) (hg : measurable g) :
measurable (λ (a : δ), linear_order.max (f a) (g a))
@[measurability]
theorem ae_measurable.max {α : Type u_1} {δ : Type u_5} [linear_order α] {f g : δ α} {μ : measure_theory.measure δ} (hf : μ) (hg : μ) :
ae_measurable (λ (a : δ), linear_order.max (f a) (g a)) μ
@[measurability]
theorem measurable.min {α : Type u_1} {δ : Type u_5} [linear_order α] {f g : δ α} (hf : measurable f) (hg : measurable g) :
measurable (λ (a : δ), linear_order.min (f a) (g a))
@[measurability]
theorem ae_measurable.min {α : Type u_1} {δ : Type u_5} [linear_order α] {f g : δ α} {μ : measure_theory.measure δ} (hf : μ) (hg : μ) :
ae_measurable (λ (a : δ), linear_order.min (f a) (g a)) μ
theorem continuous.measurable {α : Type u_1} {γ : Type u_3} [borel_space γ] {f : α γ} (hf : continuous f) :

A continuous function from an `opens_measurable_space` to a `borel_space` is measurable.

theorem continuous.ae_measurable {α : Type u_1} {γ : Type u_3} [borel_space γ] {f : α γ} (h : continuous f) {μ : measure_theory.measure α} :

A continuous function from an `opens_measurable_space` to a `borel_space` is ae-measurable.

theorem closed_embedding.measurable {α : Type u_1} {γ : Type u_3} [borel_space γ] {f : α γ} (hf : closed_embedding f) :
theorem continuous.is_open_pos_measure_map {β : Type u_2} {γ : Type u_3} [borel_space γ] {f : β γ} (hf : continuous f) (hf_surj : function.surjective f) {μ : measure_theory.measure β}  :
theorem continuous_on.measurable_piecewise {α : Type u_1} {γ : Type u_3} [borel_space γ] {f g : α γ} {s : set α} [Π (j : α), decidable (j s)] (hf : s) (hg : s) (hs : measurable_set s) :

If a function is defined piecewise in terms of functions which are continuous on their respective pieces, then it is measurable.

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def has_continuous_smul.has_measurable_smul {M : Type u_1} {α : Type u_2} [borel_space α] [ α] [ α] :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, measurability]
theorem homeomorph.measurable {α : Type u_1} {γ : Type u_3} [borel_space γ] (h : α ≃ₜ γ) :
def homeomorph.to_measurable_equiv {γ : Type u_3} {γ₂ : Type u_4} [borel_space γ] [measurable_space γ₂] [borel_space γ₂] (h : γ ≃ₜ γ₂) :
γ ≃ᵐ γ₂

A homeomorphism between two Borel spaces is a measurable equivalence.

Equations
@[simp]
theorem homeomorph.to_measurable_equiv_coe {γ : Type u_3} {γ₂ : Type u_4} [borel_space γ] [measurable_space γ₂] [borel_space γ₂] (h : γ ≃ₜ γ₂) :
@[simp]
theorem homeomorph.to_measurable_equiv_symm_coe {γ : Type u_3} {γ₂ : Type u_4} [borel_space γ] [measurable_space γ₂] [borel_space γ₂] (h : γ ≃ₜ γ₂) :
@[measurability]
theorem continuous_map.measurable {α : Type u_1} {γ : Type u_3} [borel_space γ] (f : C(α, γ)) :
theorem measurable_of_continuous_on_compl_singleton {α : Type u_1} {γ : Type u_3} [borel_space γ] [t1_space α] {f : α γ} (a : α) (hf : {a}) :
theorem continuous.measurable2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_5} [borel_space γ] {f : δ α} {g : δ β} {c : α β γ} (h : continuous (λ (p : α × β), c p.fst p.snd)) (hf : measurable f) (hg : measurable g) :
measurable (λ (a : δ), c (f a) (g a))
theorem continuous.ae_measurable2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_5} [borel_space γ] {f : δ α} {g : δ β} {c : α β γ} {μ : measure_theory.measure δ} (h : continuous (λ (p : α × β), c p.fst p.snd)) (hf : μ) (hg : μ) :
ae_measurable (λ (a : δ), c (f a) (g a)) μ
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def has_continuous_smul.has_measurable_smul₂ {M : Type u_1} {α : Type u_2} [borel_space α] [ α] [ α] :
theorem pi_le_borel_pi {ι : Type u_1} {π : ι Type u_2} [Π (i : ι), topological_space (π i)] [Π (i : ι), measurable_space (π i)] [ (i : ι), borel_space (π i)] :
measurable_space.pi borel (Π (i : ι), π i)
theorem prod_le_borel_prod {α : Type u_1} {β : Type u_2} [borel_space α] [borel_space β] :
@[protected, instance]
def pi.borel_space {ι : Type u_1} {π : ι Type u_2} [countable ι] [Π (i : ι), topological_space (π i)] [Π (i : ι), measurable_space (π i)] [ (i : ι), ] [ (i : ι), borel_space (π i)] :
borel_space (Π (i : ι), π i)
@[protected, instance]
def prod.borel_space {α : Type u_1} {β : Type u_2} [borel_space α] [borel_space β]  :
borel_space × β)
@[protected]
theorem embedding.measurable_embedding {α : Type u_1} {β : Type u_2} [borel_space α] [borel_space β] {f : α β} (h₁ : embedding f) (h₂ : measurable_set (set.range f)) :
@[protected]
theorem closed_embedding.measurable_embedding {α : Type u_1} {β : Type u_2} [borel_space α] [borel_space β] {f : α β} (h : closed_embedding f) :
@[protected]
theorem open_embedding.measurable_embedding {α : Type u_1} {β : Type u_2} [borel_space α] [borel_space β] {f : α β} (h : open_embedding f) :
theorem measurable_of_Iio {α : Type u_1} {δ : Type u_5} [borel_space α] [linear_order α] {f : δ α} (hf : (x : α), measurable_set (f ⁻¹' set.Iio x)) :
theorem upper_semicontinuous.measurable {α : Type u_1} {δ : Type u_5} [borel_space α] [linear_order α] {f : δ α} (hf : upper_semicontinuous f) :
theorem measurable_of_Ioi {α : Type u_1} {δ : Type u_5} [borel_space α] [linear_order α] {f : δ α} (hf : (x : α), measurable_set (f ⁻¹' set.Ioi x)) :
theorem lower_semicontinuous.measurable {α : Type u_1} {δ : Type u_5} [borel_space α] [linear_order α] {f : δ α} (hf : lower_semicontinuous f) :
theorem measurable_of_Iic {α : Type u_1} {δ : Type u_5} [borel_space α] [linear_order α] {f : δ α} (hf : (x : α), measurable_set (f ⁻¹' set.Iic x)) :
theorem measurable_of_Ici {α : Type u_1} {δ : Type u_5} [borel_space α] [linear_order α] {f : δ α} (hf : (x : α), measurable_set (f ⁻¹' set.Ici x)) :
theorem measurable.is_lub {α : Type u_1} {δ : Type u_5} [borel_space α] [linear_order α] {ι : Sort u_2} [countable ι] {f : ι δ α} {g : δ α} (hf : (i : ι), measurable (f i)) (hg : (b : δ), is_lub {a : α | (i : ι), f i b = a} (g b)) :
theorem ae_measurable.is_lub {α : Type u_1} {δ : Type u_5} [borel_space α] [linear_order α] {ι : Sort u_2} {μ : measure_theory.measure δ} [countable ι] {f : ι δ α} {g : δ α} (hf : (i : ι), ae_measurable (f i) μ) (hg : ∀ᵐ (b : δ) μ, is_lub {a : α | (i : ι), f i b = a} (g b)) :
theorem measurable.is_glb {α : Type u_1} {δ : Type u_5} [borel_space α] [linear_order α] {ι : Sort u_2} [countable ι] {f : ι δ α} {g : δ α} (hf : (i : ι), measurable (f i)) (hg : (b : δ), is_glb {a : α | (i : ι), f i b = a} (g b)) :
theorem ae_measurable.is_glb {α : Type u_1} {δ : Type u_5} [borel_space α] [linear_order α] {ι : Sort u_2} {μ : measure_theory.measure δ} [countable ι] {f : ι δ α} {g : δ α} (hf : (i : ι), ae_measurable (f i) μ) (hg : ∀ᵐ (b : δ) μ, is_glb {a : α | (i : ι), f i b = a} (g b)) :
@[protected]
theorem monotone.measurable {α : Type u_1} {β : Type u_2} [borel_space α] [borel_space β] [linear_order α] [linear_order β] {f : β α} (hf : monotone f) :
theorem ae_measurable_restrict_of_monotone_on {α : Type u_1} {β : Type u_2} [borel_space α] [borel_space β] [linear_order α] [linear_order β] {μ : measure_theory.measure β} {s : set β} (hs : measurable_set s) {f : β α} (hf : s) :
(μ.restrict s)
@[protected]
theorem antitone.measurable {α : Type u_1} {β : Type u_2} [borel_space α] [borel_space β] [linear_order α] [linear_order β] {f : β α} (hf : antitone f) :
theorem ae_measurable_restrict_of_antitone_on {α : Type u_1} {β : Type u_2} [borel_space α] [borel_space β] [linear_order α] [linear_order β] {μ : measure_theory.measure β} {s : set β} (hs : measurable_set s) {f : β α} (hf : s) :
(μ.restrict s)
theorem measurable_set_of_mem_nhds_within_Ioi_aux {α : Type u_1} [borel_space α] [linear_order α] {s : set α} (h : (x : α), x s s (set.Ioi x)) (h' : (x : α), x s ( (y : α), x < y)) :
theorem measurable_set_of_mem_nhds_within_Ioi {α : Type u_1} [borel_space α] [linear_order α] {s : set α} (h : (x : α), x s s (set.Ioi x)) :

If a set is a right-neighborhood of all of its points, then it is measurable.

@[measurability]
theorem measurable.supr_Prop {δ : Type u_5} {α : Type u_1} (p : Prop) {f : δ α} (hf : measurable f) :
measurable (λ (b : δ), (h : p), f b)
@[measurability]
theorem measurable.infi_Prop {δ : Type u_5} {α : Type u_1} (p : Prop) {f : δ α} (hf : measurable f) :
measurable (λ (b : δ), (h : p), f b)
@[measurability]
theorem measurable_supr {α : Type u_1} {δ : Type u_5} [borel_space α] {ι : Sort u_2} [countable ι] {f : ι δ α} (hf : (i : ι), measurable (f i)) :
measurable (λ (b : δ), (i : ι), f i b)
@[measurability]
theorem ae_measurable_supr {α : Type u_1} {δ : Type u_5} [borel_space α] {ι : Sort u_2} {μ : measure_theory.measure δ} [countable ι] {f : ι δ α} (hf : (i : ι), ae_measurable (f i) μ) :
ae_measurable (λ (b : δ), (i : ι), f i b) μ
@[measurability]
theorem measurable_infi {α : Type u_1} {δ : Type u_5} [borel_space α] {ι : Sort u_2} [countable ι] {f : ι δ α} (hf : (i : ι), measurable (f i)) :
measurable (λ (b : δ), (i : ι), f i b)
@[measurability]
theorem ae_measurable_infi {α : Type u_1} {δ : Type u_5} [borel_space α] {ι : Sort u_2} {μ : measure_theory.measure δ} [countable ι] {f : ι δ α} (hf : (i : ι), ae_measurable (f i) μ) :
ae_measurable (λ (b : δ), (i : ι), f i b) μ
theorem measurable_bsupr {α : Type u_1} {δ : Type u_5} [borel_space α] {ι : Type u_2} (s : set ι) {f : ι δ α} (hs : s.countable) (hf : (i : ι), measurable (f i)) :
measurable (λ (b : δ), (i : ι) (H : i s), f i b)
theorem ae_measurable_bsupr {α : Type u_1} {δ : Type u_5} [borel_space α] {ι : Type u_2} {μ : measure_theory.measure δ} (s : set ι) {f : ι δ α} (hs : s.countable) (hf : (i : ι), ae_measurable (f i) μ) :
ae_measurable (λ (b : δ), (i : ι) (H : i s), f i b) μ
theorem measurable_binfi {α : Type u_1} {δ : Type u_5} [borel_space α] {ι : Type u_2} (s : set ι) {f : ι δ α} (hs : s.countable) (hf : (i : ι), measurable (f i)) :
measurable (λ (b : δ), (i : ι) (H : i s), f i b)
theorem ae_measurable_binfi {α : Type u_1} {δ : Type u_5} [borel_space α] {ι : Type u_2} {μ : measure_theory.measure δ} (s : set ι) {f : ι δ α} (hs : s.countable) (hf : (i : ι), ae_measurable (f i) μ) :
ae_measurable (λ (b : δ), (i : ι) (H : i s), f i b) μ
theorem measurable_liminf' {α : Type u_1} {δ : Type u_5} [borel_space α] {ι : Type u_2} {ι' : Type u_3} {f : ι δ α} {u : filter ι} (hf : (i : ι), measurable (f i)) {p : ι' Prop} {s : ι' set ι} (hu : s) (hs : (i : ι'), (s i).countable) :
measurable (λ (x : δ), filter.liminf (λ (i : ι), f i x) u)

`liminf` over a general filter is measurable. See `measurable_liminf` for the version over `ℕ`.

theorem measurable_limsup' {α : Type u_1} {δ : Type u_5} [borel_space α] {ι : Type u_2} {ι' : Type u_3} {f : ι δ α} {u : filter ι} (hf : (i : ι), measurable (f i)) {p : ι' Prop} {s : ι' set ι} (hu : s) (hs : (i : ι'), (s i).countable) :
measurable (λ (x : δ), filter.limsup (λ (i : ι), f i x) u)

`limsup` over a general filter is measurable. See `measurable_limsup` for the version over `ℕ`.

@[measurability]
theorem measurable_liminf {α : Type u_1} {δ : Type u_5} [borel_space α] {f : δ α} (hf : (i : ), measurable (f i)) :
measurable (λ (x : δ), filter.liminf (λ (i : ), f i x) filter.at_top)

`liminf` over `ℕ` is measurable. See `measurable_liminf'` for a version with a general filter.

@[measurability]
theorem measurable_limsup {α : Type u_1} {δ : Type u_5} [borel_space α] {f : δ α} (hf : (i : ), measurable (f i)) :
measurable (λ (x : δ), filter.limsup (λ (i : ), f i x) filter.at_top)

`limsup` over `ℕ` is measurable. See `measurable_limsup'` for a version with a general filter.

theorem measurable_cSup {α : Type u_1} {δ : Type u_5} [borel_space α] {ι : Type u_2} {f : ι δ α} {s : set ι} (hs : s.countable) (hf : (i : ι), measurable (f i)) (bdd : (x : δ), bdd_above ((λ (i : ι), f i x) '' s)) :
measurable (λ (x : δ), has_Sup.Sup ((λ (i : ι), f i x) '' s))
def homemorph.to_measurable_equiv {α : Type u_1} {β : Type u_2} [borel_space α] [borel_space β] (h : α ≃ₜ β) :
α ≃ᵐ β

Convert a `homeomorph` to a `measurable_equiv`.

Equations
@[protected]
theorem is_finite_measure_on_compacts.map {α : Type u_1} {m0 : measurable_space α} {β : Type u_2} [borel_space β] [t2_space β] (μ : measure_theory.measure α) (f : α ≃ₜ β) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def is_R_or_C.measurable_space {𝕜 : Type u_1} [is_R_or_C 𝕜] :
Equations
@[protected, instance]
def is_R_or_C.borel_space {𝕜 : Type u_1} [is_R_or_C 𝕜] :
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
noncomputable def ennreal.measurable_space  :
Equations
@[protected, instance]
@[protected, instance]
noncomputable def ereal.measurable_space  :
Equations
@[protected, instance]
@[protected, instance]
noncomputable def complex.measurable_space  :
Equations
@[protected, instance]
@[protected, instance]
noncomputable def add_circle.measurable_space {a : } :
Equations
@[protected, instance]
@[protected, measurability]
theorem add_circle.measurable_mk' {a : } :
theorem measure_eq_measure_preimage_add_measure_tsum_Ico_zpow {α : Type u_1} (μ : measure_theory.measure α) {f : α ennreal} (hf : measurable f) {s : set α} (hs : measurable_set s) {t : nnreal} (ht : 1 < t) :
μ s = μ (s f ⁻¹' {0}) + μ (s f ⁻¹' {}) + ∑' (n : ), μ (s f ⁻¹' set.Ico (t ^ n) (t ^ (n + 1)))

One can cut out `ℝ≥0∞` into the sets `{0}`, `Ico (t^n) (t^(n+1))` for `n : ℤ` and `{∞}`. This gives a way to compute the measure of a set in terms of sets on which a given function `f` does not fluctuate by more than `t`.

@[measurability]
theorem measurable_set_ball {α : Type u_1} {x : α} {ε : } :
@[measurability]
theorem measurable_set_closed_ball {α : Type u_1} {x : α} {ε : } :
@[measurability]
theorem measurable_inf_dist {α : Type u_1} {s : set α} :
measurable (λ (x : α), s)
@[measurability]
theorem measurable.inf_dist {α : Type u_1} {β : Type u_2} {f : β α} (hf : measurable f) {s : set α} :
measurable (λ (x : β), metric.inf_dist (f x) s)
@[measurability]
theorem measurable_inf_nndist {α : Type u_1} {s : set α} :
measurable (λ (x : α),
@[measurability]
theorem measurable.inf_nndist {α : Type u_1} {β : Type u_2} {f : β α} (hf : measurable f) {s : set α} :
measurable (λ (x : β), metric.inf_nndist (f x) s)
@[measurability]
theorem measurable_dist {α : Type u_1}  :
measurable (λ (p : α × α), p.snd)
@[measurability]
theorem measurable.dist {α : Type u_1} {β : Type u_2} {f g : β α} (hf : measurable f) (hg : measurable g) :
measurable (λ (b : β), has_dist.dist (f b) (g b))
@[measurability]
theorem measurable_nndist {α : Type u_1}  :
measurable (λ (p : α × α), p.snd)
@[measurability]
theorem measurable.nndist {α : Type u_1} {β : Type u_2} {f g : β α} (hf : measurable f) (hg : measurable g) :
measurable (λ (b : β), has_nndist.nndist (f b) (g b))
theorem tendsto_measure_cthickening {α : Type u_1} {μ : measure_theory.measure α} {s : set α} (hs : (R : ) (H : R > 0), μ s) ) :
filter.tendsto (λ (r : ), μ s)) (nhds 0) (nhds (μ (closure s)))

If a set has a closed thickening with finite measure, then the measure of its `r`-closed thickenings converges to the measure of its closure as `r` tends to `0`.

theorem tendsto_measure_cthickening_of_is_closed {α : Type u_1} {μ : measure_theory.measure α} {s : set α} (hs : (R : ) (H : R > 0), μ s) ) (h's : is_closed s) :
filter.tendsto (λ (r : ), μ s)) (nhds 0) (nhds (μ s))

If a closed set has a closed thickening with finite measure, then the measure of its `r`-closed thickenings converges to its measure as `r` tends to `0`.

theorem tendsto_measure_cthickening_of_is_compact {α : Type u_1} [metric_space α] [proper_space α] {μ : measure_theory.measure α} {s : set α} (hs : is_compact s) :
filter.tendsto (λ (r : ), μ s)) (nhds 0) (nhds (μ s))

Given a compact set in a proper space, the measure of its `r`-closed thickenings converges to its measure as `r` tends to `0`.

@[measurability]
theorem measurable_set_eball {α : Type u_1} {x : α} {ε : ennreal} :
@[measurability]
theorem measurable_edist_right {α : Type u_1} {x : α} :
@[measurability]
theorem measurable_edist_left {α : Type u_1} {x : α} :
measurable (λ (y : α), x)
@[measurability]
theorem measurable_inf_edist {α : Type u_1} {s : set α} :
measurable (λ (x : α),
@[measurability]
theorem measurable.inf_edist {α : Type u_1} {β : Type u_2} {f : β α} (hf : measurable f) {s : set α} :
measurable (λ (x : β), emetric.inf_edist (f x) s)
@[measurability]
theorem measurable_edist {α : Type u_1}  :
measurable (λ (p : α × α), p.snd)
@[measurability]
theorem measurable.edist {α : Type u_1} {β : Type u_2} {f g : β α} (hf : measurable f) (hg : measurable g) :
measurable (λ (b : β), has_edist.edist (f b) (g b))
@[measurability]
theorem ae_measurable.edist {α : Type u_1} {β : Type u_2} {f g : β α} {μ : measure_theory.measure β} (hf : μ) (hg : μ) :
ae_measurable (λ (a : β), has_edist.edist (f a) (g a)) μ
theorem real.is_pi_system_Ioo_rat  :
is_pi_system ( (a b : ) (h : a < b), {set.Ioo a b})

The intervals `(-(n + 1), (n + 1))` form a finite spanning sets in the set of open intervals with rational endpoints for a locally finite measure `μ` on `ℝ`.

Equations
theorem real.measure_ext_Ioo_rat {μ ν : measure_theory.measure } (h : (a b : ), μ (set.Ioo a b) = ν (set.Ioo a b)) :
μ = ν
@[measurability]
@[measurability]
theorem measurable.real_to_nnreal {α : Type u_1} {f : α } (hf : measurable f) :
measurable (λ (x : α), (f x).to_nnreal)
@[measurability]
theorem ae_measurable.real_to_nnreal {α : Type u_1} {f : α } {μ : measure_theory.measure α} (hf : μ) :
ae_measurable (λ (x : α), (f x).to_nnreal) μ
@[measurability]
@[measurability]
theorem measurable.coe_nnreal_real {α : Type u_1} {f : α nnreal} (hf : measurable f) :
measurable (λ (x : α), (f x))
@[measurability]
theorem ae_measurable.coe_nnreal_real {α : Type u_1} {f : α nnreal} {μ : measure_theory.measure α} (hf : μ) :
ae_measurable (λ (x : α), (f x)) μ
@[measurability]
@[measurability]
theorem measurable.coe_nnreal_ennreal {α : Type u_1} {f : α nnreal} (hf : measurable f) :
measurable (λ (x : α), (f x))
@[measurability]
theorem ae_measurable.coe_nnreal_ennreal {α : Type u_1} {f : α nnreal} {μ : measure_theory.measure α} (hf : μ) :
ae_measurable (λ (x : α), (f x)) μ
@[measurability]
theorem measurable.ennreal_of_real {α : Type u_1} {f : α } (hf : measurable f) :
measurable (λ (x : α), ennreal.of_real (f x))
@[simp, norm_cast]
theorem measurable_coe_nnreal_real_iff {α : Type u_1} {f : α nnreal} :
measurable (λ (x : α), (f x))
@[simp, norm_cast]
theorem ae_measurable_coe_nnreal_real_iff {α : Type u_1} {f : α nnreal} {μ : measure_theory.measure α} :
ae_measurable (λ (x : α), (f x)) μ

The set of finite `ℝ≥0∞` numbers is `measurable_equiv` to `ℝ≥0`.

Equations
theorem ennreal.measurable_of_measurable_nnreal {α : Type u_1} {f : ennreal α} (h : measurable (λ (p : nnreal), f p)) :

`ℝ≥0∞` is `measurable_equiv` to `ℝ≥0 ⊕ unit`.

Equations
theorem ennreal.measurable_of_measurable_nnreal_prod {β : Type u_2} {γ : Type u_3} {f : γ} (H₁ : measurable (λ (p : nnreal × β), f ((p.fst), p.snd))) (H₂ : measurable (λ (x : β), f (, x))) :
theorem ennreal.measurable_of_measurable_nnreal_nnreal {β : Type u_2} {f : β} (h₁ : measurable (λ (p : , f ((p.fst), (p.snd)))) (h₂ : measurable (λ (r : nnreal), f (, r))) (h₃ : measurable (λ (r : nnreal), f (r, ))) :
@[measurability]
@[measurability]
@[measurability]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[measurability]
theorem measurable.ennreal_to_nnreal {α : Type u_1} {f : α ennreal} (hf : measurable f) :
measurable (λ (x : α), (f x).to_nnreal)
@[measurability]
theorem ae_measurable.ennreal_to_nnreal {α : Type u_1} {f : α ennreal} {μ : measure_theory.measure α} (hf : μ) :
ae_measurable (λ (x : α), (f x).to_nnreal) μ
@[simp, norm_cast]
theorem measurable_coe_nnreal_ennreal_iff {α : Type u_1} {f : α nnreal} :
measurable (λ (x : α), (f x))
@[simp, norm_cast]
theorem ae_measurable_coe_nnreal_ennreal_iff {α : Type u_1} {f : α nnreal} {μ : measure_theory.measure α} :
ae_measurable (λ (x : α), (f x)) μ
@[measurability]
theorem measurable.ennreal_to_real {α : Type u_1} {f : α ennreal} (hf : measurable f) :
measurable (λ (x : α), (f x).to_real)
@[measurability]
theorem ae_measurable.ennreal_to_real {α : Type u_1} {f : α ennreal} {μ : measure_theory.measure α} (hf : μ) :
ae_measurable (λ (x : α), (f x).to_real) μ
@[measurability]
theorem measurable.ennreal_tsum {α : Type u_1} {ι : Type u_2} [countable ι] {f : ι } (h : (i : ι), measurable (f i)) :
measurable (λ (x : α), ∑' (i : ι), f i x)

note: `ℝ≥0∞` can probably be generalized in a future version of this lemma.

@[measurability]
theorem measurable.ennreal_tsum' {α : Type u_1} {ι : Type u_2} [countable ι] {f : ι } (h : (i : ι), measurable (f i)) :
measurable (∑' (i : ι), f i)
@[measurability]
theorem measurable.nnreal_tsum {α : Type u_1} {ι : Type u_2} [countable ι] {f : ι } (h : (i : ι), measurable (f i)) :
measurable (λ (x : α), ∑' (i : ι), f i x)
@[measurability]
theorem ae_measurable.ennreal_tsum {α : Type u_1} {ι : Type u_2} [countable ι] {f : ι } {μ : measure_theory.measure α} (h : (i : ι), ae_measurable (f i) μ) :
ae_measurable (λ (x : α), ∑' (i : ι), f i x) μ
@[measurability]
theorem ae_measurable.nnreal_tsum {α : Type u_1} {ι : Type u_2} [countable ι] {f : ι } {μ : measure_theory.measure α} (h : (i : ι), ae_measurable (f i) μ) :
ae_measurable (λ (x : α), ∑' (i : ι), f i x) μ
@[measurability]
@[measurability]
theorem measurable.coe_real_ereal {α : Type u_1} {f : α } (hf : measurable f) :
measurable (λ (x : α), (f x))
@[measurability]
theorem ae_measurable.coe_real_ereal {α : Type u_1} {f : α } {μ : measure_theory.measure α} (hf : μ) :
ae_measurable (λ (x : α), (f x)) μ

The set of finite `ereal` numbers is `measurable_equiv` to `ℝ`.

Equations
theorem ereal.measurable_of_measurable_real {α : Type u_1} {f : ereal α} (h : measurable (λ (p : ), f p)) :
@[measurability]
@[measurability]
theorem measurable.ereal_to_real {α : Type u_1} {f : α ereal} (hf : measurable f) :
measurable (λ (x : α), (f x).to_real)
@[measurability]
theorem ae_measurable.ereal_to_real {α : Type u_1} {f : α ereal} {μ : measure_theory.measure α} (hf : μ) :
ae_measurable (λ (x : α), (f x).to_real) μ
@[measurability]
@[measurability]
theorem measurable.coe_ereal_ennreal {α : Type u_1} {f : α ennreal} (hf : measurable f) :
measurable (λ (x : α), (f x))
@[measurability]
theorem ae_measurable.coe_ereal_ennreal {α : Type u_1} {f : α ennreal} {μ : measure_theory.measure α} (hf : μ) :
ae_measurable (λ (x : α), (f x)) μ
@[measurability]
theorem measurable_norm {α : Type u_1}  :
@[measurability]
theorem measurable.norm {α : Type u_1} {β : Type u_2} {f : β α} (hf : measurable f) :
measurable (λ (a : β), f a)
@[measurability]
theorem ae_measurable.norm {α : Type u_1} {β : Type u_2} {f : β α} {μ : measure_theory.measure β} (hf : μ) :
ae_measurable (λ (a : β), f a) μ
@[measurability]
theorem measurable_nnnorm {α : Type u_1}  :
@[measurability]
theorem measurable.nnnorm {α : Type u_1} {β : Type u_2} {f : β α} (hf : measurable f) :
measurable (λ (a : β), f a‖₊)
@[measurability]
theorem ae_measurable.nnnorm {α : Type u_1} {β : Type u_2} {f : β α} {μ : measure_theory.measure β} (hf : μ) :
ae_measurable (λ (a : β), f a‖₊) μ
@[measurability]
theorem measurable_ennnorm {α : Type u_1}  :
measurable (λ (x : α), x‖₊)
@[measurability]
theorem measurable.ennnorm {α : Type u_1} {β : Type u_2} {f : β α} (hf : measurable f) :
measurable (λ (a : β), f a‖₊)
@[measurability]
theorem ae_measurable.ennnorm {α : Type u_1} {β : Type u_2} {f : β α} {μ : measure_theory.measure β} (hf : μ) :
ae_measurable (λ (a : β), f a‖₊) μ
theorem measurable_of_tendsto_ennreal' {α : Type u_1} {ι : Type u_2} {f : ι } {g : α ennreal} (u : filter ι) [u.ne_bot] (hf : (i : ι), measurable (f i)) (lim : (nhds g)) :

A limit (over a general filter) of measurable `ℝ≥0∞` valued functions is measurable.

theorem measurable_of_tendsto_ennreal {α : Type u_1} {f : } {g : α ennreal} (hf : (i : ), measurable (f i)) (lim : (nhds g)) :

A sequential limit of measurable `ℝ≥0∞` valued functions is measurable.

theorem measurable_of_tendsto_nnreal' {α : Type u_1} {ι : Type u_2} {f : ι } {g : α nnreal} (u : filter ι) [u.ne_bot] (hf : (i : ι), measurable (f i)) (lim : (nhds g)) :

A limit (over a general filter) of measurable `ℝ≥0` valued functions is measurable.

theorem measurable_of_tendsto_nnreal {α : Type u_1} {f : } {g : α nnreal} (hf : (i : ), measurable (f i)) (lim : (nhds g)) :

A sequential limit of measurable `ℝ≥0` valued functions is measurable.

theorem measurable_of_tendsto_metrizable' {α : Type u_1} {β : Type u_2} [borel_space β] {ι : Type u_3} {f : ι α β} {g : α β} (u : filter ι) [u.ne_bot] (hf : (i : ι), measurable (f i)) (lim : (nhds g)) :

A limit (over a general filter) of measurable functions valued in a (pseudo) metrizable space is measurable.

theorem measurable_of_tendsto_metrizable {α : Type u_1} {β : Type u_2} [borel_space β] {f : α β} {g : α β} (hf : (i : ), measurable (f i)) (lim : (nhds g)) :

A sequential limit of measurable functions valued in a (pseudo) metrizable space is measurable.

theorem ae_measurable_of_tendsto_metrizable_ae {α : Type u_1} {β : Type u_2} [borel_space β] {ι : Type u_3} {μ : measure_theory.measure α} {f : ι α β} {g : α β} (u : filter ι) [hu : u.ne_bot] (hf : (n : ι), ae_measurable (f n) μ) (h_tendsto : ∀ᵐ (x : α) μ, filter.tendsto (λ (n : ι), f n x) u (nhds (g x))) :
theorem ae_measurable_of_tendsto_metrizable_ae' {α : Type u_1} {β : Type u_2} [borel_space β] {μ : measure_theory.measure α} {f : α β} {g : α β} (hf : (n : ), ae_measurable (f n) μ) (h_ae_tendsto : ∀ᵐ (x : α) μ, filter.tendsto (λ (n : ), f n x) filter.at_top (nhds (g x))) :
theorem ae_measurable_of_unif_approx {α : Type u_1} {β : Type u_2} [borel_space β] {μ : measure_theory.measure α} {g : α β} (hf : (ε : ), ε > 0 ( (f : α β), ∀ᵐ (x : α) μ, has_dist.dist (f x) (g x) ε)) :
theorem measurable_of_tendsto_metrizable_ae {α : Type u_1} {β : Type u_2} [borel_space β] {μ : measure_theory.measure α} [μ.is_complete] {f : α β} {g : α β} (hf : (n : ), measurable (f n)) (h_ae_tendsto : ∀ᵐ (x : α) μ, filter.tendsto (λ (n : ), f n x) filter.at_top (nhds (g x))) :
theorem measurable_limit_of_tendsto_metrizable_ae {α : Type u_1} {β : Type u_2} [borel_space β] {ι : Type u_3} [countable ι] [nonempty ι] {μ : measure_theory.measure α} {f : ι α β} {L : filter ι} (hf : (n : ι), ae_measurable (f n) μ) (h_ae_tendsto : ∀ᵐ (x : α) μ, (l : β), filter.tendsto (λ (n : ι), f n x) L (nhds l)) :
(f_lim : α β) (hf_lim_meas : measurable f_lim), ∀ᵐ (x : α) μ, filter.tendsto (λ (n : ι), f n x) L (nhds (f_lim x))
@[protected, measurability]
theorem continuous_linear_map.measurable {𝕜 : Type u_6} [normed_field 𝕜] {E : Type u_7} [ E] {F : Type u_8} [ F] [borel_space F] (L : E →L[𝕜] F) :
theorem continuous_linear_map.measurable_comp {α : Type u_1} {𝕜 : Type u_6} [normed_field 𝕜] {E : Type u_7} [ E] {F : Type u_8} [ F] [borel_space F] (L : E →L[𝕜] F) {φ : α E} (φ_meas : measurable φ) :
measurable (λ (a : α), L (φ a))
@[protected, instance]
def continuous_linear_map.measurable_space {𝕜 : Type u_6} {E : Type u_7} [ E] {F : Type u_8} [ F] :
Equations
@[protected, instance]
def continuous_linear_map.borel_space {𝕜 : Type u_6} {E : Type u_7} [ E] {F : Type u_8} [ F] :
@[measurability]
theorem continuous_linear_map.measurable_apply {𝕜 : Type u_6} {E : Type u_7} [ E] {F : Type u_8} [ F] [borel_space F] (x : E) :
measurable (λ (f : E →L[𝕜] F), f x)
@[measurability]
theorem continuous_linear_map.measurable_apply' {𝕜 : Type u_6} {E : Type u_7} [ E] {F : Type u_8} [ F] [borel_space F] :
measurable (λ (x : E) (f : E →L[𝕜] F), f x)
@[measurability]
theorem continuous_linear_map.measurable_coe {𝕜 : Type u_6} {E : Type u_7} [ E] {F : Type u_8} [ F] [borel_space F] :
measurable (λ (f : E →L[𝕜] F) (x : E), f x)
@[measurability]
theorem measurable.apply_continuous_linear_map {α : Type u_1} {𝕜 : Type u_6} {E : Type u_7} [ E] [borel_space E] {F : Type u_8} [ F] {φ : α (F →L[𝕜] E)} (hφ : measurable φ) (v : F) :
measurable (λ (a : α), (φ a) v)
@[measurability]
theorem ae_measurable.apply_continuous_linear_map {α : Type u_1} {𝕜 : Type u_6} {E : Type u_7} [ E] [borel_space E] {F : Type u_8} [ F] {φ : α (F →L[𝕜] E)} {μ : measure_theory.measure α} (hφ : μ) (v : F) :
ae_measurable (λ (a : α), (φ a) v) μ
theorem measurable_smul_const {α : Type u_1} {𝕜 : Type u_6} [borel_space 𝕜] {E : Type u_7} [ E] [borel_space E] {f : α 𝕜} {c : E} (hc : c 0) :
measurable (λ (x : α), f x c)
theorem ae_measurable_smul_const {α : Type u_1} {𝕜 : Type u_6} [borel_space 𝕜] {E : Type u_7} [ E] [borel_space E] {f : α 𝕜} {μ : measure_theory.measure α} {c : E} (hc : c 0) :
ae_measurable (λ (x : α), f x c) μ