# Borel (measurable) space #

## Main definitions #

• borel α : the least σ-algebra that contains all open sets;
• class BorelSpace : a space with TopologicalSpace and MeasurableSpace structures such that ‹MeasurableSpace α› = borel α;
• class OpensMeasurableSpace : a space with TopologicalSpace and MeasurableSpace structures such that all open sets are measurable; equivalently, borel α ≤ ‹MeasurableSpace α›.
• BorelSpace instances on Empty, Unit, Bool, Nat, Int, Rat;
• MeasurableSpace and BorelSpace instances on ℝ, ℝ≥0, ℝ≥0∞.

## Main statements #

• IsOpen.measurableSet, IsClosed.measurableSet: 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 fun 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;
• AEMeasurable.add : similar dot notation for almost everywhere measurable functions;
• Measurable.ennreal* : special cases for arithmetic operations on ℝ≥0∞.
def borel (α : Type u) [] :

MeasurableSpace structure generated by TopologicalSpace.

Equations
Instances For
theorem borel_anti {α : Type u_1} :
theorem borel_eq_top_of_discrete {α : Type u_1} [] [] :
theorem borel_eq_top_of_countable {α : Type u_1} [] [] [] :
theorem borel_eq_generateFrom_of_subbasis {α : Type u_1} {s : Set (Set α)} [t : ] (hs : ) :
theorem isPiSystem_isOpen {α : Type u_1} [] :
IsPiSystem {s : Set α | }
theorem isPiSystem_isClosed {α : Type u_1} [] :
IsPiSystem {s : Set α | }
theorem borel_comap {α : Type u_1} {β : Type u_2} {f : αβ} {t : } :
=
theorem Continuous.borel_measurable {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
class OpensMeasurableSpace (α : Type u_6) [] [h : ] :

A space with MeasurableSpace and TopologicalSpace structures such that all open sets are measurable.

• borel_le : h

Borel-measurable sets are measurable.

Instances
class BorelSpace (α : Type u_6) [] [] :

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

• measurable_eq : inst✝ =

The measurable sets are exactly the Borel-measurable sets.

Instances

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

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

Finally, borelize α β γ runs borelize α; borelize β; borelize γ.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Add instances borel e : MeasurableSpace e and ⟨rfl⟩ : BorelSpace e.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Given a type e, an assumption i : MeasurableSpace e, and an instance [BorelSpace e], replace i with borel e.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Given a type $t, if there is an assumption [i : MeasurableSpace$t], then try to prove [BorelSpace $t] and replace i with borel$t. Otherwise, add instances borel $t : MeasurableSpace$t and ⟨rfl⟩ : BorelSpace \$t.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance OrderDual.opensMeasurableSpace {α : Type u_6} [] [] [h : ] :
Equations
• =
instance OrderDual.borelSpace {α : Type u_6} [] [] [h : ] :
Equations
• =
instance BorelSpace.opensMeasurable {α : Type u_6} [] [] [] :

In a BorelSpace all open sets are measurable.

Equations
• =
instance Subtype.borelSpace {α : Type u_6} [] [] [hα : ] (s : Set α) :
Equations
• =
instance Countable.instBorelSpace {α : Type u_1} [] [] [] [] :
Equations
• =
instance Subtype.opensMeasurableSpace {α : Type u_6} [] [] [h : ] (s : Set α) :
Equations
• =
theorem opensMeasurableSpace_iff_forall_measurableSet {α : Type u_1} [] [] :
∀ (s : Set α),
instance BorelSpace.countablyGenerated {α : Type u_6} [] [] [] :
Equations
• =
theorem MeasurableSet.induction_on_open {α : Type u_1} [] [] [] {C : Set αProp} (h_open : ∀ (U : Set α), C U) (h_compl : ∀ (t : Set α), C tC t) (h_union : ∀ (f : Set α), Pairwise (Disjoint on f)(∀ (i : ), MeasurableSet (f i))(∀ (i : ), C (f i))C (⋃ (i : ), f i)) ⦃t : Set α :
C t
theorem IsOpen.measurableSet {α : Type u_1} {s : Set α} [] [] (h : ) :
instance instHasCountableSeparatingOnMeasurableSet {α : Type u_1} [] [] {s : Set α} [HasCountableSeparatingOn α IsOpen s] :
HasCountableSeparatingOn α MeasurableSet s
Equations
• =
theorem measurableSet_interior {α : Type u_1} {s : Set α} [] [] :
theorem IsGδ.measurableSet {α : Type u_1} {s : Set α} [] [] (h : IsGδ s) :
theorem measurableSet_of_continuousAt {α : Type u_1} [] [] {β : Type u_6} [] (f : αβ) :
MeasurableSet {x : α | }
theorem IsClosed.measurableSet {α : Type u_1} {s : Set α} [] [] (h : ) :
theorem IsCompact.measurableSet {α : Type u_1} {s : Set α} [] [] [] (h : ) :
theorem Inseparable.mem_measurableSet_iff {γ : Type u_3} [] [] [] {x : γ} {y : γ} (h : ) {s : Set γ} (hs : ) :
x s y s

If two points are topologically inseparable, then they can't be separated by a Borel measurable set.

theorem IsCompact.closure_subset_measurableSet {γ : Type u_3} [] [] [] [] {K : Set γ} {s : Set γ} (hK : ) (hs : ) (hKs : K s) :
s

If K is a compact set in an R₁ space and s ⊇ K is a Borel measurable superset, then s includes the closure of K as well.

theorem IsCompact.measure_closure {γ : Type u_3} [] [] [] [] {K : Set γ} (hK : ) (μ : ) :
μ () = μ K

In an R₁ topological space with Borel measure μ, the measure of the closure of a compact set K is equal to the measure of K.

See also MeasureTheory.Measure.OuterRegular.measure_closure_eq_of_isCompact for a version that assumes μ to be outer regular but does not assume the σ-algebra to be Borel.

theorem measurableSet_closure {α : Type u_1} {s : Set α} [] [] :
theorem measurable_of_isOpen {γ : Type u_3} {δ : Type u_5} [] [] [] [] {f : δγ} (hf : ∀ (s : Set γ), MeasurableSet (f ⁻¹' s)) :
theorem measurable_of_isClosed {γ : Type u_3} {δ : Type u_5} [] [] [] [] {f : δγ} (hf : ∀ (s : Set γ), MeasurableSet (f ⁻¹' s)) :
theorem measurable_of_isClosed' {γ : Type u_3} {δ : Type u_5} [] [] [] [] {f : δγ} (hf : ∀ (s : Set γ), s Set.univMeasurableSet (f ⁻¹' s)) :
instance nhds_isMeasurablyGenerated {α : Type u_1} [] [] (a : α) :
Equations
• =
theorem MeasurableSet.nhdsWithin_isMeasurablyGenerated {α : Type u_1} [] [] {s : Set α} (hs : ) (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 : MeasurableSet s.

instance OpensMeasurableSpace.separatesPoints {α : Type u_1} [] [] [] :
Equations
• =
Equations
• =
instance Pi.opensMeasurableSpace {ι : Type u_6} {π : ιType u_7} [] [t' : (i : ι) → TopologicalSpace (π i)] [(i : ι) → MeasurableSpace (π i)] [∀ (i : ι), ] [∀ (i : ι), OpensMeasurableSpace (π i)] :
OpensMeasurableSpace ((i : ι) → π i)
Equations
• =
class SecondCountableTopologyEither (α : Type u_6) (β : Type u_7) [] [] :

The typeclass SecondCountableTopologyEither α β 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.

• The projection out of SecondCountableTopologyEither

Instances
instance secondCountableTopologyEither_of_left (α : Type u_6) (β : Type u_7) [] [] :
Equations
• =
instance secondCountableTopologyEither_of_right (α : Type u_6) (β : Type u_7) [] [] :
Equations
• =
instance Prod.opensMeasurableSpace {α : Type u_1} {β : Type u_2} [] [] [] [] [h : ] :

If either α or β has second-countable topology, then the open sets in α × β belong to the product sigma-algebra.

Equations
• =
theorem interior_ae_eq_of_null_frontier {α' : Type u_6} [] [] {μ : } {s : Set α'} (h : μ () = 0) :
theorem measure_interior_of_null_frontier {α' : Type u_6} [] [] {μ : } {s : Set α'} (h : μ () = 0) :
μ () = μ s
theorem nullMeasurableSet_of_null_frontier {α : Type u_1} [] [] {s : Set α} {μ : } (h : μ () = 0) :
theorem closure_ae_eq_of_null_frontier {α' : Type u_6} [] [] {μ : } {s : Set α'} (h : μ () = 0) :
theorem measure_closure_of_null_frontier {α' : Type u_6} [] [] {μ : } {s : Set α'} (h : μ () = 0) :
μ () = μ s
@[simp]
theorem measurableSet_Ici {α : Type u_1} [] [] [] {a : α} :
@[simp]
theorem measurableSet_Iic {α : Type u_1} [] [] [] {a : α} :
@[simp]
theorem measurableSet_Icc {α : Type u_1} [] [] [] {a : α} {b : α} :
instance nhdsWithin_Ici_isMeasurablyGenerated {α : Type u_1} [] [] [] {a : α} {b : α} :
Equations
• =
instance nhdsWithin_Iic_isMeasurablyGenerated {α : Type u_1} [] [] [] {a : α} {b : α} :
Equations
• =
instance nhdsWithin_Icc_isMeasurablyGenerated {α : Type u_1} [] [] [] {a : α} {b : α} {x : α} :
Equations
• =
instance atTop_isMeasurablyGenerated {α : Type u_1} [] [] [] :
Equations
• =
instance atBot_isMeasurablyGenerated {α : Type u_1} [] [] [] :
Equations
• =
instance instIsMeasurablyGeneratedCocompact {α : Type u_1} [] [] [] :
Equations
• =
theorem measurableSet_le' {α : Type u_1} [] [] [] :
MeasurableSet {p : α × α | p.1 p.2}
theorem measurableSet_le {α : Type u_1} {δ : Type u_5} [] [] [] [] {f : δα} {g : δα} (hf : ) (hg : ) :
MeasurableSet {a : δ | f a g a}
@[simp]
theorem measurableSet_Iio {α : Type u_1} [] [] [] {a : α} :
@[simp]
theorem measurableSet_Ioi {α : Type u_1} [] [] [] {a : α} :
@[simp]
theorem measurableSet_Ioo {α : Type u_1} [] [] [] {a : α} {b : α} :
@[simp]
theorem measurableSet_Ioc {α : Type u_1} [] [] [] {a : α} {b : α} :
@[simp]
theorem measurableSet_Ico {α : Type u_1} [] [] [] {a : α} {b : α} :
instance nhdsWithin_Ioi_isMeasurablyGenerated {α : Type u_1} [] [] [] {a : α} {b : α} :
Equations
• =
instance nhdsWithin_Iio_isMeasurablyGenerated {α : Type u_1} [] [] [] {a : α} {b : α} :
Equations
• =
instance nhdsWithin_uIcc_isMeasurablyGenerated {α : Type u_1} [] [] [] {a : α} {b : α} {x : α} :
Equations
• =
theorem measurableSet_lt' {α : Type u_1} [] [] [] :
MeasurableSet {p : α × α | p.1 < p.2}
theorem measurableSet_lt {α : Type u_1} {δ : Type u_5} [] [] [] [] {f : δα} {g : δα} (hf : ) (hg : ) :
MeasurableSet {a : δ | f a < g a}
theorem nullMeasurableSet_lt {α : Type u_1} {δ : Type u_5} [] [] [] [] {μ : } {f : δα} {g : δα} (hf : ) (hg : ) :
MeasureTheory.NullMeasurableSet {a : δ | f a < g a} μ
theorem nullMeasurableSet_lt' {α : Type u_1} [] [] [] {μ : MeasureTheory.Measure (α × α)} :
MeasureTheory.NullMeasurableSet {p : α × α | p.1 < p.2} μ
theorem nullMeasurableSet_le {α : Type u_1} {δ : Type u_5} [] [] [] [] {μ : } {f : δα} {g : δα} (hf : ) (hg : ) :
MeasureTheory.NullMeasurableSet {a : δ | f a g a} μ
theorem Set.OrdConnected.measurableSet {α : Type u_1} {s : Set α} [] [] [] (h : ) :
theorem IsPreconnected.measurableSet {α : Type u_1} {s : Set α} [] [] [] (h : ) :
theorem generateFrom_Ico_mem_le_borel {α : Type u_7} [] [] (s : Set α) (t : Set α) :
MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ t, l < u Set.Ico l u = S}
theorem Dense.borel_eq_generateFrom_Ico_mem_aux {α : Type u_7} [] [] [] {s : Set α} (hd : ) (hbot : ∀ (x : α), x s) (hIoo : ∀ (x y : α), x < ySet.Ioo x y = y s) :
= MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u Set.Ico l u = S}
theorem Dense.borel_eq_generateFrom_Ico_mem {α : Type u_7} [] [] [] [] [] {s : Set α} (hd : ) :
= MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u Set.Ico l u = S}
theorem borel_eq_generateFrom_Ico (α : Type u_7) [] [] [] :
= MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l < u Set.Ico l u = S}
theorem Dense.borel_eq_generateFrom_Ioc_mem_aux {α : Type u_7} [] [] [] {s : Set α} (hd : ) (hbot : ∀ (x : α), x s) (hIoo : ∀ (x y : α), x < ySet.Ioo x y = x s) :
= MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u Set.Ioc l u = S}
theorem Dense.borel_eq_generateFrom_Ioc_mem {α : Type u_7} [] [] [] [] [] {s : Set α} (hd : ) :
= MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u Set.Ioc l u = S}
theorem borel_eq_generateFrom_Ioc (α : Type u_7) [] [] [] :
= MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l < u Set.Ioc l u = S}
theorem MeasureTheory.Measure.ext_of_Ico_finite {α : Type u_7} [] {m : } [] [] [] (μ : ) (ν : ) (hμν : μ Set.univ = ν Set.univ) (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, MeasureTheory.Measure.ext_of_Ico is an extensionality lemma with weaker assumptions on μ and ν.

theorem MeasureTheory.Measure.ext_of_Ioc_finite {α : Type u_7} [] {m : } [] [] [] (μ : ) (ν : ) (hμν : μ Set.univ = ν Set.univ) (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, MeasureTheory.Measure.ext_of_Ioc is an extensionality lemma with weaker assumptions on μ and ν.

theorem MeasureTheory.Measure.ext_of_Ico' {α : Type u_7} [] {m : } [] [] [] [] (μ : ) (ν : ) (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 they agree on all closed-open intervals.

theorem MeasureTheory.Measure.ext_of_Ioc' {α : Type u_7} [] {m : } [] [] [] [] (μ : ) (ν : ) (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 they agree on all open-closed intervals.

theorem MeasureTheory.Measure.ext_of_Ico {α : Type u_7} [] {_m : } [] [] [] (μ : ) (ν : ) (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 they agree on all closed-open intervals.

theorem MeasureTheory.Measure.ext_of_Ioc {α : Type u_7} [] {_m : } [] [] [] (μ : ) (ν : ) (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 they agree on all open-closed intervals.

theorem MeasureTheory.Measure.ext_of_Iic {α : Type u_7} [] {m : } [] [] [] (μ : ) (ν : ) (h : ∀ (a : α), μ () = ν ()) :
μ = ν

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

theorem MeasureTheory.Measure.ext_of_Ici {α : Type u_7} [] {m : } [] [] [] (μ : ) (ν : ) (h : ∀ (a : α), μ () = ν ()) :
μ = ν

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

theorem measurableSet_uIcc {α : Type u_1} [] [] [] {a : α} {b : α} :
theorem measurableSet_uIoc {α : Type u_1} [] [] [] {a : α} {b : α} :
theorem Measurable.max {α : Type u_1} {δ : Type u_5} [] [] [] [] {f : δα} {g : δα} (hf : ) (hg : ) :
Measurable fun (a : δ) => max (f a) (g a)
theorem AEMeasurable.max {α : Type u_1} {δ : Type u_5} [] [] [] [] {f : δα} {g : δα} {μ : } (hf : ) (hg : ) :
AEMeasurable (fun (a : δ) => max (f a) (g a)) μ
theorem Measurable.min {α : Type u_1} {δ : Type u_5} [] [] [] [] {f : δα} {g : δα} (hf : ) (hg : ) :
Measurable fun (a : δ) => min (f a) (g a)
theorem AEMeasurable.min {α : Type u_1} {δ : Type u_5} [] [] [] [] {f : δα} {g : δα} {μ : } (hf : ) (hg : ) :
AEMeasurable (fun (a : δ) => min (f a) (g a)) μ
theorem Continuous.measurable {α : Type u_1} {γ : Type u_3} [] [] [] [] [] {f : αγ} (hf : ) :

A continuous function from an OpensMeasurableSpace to a BorelSpace is measurable.

theorem Continuous.aemeasurable {α : Type u_1} {γ : Type u_3} [] [] [] [] [] {f : αγ} (h : ) {μ : } :

A continuous function from an OpensMeasurableSpace to a BorelSpace is ae-measurable.

theorem ClosedEmbedding.measurable {α : Type u_1} {γ : Type u_3} [] [] [] [] [] {f : αγ} (hf : ) :
theorem ContinuousOn.measurable_piecewise {α : Type u_1} {γ : Type u_3} [] [] [] [] [] {f : αγ} {g : αγ} {s : Set α} [(j : α) → Decidable (j s)] (hf : ) (hg : ) (hs : ) :

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

Equations
• =
instance ContinuousMul.measurableMul {γ : Type u_3} [] [] [] [Mul γ] [] :
Equations
• =
instance ContinuousSub.measurableSub {γ : Type u_3} [] [] [] [Sub γ] [] :
Equations
• =
instance TopologicalAddGroup.measurableNeg {γ : Type u_3} [] [] [] [] :
Equations
• =
instance TopologicalGroup.measurableInv {γ : Type u_3} [] [] [] [] [] :
Equations
• =
instance ContinuousSMul.measurableSMul {M : Type u_7} {α : Type u_8} [] [] [] [] [] [SMul M α] [] :
Equations
• =
instance ContinuousSup.measurableSup {γ : Type u_3} [] [] [] [Sup γ] [] :
Equations
• =
instance ContinuousSup.measurableSup₂ {γ : Type u_3} [] [] [] [Sup γ] [] :
Equations
• =
instance ContinuousInf.measurableInf {γ : Type u_3} [] [] [] [Inf γ] [] :
Equations
• =
instance ContinuousInf.measurableInf₂ {γ : Type u_3} [] [] [] [Inf γ] [] :
Equations
• =
theorem Homeomorph.measurable {α : Type u_1} {γ : Type u_3} [] [] [] [] [] (h : α ≃ₜ γ) :
def Homeomorph.toMeasurableEquiv {γ : Type u_3} {γ₂ : Type u_4} [] [] [] [] [] [] (h : γ ≃ₜ γ₂) :
γ ≃ᵐ γ₂

A homeomorphism between two Borel spaces is a measurable equivalence.

Equations
• = { toEquiv := h.toEquiv, measurable_toFun := , measurable_invFun := }
Instances For
theorem Homeomorph.measurableEmbedding {γ : Type u_3} {γ₂ : Type u_4} [] [] [] [] [] [] (h : γ ≃ₜ γ₂) :
@[simp]
theorem Homeomorph.toMeasurableEquiv_coe {γ : Type u_3} {γ₂ : Type u_4} [] [] [] [] [] [] (h : γ ≃ₜ γ₂) :
@[simp]
theorem Homeomorph.toMeasurableEquiv_symm_coe {γ : Type u_3} {γ₂ : Type u_4} [] [] [] [] [] [] (h : γ ≃ₜ γ₂) :
.symm = ()
theorem ContinuousMap.measurable {α : Type u_1} {γ : Type u_3} [] [] [] [] [] (f : C(α, γ)) :
theorem measurable_of_continuousOn_compl_singleton {α : Type u_1} {γ : Type u_3} [] [] [] [] [] [] {f : αγ} (a : α) (hf : ContinuousOn f {a}) :
theorem Continuous.measurable2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_5} [] [] [] [] [] [] [] [] {f : δα} {g : δβ} {c : αβγ} (h : Continuous fun (p : α × β) => c p.1 p.2) (hf : ) (hg : ) :
Measurable fun (a : δ) => c (f a) (g a)
theorem Continuous.aemeasurable2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_5} [] [] [] [] [] [] [] [] {f : δα} {g : δβ} {c : αβγ} {μ : } (h : Continuous fun (p : α × β) => c p.1 p.2) (hf : ) (hg : ) :
AEMeasurable (fun (a : δ) => c (f a) (g a)) μ
instance HasContinuousInv₀.measurableInv {γ : Type u_3} [] [] [] [] [] :
Equations
• =
instance ContinuousAdd.measurableMul₂ {γ : Type u_3} [] [] [] [Add γ] [] :
Equations
• =
instance ContinuousMul.measurableMul₂ {γ : Type u_3} [] [] [] [Mul γ] [] :
Equations
• =
instance ContinuousSub.measurableSub₂ {γ : Type u_3} [] [] [] [Sub γ] [] :
Equations
• =
instance ContinuousSMul.measurableSMul₂ {M : Type u_7} {α : Type u_8} [] [] [] [] [] [SMul M α] [] :
Equations
• =
theorem pi_le_borel_pi {ι : Type u_6} {π : ιType u_7} [(i : ι) → TopologicalSpace (π i)] [(i : ι) → MeasurableSpace (π i)] [∀ (i : ι), BorelSpace (π i)] :
MeasurableSpace.pi borel ((i : ι) → π i)
theorem prod_le_borel_prod {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] :
Prod.instMeasurableSpace borel (α × β)
instance Pi.borelSpace {ι : Type u_6} {π : ιType u_7} [] [(i : ι) → TopologicalSpace (π i)] [(i : ι) → MeasurableSpace (π i)] [∀ (i : ι), ] [∀ (i : ι), BorelSpace (π i)] :
BorelSpace ((i : ι) → π i)
Equations
• =
instance Prod.borelSpace {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] :
BorelSpace (α × β)
Equations
• =
theorem MeasurableEmbedding.borelSpace {α : Type u_6} {β : Type u_7} [] [] [] [] [hβ : ] {e : αβ} (h'e : ) (h''e : ) :

Given a measurable embedding to a Borel space which is also a topological embedding, then the source space is also a Borel space.

instance ULift.instBorelSpace {α : Type u_1} [] [] [] :
Equations
• =
instance DiscreteMeasurableSpace.toBorelSpace {α : Type u_6} [] [] [] :
Equations
• =
theorem Embedding.measurableEmbedding {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] {f : αβ} (h₁ : ) (h₂ : ) :
theorem ClosedEmbedding.measurableEmbedding {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] {f : αβ} (h : ) :
theorem OpenEmbedding.measurableEmbedding {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] {f : αβ} (h : ) :
theorem measurable_of_Iio {α : Type u_1} {δ : Type u_5} [] [] [] [] [] [] {f : δα} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' )) :
theorem UpperSemicontinuous.measurable {α : Type u_1} {δ : Type u_5} [] [] [] [] [] [] [] {f : δα} (hf : ) :
theorem measurable_of_Ioi {α : Type u_1} {δ : Type u_5} [] [] [] [] [] [] {f : δα} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' )) :
theorem LowerSemicontinuous.measurable {α : Type u_1} {δ : Type u_5} [] [] [] [] [] [] [] {f : δα} (hf : ) :
theorem measurable_of_Iic {α : Type u_1} {δ : Type u_5} [] [] [] [] [] [] {f : δα} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' )) :
theorem measurable_of_Ici {α : Type u_1} {δ : Type u_5} [] [] [] [] [] [] {f : δα} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' )) :
theorem Measurable.isLUB {α : Type u_1} {δ : Type u_5} [] [] [] [] [] [] {ι : Sort u_6} [] {f : ιδα} {g : δα} (hf : ∀ (i : ι), Measurable (f i)) (hg : ∀ (b : δ), IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)) :

If a function is the least upper bound of countably many measurable functions, then it is measurable.

theorem Measurable.isLUB_of_mem {α : Type u_1} {δ : Type u_5} [] [] [] [] [] [] {ι : Sort u_6} [] {f : ιδα} {g : δα} {g' : δα} (hf : ∀ (i : ι), Measurable (f i)) {s : Set δ} (hs : ) (hg : bs, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)) (hg' : Set.EqOn g g' s) (g'_meas : ) :

If a function is the least upper bound of countably many measurable functions on a measurable set s, and coincides with a measurable function outside of s, then it is measurable.

theorem AEMeasurable.isLUB {α : Type u_1} {δ : Type u_5} [] [] [] [] [] [] {ι : Sort u_6} {μ : } [] {f : ιδα} {g : δα} (hf : ∀ (i : ι), AEMeasurable (f i) μ) (hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)) :
theorem Measurable.isGLB {α : Type u_1} {δ : Type u_5} [] [] [] [] [] [] {ι : Sort u_6} [] {f : ιδα} {g : δα} (hf : ∀ (i : ι), Measurable (f i)) (hg : ∀ (b : δ), IsGLB {a : α | ∃ (i : ι), f i b = a} (g b)) :

If a function is the greatest lower bound of countably many measurable functions, then it is measurable.

theorem Measurable.isGLB_of_mem {α : Type u_1} {δ : Type u_5} [] [] [] [] [] [] {ι : Sort u_6} [] {f : ιδα} {g : δα} {g' : δα} (hf : ∀ (i : ι), Measurable (f i)) {s : Set δ} (hs : ) (hg : bs, IsGLB {a : α | ∃ (i : ι), f i b = a} (g b)) (hg' : Set.EqOn g g' s) (g'_meas : ) :

If a function is the greatest lower bound of countably many measurable functions on a measurable set s, and coincides with a measurable function outside of s, then it is measurable.

theorem AEMeasurable.isGLB {α : Type u_1} {δ : Type u_5} [] [] [] [] [] [] {ι : Sort u_6} {μ : } [] {f : ιδα} {g : δα} (hf : ∀ (i : ι), AEMeasurable (f i) μ) (hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a : α | ∃ (i : ι), f i b = a} (g b)) :
theorem Monotone.measurable {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] [] [] [] {f : βα} (hf : ) :
theorem aemeasurable_restrict_of_monotoneOn {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] [] [] [] {μ : } {s : Set β} (hs : ) {f : βα} (hf : ) :
AEMeasurable f (μ.restrict s)
theorem Antitone.measurable {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] [] [] [] {f : βα} (hf : ) :
theorem aemeasurable_restrict_of_antitoneOn {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] [] [] [] {μ : } {s : Set β} (hs : ) {f : βα} (hf : ) :
AEMeasurable f (μ.restrict s)
theorem measurableSet_of_mem_nhdsWithin_Ioi_aux {α : Type u_1} [] [] [] [] [] {s : Set α} (h : xs, s nhdsWithin x ()) (h' : xs, ∃ (y : α), x < y) :
theorem measurableSet_of_mem_nhdsWithin_Ioi {α : Type u_1} [] [] [] [] [] {s : Set α} (h : xs, s nhdsWithin x ()) :

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

theorem measurableSet_bddAbove_range {α : Type u_1} {δ : Type u_5} [] [] [] [] [] [] {ι : Sort u_6} [] {f : ιδα} (hf : ∀ (i : ι), Measurable (f i)) :
MeasurableSet {b : δ | BddAbove (Set.range fun (i : ι) => f i b)}
theorem measurableSet_bddBelow_range {α : Type u_1} {δ : Type u_5} [] [] [] [] [] [] {ι : Sort u_6} [] {f : ιδα} (hf : ∀ (i : ι), Measurable (f i)) :
MeasurableSet {b : δ | BddBelow (Set.range fun (i : ι) => f i b)}
theorem Measurable.iSup_Prop {δ : Type u_5} [] {α : Type u_6} [] (p : Prop) {f : δα} (hf : ) :
Measurable fun (b : δ) => ⨆ (_ : p), f b
theorem Measurable.iInf_Prop {δ : Type u_5} [] {α : Type u_6} [] (p : Prop) {f : δα} (hf : ) :
Measurable fun (b : δ) => ⨅ (_ : p), f b
theorem measurable_iSup {α : Type u_1} {δ : Type u_5} [] [] [] [] [] {ι : Sort u_6} [] {f : ιδα} (hf : ∀ (i : ι), Measurable (f i)) :
Measurable fun (b : δ) => ⨆ (i : ι), f i b
theorem aemeasurable_iSup {α : Type u_1} {δ : Type u_5} [] [] [] [] [] {ι : Sort u_6} {μ : } [] {f : ιδα} (hf : ∀ (i : ι), AEMeasurable (f i) μ) :
AEMeasurable (fun (b : δ) => ⨆ (i : ι), f i b) μ
theorem measurable_iInf {α : Type u_1} {δ : Type u_5} [] [] [] [] [] {ι : Sort u_6} [] {f : ιδα} (hf : ∀ (i : ι), Measurable (f i)) :
Measurable fun (b : δ) => ⨅ (i : ι), f i b
theorem aemeasurable_iInf {α : Type u_1} {δ : Type u_5} [] [] [] [] [] {ι : Sort u_6} {μ : } [] {f : ιδα} (hf : ∀ (i : ι), AEMeasurable (f i) μ) :
AEMeasurable (fun (b : δ) => ⨅ (i : ι), f i b) μ
theorem measurable_sSup {α : Type u_1} {δ : Type u_5} [] [] [] [] [] {ι : Type u_6} {f : ιδα} {s : Set ι} (hs : ) (hf : is, Measurable (f i)) :
Measurable fun (x : δ) => sSup ((fun (i : ι) => f i x) '' s)
theorem measurable_sInf {α : Type u_1} {δ : Type u_5} [] [] [] [] [] {ι : Type u_6} {f : ιδα} {s : Set ι} (hs : ) (hf : is, Measurable (f i)) :
Measurable fun (x : δ) => sInf ((fun (i : ι) => f i x) '' s)
theorem measurable_biSup {α : Type u_1} {δ : Type u_5} [] [] [] [] [] {ι : Type u_6} (s : Set ι) {f : ιδα} (hs : ) (hf : is, Measurable (f i)) :
Measurable fun (b : δ) => ⨆ i ∈ s, f i b
theorem aemeasurable_biSup {α : Type u_1} {δ : Type u_5} [] [] [] [] [] {ι : Type u_6} {μ : } (s : Set ι) {f : ιδα} (hs : ) (hf : is, AEMeasurable (f i) μ) :
AEMeasurable (fun (b : δ) => ⨆ i ∈ s, f i b) μ
theorem measurable_biInf {α : Type u_1} {δ : Type u_5} [] [] [] [] [] {ι : Type u_6} (s : Set ι) {f : ιδα} (hs : ) (hf : is, Measurable (f i)) :
Measurable fun (b : δ) => ⨅ i ∈ s, f i b
theorem aemeasurable_biInf {α : Type u_1} {δ : Type u_5} [] [] [] [] [] {ι : Type u_6} {μ : } (s : Set ι) {f : ιδα} (hs : ) (hf : is, AEMeasurable (f i) μ) :
AEMeasurable (fun (b : δ) => ⨅ i ∈ s, f i b) μ
theorem measurable_liminf' {α : Type u_1} {δ : Type u_5} [] [] [] [] [] {ι : Type u_6} {ι' : Type u_7} {f : ιδα} {v : } (hf : ∀ (i : ι), Measurable (f i)) {p : ι'Prop} {s : ι'Set ι} (hv : ) (hs : ∀ (j : ι'), Set.Countable (s j)) :
Measurable fun (x : δ) => Filter.liminf (fun (x_1 : ι) => f x_1 x) v

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

theorem measurable_limsup' {α : Type u_1} {δ : Type u_5} [] [] [] [] [] {ι : Type u_6} {ι' : Type u_7} {f : ιδα} {u : } (hf : ∀ (i : ι), Measurable (f i)) {p : ι'Prop} {s : ι'Set ι} (hu : ) (hs : ∀ (i : ι'), Set.Countable (s i)) :
Measurable fun (x : δ) => Filter.limsup (fun (i : ι) => f i x) u

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

theorem measurable_liminf {α : Type u_1} {δ : Type u_5} [] [] [] [] [] {f : δα} (hf : ∀ (i : ), Measurable (f i)) :
Measurable fun (x : δ) => Filter.liminf (fun (i : ) => f i x) Filter.atTop

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

theorem measurable_limsup {α : Type u_1} {δ : Type u_5} [] [] [] [] [] {f : δα} (hf : ∀ (i : ), Measurable (f i)) :
Measurable fun (x : δ) => Filter.limsup (fun (i : ) => f i x) Filter.atTop

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

def Homemorph.toMeasurableEquiv {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] (h : α ≃ₜ β) :
α ≃ᵐ β

Convert a Homeomorph to a MeasurableEquiv.

Equations
• = { toEquiv := h.toEquiv, measurable_toFun := , measurable_invFun := }
Instances For
theorem IsFiniteMeasureOnCompacts.map {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] (μ : ) (f : α ≃ₜ β) :
instance Empty.borelSpace :
Equations
instance Unit.borelSpace :
Equations
instance Bool.borelSpace :
Equations
instance Nat.borelSpace :
Equations
instance Int.borelSpace :
Equations
instance Rat.borelSpace :
Equations
Equations
instance Real.borelSpace :
Equations
Equations
Equations
Equations
Equations
Equations
instance EReal.borelSpace :
Equations
theorem measure_eq_measure_preimage_add_measure_tsum_Ico_zpow {α : Type u_1} [] (μ : ) {f : αENNReal} (hf : ) {s : Set α} (hs : ) {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.

theorem measurableSet_ball {α : Type u_1} [] {x : α} {ε : } :
theorem measurableSet_closedBall {α : Type u_1} [] {x : α} {ε : } :
theorem measurable_infDist {α : Type u_1} [] {s : Set α} :
Measurable fun (x : α) =>
theorem Measurable.infDist {α : Type u_1} {β : Type u_2} [] [] {f : βα} (hf : ) {s : Set α} :
Measurable fun (x : β) => Metric.infDist (f x) s
theorem measurable_infNndist {α : Type u_1} [] {s : Set α} :
Measurable fun (x : α) =>
theorem Measurable.infNndist {α : Type u_1} {β : Type u_2} [] [] {f : βα} (hf : ) {s : Set α} :
Measurable fun (x : β) => Metric.infNndist (f x) s
theorem measurable_dist {α : Type u_1} [] :
Measurable fun (p : α × α) => dist p.1 p.2
theorem Measurable.dist {α : Type u_1} {β : Type u_2} [] [] {f : βα} {g : βα} (hf : ) (hg : ) :
Measurable fun (b : β) => dist (f b) (g b)
theorem measurable_nndist {α : Type u_1} [] :
Measurable fun (p : α × α) => nndist p.1 p.2
theorem Measurable.nndist {α : Type u_1} {β : Type u_2} [] [] {f : βα} {g : βα} (hf : ) (hg : ) :
Measurable fun (b : β) => nndist (f b) (g b)
theorem measurableSet_eball {α : Type u_1} [] {x : α} {ε : ENNReal} :
theorem measurable_edist_right {α : Type u_1} [] {x : α} :
theorem measurable_edist_left {α : Type u_1} [] {x : α} :
Measurable fun (y : α) => edist y x
theorem measurable_infEdist {α : Type u_1} [] {s : Set α} :
Measurable fun (x : α) =>
theorem Measurable.infEdist {α : Type u_1} {β : Type u_2} [] [] {f : βα} (hf : ) {s : Set α} :
Measurable fun (x : β) => EMetric.infEdist (f x) s
theorem tendsto_measure_cthickening {α : Type u_1} [] {μ : } {s : Set α} (hs : ∃ R > 0, μ () ) :
Filter.Tendsto (fun (r : ) => μ ()) (nhds 0) (nhds (μ ()))

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_isClosed {α : Type u_1} [] {μ : } {s : Set α} (hs : ∃ R > 0, μ () ) (h's : ) :
Filter.Tendsto (fun (r : ) => μ ()) (nhds 0) (nhds (μ s))

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

theorem tendsto_measure_thickening {α : Type u_1} [] {μ : } {s : Set α} (hs : ∃ R > 0, μ () ) :
Filter.Tendsto (fun (r : ) => μ ()) (nhdsWithin 0 ()) (nhds (μ ()))

If a set has a thickening with finite measure, then the measures of its r-thickenings converge to the measure of its closure as r > 0 tends to 0.

theorem tendsto_measure_thickening_of_isClosed {α : Type u_1} [] {μ : } {s : Set α} (hs : ∃ R > 0, μ () ) (h's : ) :
Filter.Tendsto (fun (r : ) => μ ()) (nhdsWithin 0 ()) (nhds (μ s))

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

theorem measurable_edist {α : Type u_1} [] :
Measurable fun (p : α × α) => edist p.1 p.2
theorem Measurable.edist {α : Type u_1} {β : Type u_2} [] [] {f : βα} {g : βα} (hf : ) (hg : ) :
Measurable fun (b : β) => edist (f b) (g b)
theorem AEMeasurable.edist {α : Type u_1} {β : Type u_2} [] [] {f : βα} {g : βα} {μ : } (hf : ) (hg : ) :
AEMeasurable (fun (a : β) => edist (f a) (g a)) μ
theorem tendsto_measure_cthickening_of_isCompact {α : Type u_1} [] [] [] {μ : } {s : Set α} (hs : ) :
Filter.Tendsto (fun (r : ) => μ ()) (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.

theorem exists_borelSpace_of_countablyGenerated_of_separatesPoints (α : Type u_6) [m : ] :
∃ (τ : ),

If a measurable space is countably generated and separates points, it arises as the borel sets of some second countable t4 topology (i.e. a separable metrizable one).

theorem exists_opensMeasurableSpace_of_hasCountableSeparatingOn (α : Type u_6) [m : ] [HasCountableSeparatingOn α MeasurableSet Set.univ] :
∃ (τ : ),

If a measurable space on α is countably generated and separates points, there is some second countable t4 topology on α (i.e. a separable metrizable one) for which every open set is measurable.

theorem Real.borel_eq_generateFrom_Ioo_rat :
= MeasurableSpace.generateFrom (⋃ (a : ), ⋃ (b : ), ⋃ (_ : a < b), {Set.Ioo a b})
theorem Real.isPiSystem_Ioo_rat :
IsPiSystem (⋃ (a : ), ⋃ (b : ), ⋃ (_ : a < b), {Set.Ioo a b})
def Real.finiteSpanningSetsInIooRat (μ : ) :
MeasureTheory.Measure.FiniteSpanningSetsIn μ (⋃ (a : ), ⋃ (b : ), ⋃ (_ : 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
• One or more equations did not get rendered due to their size.
Instances For
theorem Real.measure_ext_Ioo_rat {μ : } {ν : } (h : ∀ (a b : ), μ (Set.Ioo a b) = ν (Set.Ioo a b)) :
μ = ν
theorem Measurable.real_toNNReal {α : Type u_1} [] {f : α} (hf : ) :
Measurable fun (x : α) => Real.toNNReal (f x)
theorem AEMeasurable.real_toNNReal {α : Type u_1} [] {f : α} {μ : } (hf : ) :
AEMeasurable (fun (x : α) => Real.toNNReal (f x)) μ
theorem Measurable.coe_nnreal_real {α : Type u_1} [] {f : αNNReal} (hf : ) :
Measurable fun (x : α) => (f x)
theorem AEMeasurable.coe_nnreal_real {α : Type u_1} [] {f : αNNReal} {μ : } (hf : ) :
AEMeasurable (fun (x : α) => (f x)) μ
theorem Measurable.coe_nnreal_ennreal {α : Type u_1} [] {f : αNNReal} (hf : ) :
Measurable fun (x : α) => (f x)
theorem AEMeasurable.coe_nnreal_ennreal {α : Type u_1} [] {f : αNNReal} {μ : } (hf : ) :
AEMeasurable (fun (x : α) => (f x)) μ
theorem Measurable.ennreal_ofReal {α : Type u_1} [] {f : α} (hf : ) :
Measurable fun (x : α) => ENNReal.ofReal (f x)
theorem AEMeasurable.ennreal_ofReal {α : Type u_1} [] {f : α} {μ : } (hf : ) :
AEMeasurable (fun (x : α) => ENNReal.ofReal (f x)) μ
@[simp]
theorem measurable_coe_nnreal_real_iff {α : Type u_1} [] {f : αNNReal} :
(Measurable fun (x : α) => (f x))
@[simp]
theorem aemeasurable_coe_nnreal_real_iff {α : Type u_1} [] {f : αNNReal} {μ : } :
AEMeasurable (fun (x : α) => (f x)) μ
@[deprecated aemeasurable_coe_nnreal_real_iff]
theorem aEMeasurable_coe_nnreal_real_iff {α : Type u_1} [] {f : αNNReal} {μ : } :
AEMeasurable (fun (x : α) => (f x)) μ

Alias of aemeasurable_coe_nnreal_real_iff.

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

Equations
Instances For
theorem ENNReal.measurable_of_measurable_nnreal {α : Type u_1} [] {f : ENNRealα} (h : Measurable fun (p : NNReal) => f p) :

ℝ≥0∞ is MeasurableEquiv to ℝ≥0 ⊕ Unit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem ENNReal.measurable_of_measurable_nnreal_prod {β : Type u_2} {γ : Type u_3} [] [] {f : γ} (H₁ : Measurable fun (p : ) => f (p.1, p.2)) (H₂ : Measurable fun (x : β) => f (, x)) :
theorem ENNReal.measurable_of_measurable_nnreal_nnreal {β : Type u_2} [] {f : β} (h₁ : Measurable fun (p : ) => f (p.1, p.2)) (h₂ : Measurable fun (r : NNReal) => f (, r)) (h₃ : Measurable fun (r : NNReal) => f (r, )) :
Equations
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
theorem ENNReal.measurable_of_tendsto' {α : Type u_1} [] {ι : Type u_6} {f : ιαENNReal} {g : αENNReal} (u : ) [] (hf : ∀ (i : ι), Measurable (f i)) (lim : Filter.Tendsto f u (nhds g)) :

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

@[deprecated ENNReal.measurable_of_tendsto']
theorem measurable_of_tendsto_ennreal' {α : Type u_1} [] {ι : Type u_6} {f : ιαENNReal} {g : αENNReal} (u : ) [] (hf : ∀ (i : ι), Measurable (f i)) (lim : Filter.Tendsto f u (nhds g)) :

Alias of ENNReal.measurable_of_tendsto'.

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

theorem ENNReal.measurable_of_tendsto {α : Type u_1} [] {f : αENNReal} {g : αENNReal} (hf : ∀ (i : ), Measurable (f i)) (lim : Filter.Tendsto f Filter.atTop (nhds g)) :

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

@[deprecated ENNReal.measurable_of_tendsto]
theorem measurable_of_tendsto_ennreal {α : Type u_1} [] {f : αENNReal} {g : αENNReal} (hf : ∀ (i : ), Measurable (f i)) (lim : Filter.Tendsto f Filter.atTop (nhds g)) :

Alias of ENNReal.measurable_of_tendsto.

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

theorem ENNReal.aemeasurable_of_tendsto' {α : Type u_1} [] {ι : Type u_6} {f : ιαENNReal} {g : αENNReal} {μ : } (u : ) [] (hf : ∀ (i : ι), AEMeasurable (f i) μ) (hlim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (i : ι) => f i a) u (nhds (g a))) :

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

theorem ENNReal.aemeasurable_of_tendsto {α : Type u_1} [] {f : αENNReal} {g : αENNReal} {μ : } (hf : ∀ (i : ), AEMeasurable (f i) μ) (hlim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (i : ) => f i a) Filter.atTop (nhds (g a))) :

A limit of a.e.-measurable ℝ≥0∞ valued functions is a.e.-measurable.

theorem Measurable.ennreal_toNNReal {α : Type u_1} [] {f : αENNReal} (hf : ) :
Measurable fun (x : α) => (f x).toNNReal
theorem AEMeasurable.ennreal_toNNReal {α : Type u_1} [] {f : αENNReal} {μ : } (hf : ) :
AEMeasurable (fun (x : α) => (f x).toNNReal) μ
@[simp]
theorem measurable_coe_nnreal_ennreal_iff {α : Type u_1} [] {f : αNNReal} :
(Measurable fun (x : α) => (f x))
@[simp]
theorem aemeasurable_coe_nnreal_ennreal_iff {α : Type u_1} [] {f : αNNReal} {μ : } :
AEMeasurable (fun (x : α) => (f x)) μ
theorem Measurable.ennreal_toReal {α : Type u_1} [] {f : αENNReal} (hf : ) :
Measurable fun (x : α) => (f x).toReal
theorem AEMeasurable.ennreal_toReal {α : Type u_1} [] {f : αENNReal} {μ : } (hf : ) :
AEMeasurable (fun (x : α) => (f x).toReal) μ
theorem Measurable.ennreal_tsum {α : Type u_1} [] {ι : Type u_6} [] {f : ιαENNReal} (h : ∀ (i : ι), Measurable (f i)) :
Measurable fun (x : α) => ∑' (i : ι), f i x

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

theorem Measurable.ennreal_tsum' {α : Type u_1} [] {ι : Type u_6} [] {f : ιαENNReal} (h : ∀ (i : ι), Measurable (f i)) :
Measurable (∑' (i : ι), f i)
theorem Measurable.nnreal_tsum {α : Type u_1} [] {ι : Type u_6} [] {f : ιαNNReal} (h : ∀ (i : ι), Measurable (f i)) :
Measurable fun (x : α) => ∑' (i : ι), f i x
theorem AEMeasurable.ennreal_tsum {α : Type u_1} [] {ι : Type u_6} [] {f : ιαENNReal} {μ : } (h : ∀ (i : ι), AEMeasurable (f i) μ) :
AEMeasurable (fun (x : α) => ∑' (i : ι), f i x) μ
theorem AEMeasurable.nnreal_tsum {α : Type u_6} [] {ι : Type u_7} [] {f : ιαNNReal} {μ : } (h : ∀ (i : ι), AEMeasurable (f i) μ) :
AEMeasurable (fun (x : α) => ∑' (i : ι), f i x) μ
theorem Measurable.coe_real_ereal {α : Type u_1} [] {f : α} (hf : ) :
Measurable fun (x : α) => (f x)
theorem AEMeasurable.coe_real_ereal {α : Type u_1} [] {f : α} {μ : } (hf : ) :
AEMeasurable (fun (x : α) => (f x)) μ

The set of finite EReal numbers is MeasurableEquiv to ℝ.

Equations
Instances For
theorem EReal.measurable_of_measurable_real {α : Type u_1} [] {f : ERealα} (h : Measurable fun (p : ) => f p) :
theorem Measurable.ereal_toReal {α : Type u_1} [] {f : αEReal} (hf : ) :
Measurable fun (x : α) => EReal.toReal (f x)
theorem AEMeasurable.ereal_toReal {α : Type u_1} [] {f : αEReal} {μ : } (hf : ) :
AEMeasurable (fun (x : α) => EReal.toReal (f x)) μ
theorem Measurable.coe_ereal_ennreal {α : Type u_1} [] {f : αENNReal} (hf : ) :
Measurable fun (x : α) => (f x)
theorem AEMeasurable.coe_ereal_ennreal {α : Type u_1} [] {f : αENNReal} {μ : } (hf : ) :
AEMeasurable (fun (x : α) => (f x)) μ
theorem NNReal.measurable_of_tendsto' {α : Type u_1} [] {ι : Type u_6} {f : ιαNNReal} {g : αNNReal} (u : ) [] (hf : ∀ (i : ι), Measurable (f i)) (lim : Filter.Tendsto f u (nhds g)) :

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

@[deprecated NNReal.measurable_of_tendsto']
theorem measurable_of_tendsto_nnreal' {α : Type u_1} [] {ι : Type u_6} {f : ιαNNReal} {g : αNNReal} (u : ) [] (hf : ∀ (i : ι), Measurable (f i)) (lim : Filter.Tendsto f u (nhds g)) :

Alias of NNReal.measurable_of_tendsto'.

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

theorem NNReal.measurable_of_tendsto {α : Type u_1} [] {f : αNNReal} {g : αNNReal} (hf : ∀ (i : ), Measurable (f i)) (lim : Filter.Tendsto f Filter.atTop (nhds g)) :

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

@[deprecated NNReal.measurable_of_tendsto]
theorem measurable_of_tendsto_nnreal {α : Type u_1} [] {f : αNNReal} {g : αNNReal} (hf : ∀ (i : ), Measurable (f i)) (lim : Filter.Tendsto f Filter.atTop (nhds g)) :

Alias of NNReal.measurable_of_tendsto.

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

theorem exists_spanning_measurableSet_le {α : Type u_1} {m : } {f : αNNReal} (hf : ) (μ : ) :
∃ (s : Set α), (∀ (n : ), MeasurableSet (s n) μ (s n) < xs n, f x n) ⋃ (i : ), s i = Set.univ

If a function f : α → ℝ≥0 is measurable and the measure is σ-finite, then there exists spanning measurable sets with finite measure on which f is bounded. See also StronglyMeasurable.exists_spanning_measurableSet_norm_le for functions into normed groups.

theorem measurable_norm {α : Type u_1} [] :
theorem Measurable.norm {α : Type u_1} {β : Type u_2} [] [] {f : βα} (hf : ) :
Measurable fun (a : β) => f a
theorem AEMeasurable.norm {α : Type u_1} {β : Type u_2} [] [] {f : βα} {μ : } (hf : ) :
AEMeasurable (fun (a : β) => f a) μ
theorem measurable_nnnorm {α : Type u_1} [] :
Measurable nnnorm
theorem Measurable.nnnorm {α : Type u_1} {β : Type u_2} [] [] {f : βα} (hf : ) :
Measurable fun (a : β) => f a‖₊
theorem AEMeasurable.nnnorm {α : Type u_1} {β : Type u_2} [] [] {f : βα} {μ : } (hf : ) :
AEMeasurable (fun (a : β) => f a‖₊) μ
theorem measurable_ennnorm {α : Type u_1} [] :
Measurable fun (x : α) => x‖₊
theorem Measurable.ennnorm {α : Type u_1} {β : Type u_2} [] [] {f : βα} (hf : ) :
Measurable fun (a : β) => f a‖₊
theorem AEMeasurable.ennnorm {α : Type u_1} {β : Type u_2} [] [] {f : βα} {μ : } (hf : ) :
AEMeasurable (fun (a : β) => f a‖₊) μ