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) [TopologicalSpace α] : MeasurableSpace α

MeasurableSpace structure generated by TopologicalSpace.

Equations

• borel α = MeasurableSpace.generateFrom {s : Set α | IsOpen s}

theorem borel_anti {α : Type u_1} : Antitone (@borel α)

theorem borel_eq_top_of_discrete {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] : borel α = ⊤

theorem borel_eq_top_of_countable {α : Type u_1} [TopologicalSpace α] [T1Space α] [Countable α] : borel α = ⊤

theorem borel_eq_generateFrom_of_subbasis {α : Type u_1} {s : Set (Set α)} [t : TopologicalSpace α] [SecondCountableTopology α] (hs : t = TopologicalSpace.generateFrom s) : borel α = MeasurableSpace.generateFrom s

theorem TopologicalSpace.IsTopologicalBasis.borel_eq_generateFrom {α : Type u_1} [TopologicalSpace α] [SecondCountableTopology α] {s : Set (Set α)} (hs : TopologicalSpace.IsTopologicalBasis s) : borel α = MeasurableSpace.generateFrom s

theorem isPiSystem_isOpen {α : Type u_1} [TopologicalSpace α] : IsPiSystem {s : Set α | IsOpen s}

theorem isPiSystem_isClosed {α : Type u_1} [TopologicalSpace α] : IsPiSystem {s : Set α | IsClosed s}

theorem borel_eq_generateFrom_isClosed {α : Type u_1} [TopologicalSpace α] : borel α = MeasurableSpace.generateFrom {s : Set α | IsClosed s}

theorem borel_eq_generateFrom_Iio (α : Type u_1) [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] : borel α = MeasurableSpace.generateFrom (Set.range Set.Iio)

theorem borel_eq_generateFrom_Ioi (α : Type u_1) [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] : borel α = MeasurableSpace.generateFrom (Set.range Set.Ioi)

theorem borel_eq_generateFrom_Iic (α : Type u_1) [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] : borel α = MeasurableSpace.generateFrom (Set.range Set.Iic)

theorem borel_eq_generateFrom_Ici (α : Type u_1) [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] : borel α = MeasurableSpace.generateFrom (Set.range Set.Ici)

theorem borel_comap {α : Type u_1} {β : Type u_2} {f : α → β} {t : TopologicalSpace β} : borel α = MeasurableSpace.comap f (borel β)

theorem Continuous.borel_measurable {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Continuous f) : Measurable f

class OpensMeasurableSpace (α : Type u_6) [TopologicalSpace α] [h : MeasurableSpace α] : Prop

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

• borel_le : borel α ≤ h

  Borel-measurable sets are measurable.

class BorelSpace (α : Type u_6) [TopologicalSpace α] [MeasurableSpace α] : Prop

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✝ = borel α

  The measurable sets are exactly the Borel-measurable sets.

def Mathlib.Tactic.Borelize.tacticBorelize___ : Lean.ParserDescr

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.

def Mathlib.Tactic.Borelize.addBorelInstance (e : Lean.Expr) : Lean.Elab.Tactic.TacticM Unit

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

Equations

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

def Mathlib.Tactic.Borelize.borelToRefl (e : Lean.Expr) (i : Lean.FVarId) : Lean.Elab.Tactic.TacticM Unit

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.

def Mathlib.Tactic.Borelize.borelize (t : Lean.Term) : Lean.Elab.Tactic.TacticM Unit

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.

instance OrderDual.opensMeasurableSpace {α : Type u_6} [TopologicalSpace α] [MeasurableSpace α] [h : OpensMeasurableSpace α] : OpensMeasurableSpace αᵒᵈ

Equations

• ⋯ = ⋯

instance OrderDual.borelSpace {α : Type u_6} [TopologicalSpace α] [MeasurableSpace α] [h : BorelSpace α] : BorelSpace αᵒᵈ

Equations

• ⋯ = ⋯

instance BorelSpace.opensMeasurable {α : Type u_6} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] : OpensMeasurableSpace α

In a BorelSpace all open sets are measurable.

Equations

• ⋯ = ⋯

instance Subtype.borelSpace {α : Type u_6} [TopologicalSpace α] [MeasurableSpace α] [hα : BorelSpace α] (s : Set α) : BorelSpace ↑s

Equations

• ⋯ = ⋯

instance Countable.instBorelSpace {α : Type u_1} [Countable α] [MeasurableSpace α] [MeasurableSingletonClass α] [TopologicalSpace α] [DiscreteTopology α] : BorelSpace α

Equations

• ⋯ = ⋯

instance Subtype.opensMeasurableSpace {α : Type u_6} [TopologicalSpace α] [MeasurableSpace α] [h : OpensMeasurableSpace α] (s : Set α) : OpensMeasurableSpace ↑s

Equations

• ⋯ = ⋯

theorem opensMeasurableSpace_iff_forall_measurableSet {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] : OpensMeasurableSpace α ↔ ∀ (s : Set α), IsOpen s → MeasurableSet s

instance BorelSpace.countablyGenerated {α : Type u_6} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] : MeasurableSpace.CountablyGenerated α

Equations

• ⋯ = ⋯

theorem MeasurableSet.induction_on_open {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] {C : Set α → Prop} (h_open : ∀ (U : Set α), IsOpen U → C U) (h_compl : ∀ (t : Set α), MeasurableSet t → C t → C tᶜ) (h_union : ∀ (f : ℕ → Set α), Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ (i : ℕ), f i)) ⦃t : Set α⦄ : MeasurableSet t → C t

theorem IsOpen.measurableSet {α : Type u_1} {s : Set α} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] (h : IsOpen s) : MeasurableSet s

instance instHasCountableSeparatingOnMeasurableSet {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {s : Set α} [HasCountableSeparatingOn α IsOpen s] : HasCountableSeparatingOn α MeasurableSet s

Equations

• ⋯ = ⋯

theorem measurableSet_interior {α : Type u_1} {s : Set α} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] : MeasurableSet (interior s)

theorem IsGδ.measurableSet {α : Type u_1} {s : Set α} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] (h : IsGδ s) : MeasurableSet s

theorem measurableSet_of_continuousAt {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {β : Type u_6} [EMetricSpace β] (f : α → β) : MeasurableSet {x : α | ContinuousAt f x}

theorem IsClosed.measurableSet {α : Type u_1} {s : Set α} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] (h : IsClosed s) : MeasurableSet s

theorem IsCompact.measurableSet {α : Type u_1} {s : Set α} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [T2Space α] (h : IsCompact s) : MeasurableSet s

theorem Inseparable.mem_measurableSet_iff {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] {x : γ} {y : γ} (h : Inseparable x y) {s : Set γ} (hs : MeasurableSet s) : 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} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [R1Space γ] {K : Set γ} {s : Set γ} (hK : IsCompact K) (hs : MeasurableSet s) (hKs : K ⊆ s) : closure K ⊆ 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} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [R1Space γ] {K : Set γ} (hK : IsCompact K) (μ : MeasureTheory.Measure γ) : ↑↑μ (closure K) = ↑↑μ 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 α} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] : MeasurableSet (closure s)

theorem measurable_of_isOpen {γ : Type u_3} {δ : Type u_5} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [MeasurableSpace δ] {f : δ → γ} (hf : ∀ (s : Set γ), IsOpen s → MeasurableSet (f ⁻¹' s)) : Measurable f

theorem measurable_of_isClosed {γ : Type u_3} {δ : Type u_5} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [MeasurableSpace δ] {f : δ → γ} (hf : ∀ (s : Set γ), IsClosed s → MeasurableSet (f ⁻¹' s)) : Measurable f

theorem measurable_of_isClosed' {γ : Type u_3} {δ : Type u_5} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [MeasurableSpace δ] {f : δ → γ} (hf : ∀ (s : Set γ), IsClosed s → Set.Nonempty s → s ≠ Set.univ → MeasurableSet (f ⁻¹' s)) : Measurable f

instance nhds_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] (a : α) : Filter.IsMeasurablyGenerated (nhds a)

Equations

• ⋯ = ⋯

theorem MeasurableSet.nhdsWithin_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {s : Set α} (hs : MeasurableSet s) (a : α) : Filter.IsMeasurablyGenerated (nhdsWithin a s)

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.toMeasurableSingletonClass {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [T1Space α] : MeasurableSingletonClass α

Equations

• ⋯ = ⋯

instance Pi.opensMeasurableSpace {ι : Type u_6} {π : ι → Type u_7} [Countable ι] [t' : (i : ι) → TopologicalSpace (π i)] [(i : ι) → MeasurableSpace (π i)] [∀ (i : ι), SecondCountableTopology (π i)] [∀ (i : ι), OpensMeasurableSpace (π i)] : OpensMeasurableSpace ((i : ι) → π i)

Equations

• ⋯ = ⋯

class SecondCountableTopologyEither (α : Type u_6) (β : Type u_7) [TopologicalSpace α] [TopologicalSpace β] : Prop

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.

• out : SecondCountableTopology α ∨ SecondCountableTopology β

  The projection out of SecondCountableTopologyEither

instance secondCountableTopologyEither_of_left (α : Type u_6) (β : Type u_7) [TopologicalSpace α] [TopologicalSpace β] [SecondCountableTopology α] : SecondCountableTopologyEither α β

Equations

• ⋯ = ⋯

instance secondCountableTopologyEither_of_right (α : Type u_6) (β : Type u_7) [TopologicalSpace α] [TopologicalSpace β] [SecondCountableTopology β] : SecondCountableTopologyEither α β

Equations

• ⋯ = ⋯

instance Prod.opensMeasurableSpace {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace β] [MeasurableSpace β] [OpensMeasurableSpace β] [h : SecondCountableTopologyEither α β] : OpensMeasurableSpace (α × β)

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} [TopologicalSpace α'] [MeasurableSpace α'] {μ : MeasureTheory.Measure α'} {s : Set α'} (h : ↑↑μ (frontier s) = 0) : interior s =ᶠ[MeasureTheory.Measure.ae μ] s

theorem measure_interior_of_null_frontier {α' : Type u_6} [TopologicalSpace α'] [MeasurableSpace α'] {μ : MeasureTheory.Measure α'} {s : Set α'} (h : ↑↑μ (frontier s) = 0) : ↑↑μ (interior s) = ↑↑μ s

theorem nullMeasurableSet_of_null_frontier {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {s : Set α} {μ : MeasureTheory.Measure α} (h : ↑↑μ (frontier s) = 0) : MeasureTheory.NullMeasurableSet s μ

theorem closure_ae_eq_of_null_frontier {α' : Type u_6} [TopologicalSpace α'] [MeasurableSpace α'] {μ : MeasureTheory.Measure α'} {s : Set α'} (h : ↑↑μ (frontier s) = 0) : closure s =ᶠ[MeasureTheory.Measure.ae μ] s

theorem measure_closure_of_null_frontier {α' : Type u_6} [TopologicalSpace α'] [MeasurableSpace α'] {μ : MeasureTheory.Measure α'} {s : Set α'} (h : ↑↑μ (frontier s) = 0) : ↑↑μ (closure s) = ↑↑μ s

@[simp]

theorem measurableSet_Ici {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [Preorder α] [OrderClosedTopology α] {a : α} : MeasurableSet (Set.Ici a)

@[simp]

theorem measurableSet_Iic {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [Preorder α] [OrderClosedTopology α] {a : α} : MeasurableSet (Set.Iic a)

@[simp]

theorem measurableSet_Icc {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [Preorder α] [OrderClosedTopology α] {a : α} {b : α} : MeasurableSet (Set.Icc a b)

instance nhdsWithin_Ici_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [Preorder α] [OrderClosedTopology α] {a : α} {b : α} : Filter.IsMeasurablyGenerated (nhdsWithin a (Set.Ici b))

Equations

• ⋯ = ⋯

instance nhdsWithin_Iic_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [Preorder α] [OrderClosedTopology α] {a : α} {b : α} : Filter.IsMeasurablyGenerated (nhdsWithin a (Set.Iic b))

Equations

• ⋯ = ⋯

instance nhdsWithin_Icc_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [Preorder α] [OrderClosedTopology α] {a : α} {b : α} {x : α} : Filter.IsMeasurablyGenerated (nhdsWithin x (Set.Icc a b))

Equations

• ⋯ = ⋯

instance atTop_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [Preorder α] [OrderClosedTopology α] : Filter.IsMeasurablyGenerated Filter.atTop

Equations

• ⋯ = ⋯

instance atBot_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [Preorder α] [OrderClosedTopology α] : Filter.IsMeasurablyGenerated Filter.atBot

Equations

• ⋯ = ⋯

instance instIsMeasurablyGeneratedCocompact {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [R1Space α] : Filter.IsMeasurablyGenerated (Filter.cocompact α)

Equations

• ⋯ = ⋯

theorem measurableSet_le' {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [PartialOrder α] [OrderClosedTopology α] [SecondCountableTopology α] : MeasurableSet {p : α × α | p.1 ≤ p.2}

theorem measurableSet_le {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [PartialOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f : δ → α} {g : δ → α} (hf : Measurable f) (hg : Measurable g) : MeasurableSet {a : δ | f a ≤ g a}

@[simp]

theorem measurableSet_Iio {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} : MeasurableSet (Set.Iio a)

@[simp]

theorem measurableSet_Ioi {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} : MeasurableSet (Set.Ioi a)

@[simp]

theorem measurableSet_Ioo {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} : MeasurableSet (Set.Ioo a b)

@[simp]

theorem measurableSet_Ioc {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} : MeasurableSet (Set.Ioc a b)

@[simp]

theorem measurableSet_Ico {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} : MeasurableSet (Set.Ico a b)

instance nhdsWithin_Ioi_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} : Filter.IsMeasurablyGenerated (nhdsWithin a (Set.Ioi b))

Equations

• ⋯ = ⋯

instance nhdsWithin_Iio_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} : Filter.IsMeasurablyGenerated (nhdsWithin a (Set.Iio b))

Equations

• ⋯ = ⋯

instance nhdsWithin_uIcc_isMeasurablyGenerated {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} {x : α} : Filter.IsMeasurablyGenerated (nhdsWithin x (Set.uIcc a b))

Equations

• ⋯ = ⋯

theorem measurableSet_lt' {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] : MeasurableSet {p : α × α | p.1 < p.2}

theorem measurableSet_lt {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f : δ → α} {g : δ → α} (hf : Measurable f) (hg : Measurable g) : MeasurableSet {a : δ | f a < g a}

theorem nullMeasurableSet_lt {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {μ : MeasureTheory.Measure δ} {f : δ → α} {g : δ → α} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : MeasureTheory.NullMeasurableSet {a : δ | f a < g a} μ

theorem nullMeasurableSet_lt' {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {μ : MeasureTheory.Measure (α × α)} : MeasureTheory.NullMeasurableSet {p : α × α | p.1 < p.2} μ

theorem nullMeasurableSet_le {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {μ : MeasureTheory.Measure δ} {f : δ → α} {g : δ → α} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : MeasureTheory.NullMeasurableSet {a : δ | f a ≤ g a} μ

theorem Set.OrdConnected.measurableSet {α : Type u_1} {s : Set α} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] (h : Set.OrdConnected s) : MeasurableSet s

theorem IsPreconnected.measurableSet {α : Type u_1} {s : Set α} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] (h : IsPreconnected s) : MeasurableSet s

theorem generateFrom_Ico_mem_le_borel {α : Type u_7} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] (s : Set α) (t : Set α) : MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Set.Ico l u = S} ≤ borel α

theorem Dense.borel_eq_generateFrom_Ico_mem_aux {α : Type u_7} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {s : Set α} (hd : Dense s) (hbot : ∀ (x : α), IsBot x → x ∈ s) (hIoo : ∀ (x y : α), x < y → Set.Ioo x y = ∅ → y ∈ s) : borel α = 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} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [DenselyOrdered α] [NoMinOrder α] {s : Set α} (hd : Dense s) : borel α = MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Set.Ico l u = S}

theorem borel_eq_generateFrom_Ico (α : Type u_7) [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] : borel α = MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l < u ∧ Set.Ico l u = S}

theorem Dense.borel_eq_generateFrom_Ioc_mem_aux {α : Type u_7} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {s : Set α} (hd : Dense s) (hbot : ∀ (x : α), IsTop x → x ∈ s) (hIoo : ∀ (x y : α), x < y → Set.Ioo x y = ∅ → x ∈ s) : borel α = 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} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [DenselyOrdered α] [NoMaxOrder α] {s : Set α} (hd : Dense s) : borel α = MeasurableSpace.generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Set.Ioc l u = S}

theorem borel_eq_generateFrom_Ioc (α : Type u_7) [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] : borel α = MeasurableSpace.generateFrom {S : Set α | ∃ (l : α) (u : α), l < u ∧ Set.Ioc l u = S}

theorem MeasureTheory.Measure.ext_of_Ico_finite {α : Type u_7} [TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (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} [TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (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} [TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] [NoMaxOrder α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.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 they agree on all closed-open intervals.

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

theorem MeasureTheory.Measure.ext_of_Ico {α : Type u_7} [TopologicalSpace α] {_m : MeasurableSpace α} [SecondCountableTopology α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [BorelSpace α] [NoMaxOrder α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] (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} [TopologicalSpace α] {_m : MeasurableSpace α} [SecondCountableTopology α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [BorelSpace α] [NoMinOrder α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] (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} [TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (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 MeasureTheory.Measure.ext_of_Ici {α : Type u_7} [TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (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.

theorem measurableSet_uIcc {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} : MeasurableSet (Set.uIcc a b)

theorem measurableSet_uIoc {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [OrderClosedTopology α] {a : α} {b : α} : MeasurableSet (Ι a b)

theorem Measurable.max {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f : δ → α} {g : δ → α} (hf : Measurable f) (hg : Measurable g) : Measurable fun (a : δ) => max (f a) (g a)

theorem AEMeasurable.max {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f : δ → α} {g : δ → α} {μ : MeasureTheory.Measure δ} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : AEMeasurable (fun (a : δ) => max (f a) (g a)) μ

theorem Measurable.min {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f : δ → α} {g : δ → α} (hf : Measurable f) (hg : Measurable g) : Measurable fun (a : δ) => min (f a) (g a)

theorem AEMeasurable.min {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f : δ → α} {g : δ → α} {μ : MeasureTheory.Measure δ} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : AEMeasurable (fun (a : δ) => min (f a) (g a)) μ

theorem Continuous.measurable {α : Type u_1} {γ : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] {f : α → γ} (hf : Continuous f) : Measurable f

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

theorem Continuous.aemeasurable {α : Type u_1} {γ : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] {f : α → γ} (h : Continuous f) {μ : MeasureTheory.Measure α} : AEMeasurable f μ

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

theorem ClosedEmbedding.measurable {α : Type u_1} {γ : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] {f : α → γ} (hf : ClosedEmbedding f) : Measurable f

theorem ContinuousOn.measurable_piecewise {α : Type u_1} {γ : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] {f : α → γ} {g : α → γ} {s : Set α} [(j : α) → Decidable (j ∈ s)] (hf : ContinuousOn f s) (hg : ContinuousOn g sᶜ) (hs : MeasurableSet s) : Measurable (Set.piecewise s f g)

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

instance ContinuousAdd.measurableAdd {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [Add γ] [ContinuousAdd γ] : MeasurableAdd γ

Equations

• ⋯ = ⋯

instance ContinuousMul.measurableMul {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [Mul γ] [ContinuousMul γ] : MeasurableMul γ

Equations

• ⋯ = ⋯

instance ContinuousSub.measurableSub {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [Sub γ] [ContinuousSub γ] : MeasurableSub γ

Equations

• ⋯ = ⋯

instance TopologicalAddGroup.measurableNeg {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [AddGroup γ] [TopologicalAddGroup γ] : MeasurableNeg γ

Equations

• ⋯ = ⋯

instance TopologicalGroup.measurableInv {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [Group γ] [TopologicalGroup γ] : MeasurableInv γ

Equations

• ⋯ = ⋯

instance ContinuousSMul.measurableSMul {M : Type u_7} {α : Type u_8} [TopologicalSpace M] [TopologicalSpace α] [MeasurableSpace M] [MeasurableSpace α] [OpensMeasurableSpace M] [BorelSpace α] [SMul M α] [ContinuousSMul M α] : MeasurableSMul M α

Equations

• ⋯ = ⋯

instance ContinuousSup.measurableSup {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [Sup γ] [ContinuousSup γ] : MeasurableSup γ

Equations

• ⋯ = ⋯

instance ContinuousSup.measurableSup₂ {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [SecondCountableTopology γ] [Sup γ] [ContinuousSup γ] : MeasurableSup₂ γ

Equations

• ⋯ = ⋯

instance ContinuousInf.measurableInf {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [Inf γ] [ContinuousInf γ] : MeasurableInf γ

Equations

• ⋯ = ⋯

instance ContinuousInf.measurableInf₂ {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [SecondCountableTopology γ] [Inf γ] [ContinuousInf γ] : MeasurableInf₂ γ

Equations

• ⋯ = ⋯

theorem Homeomorph.measurable {α : Type u_1} {γ : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] (h : α ≃ₜ γ) : Measurable ⇑h

def Homeomorph.toMeasurableEquiv {γ : Type u_3} {γ₂ : Type u_4} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [TopologicalSpace γ₂] [MeasurableSpace γ₂] [BorelSpace γ₂] (h : γ ≃ₜ γ₂) : γ ≃ᵐ γ₂

A homeomorphism between two Borel spaces is a measurable equivalence.

Equations

• Homeomorph.toMeasurableEquiv h = { toEquiv := h.toEquiv, measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem Homeomorph.measurableEmbedding {γ : Type u_3} {γ₂ : Type u_4} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [TopologicalSpace γ₂] [MeasurableSpace γ₂] [BorelSpace γ₂] (h : γ ≃ₜ γ₂) : MeasurableEmbedding ⇑h

@[simp]

theorem Homeomorph.toMeasurableEquiv_coe {γ : Type u_3} {γ₂ : Type u_4} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [TopologicalSpace γ₂] [MeasurableSpace γ₂] [BorelSpace γ₂] (h : γ ≃ₜ γ₂) : ⇑(Homeomorph.toMeasurableEquiv h) = ⇑h

@[simp]

theorem Homeomorph.toMeasurableEquiv_symm_coe {γ : Type u_3} {γ₂ : Type u_4} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [TopologicalSpace γ₂] [MeasurableSpace γ₂] [BorelSpace γ₂] (h : γ ≃ₜ γ₂) : ⇑(Homeomorph.toMeasurableEquiv h).symm = ⇑(Homeomorph.symm h)

theorem ContinuousMap.measurable {α : Type u_1} {γ : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] (f : C(α, γ)) : Measurable ⇑f

theorem measurable_of_continuousOn_compl_singleton {α : Type u_1} {γ : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [T1Space α] {f : α → γ} (a : α) (hf : ContinuousOn f {a}ᶜ) : Measurable f

theorem Continuous.measurable2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace β] [MeasurableSpace β] [OpensMeasurableSpace β] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [MeasurableSpace δ] [SecondCountableTopologyEither α β] {f : δ → α} {g : δ → β} {c : α → β → γ} (h : Continuous fun (p : α × β) => c p.1 p.2) (hf : Measurable f) (hg : Measurable g) : Measurable fun (a : δ) => c (f a) (g a)

theorem Continuous.aemeasurable2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [TopologicalSpace β] [MeasurableSpace β] [OpensMeasurableSpace β] [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [MeasurableSpace δ] [SecondCountableTopologyEither α β] {f : δ → α} {g : δ → β} {c : α → β → γ} {μ : MeasureTheory.Measure δ} (h : Continuous fun (p : α × β) => c p.1 p.2) (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : AEMeasurable (fun (a : δ) => c (f a) (g a)) μ

instance HasContinuousInv₀.measurableInv {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [GroupWithZero γ] [T1Space γ] [HasContinuousInv₀ γ] : MeasurableInv γ

Equations

• ⋯ = ⋯

instance ContinuousAdd.measurableMul₂ {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [SecondCountableTopology γ] [Add γ] [ContinuousAdd γ] : MeasurableAdd₂ γ

Equations

• ⋯ = ⋯

instance ContinuousMul.measurableMul₂ {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [SecondCountableTopology γ] [Mul γ] [ContinuousMul γ] : MeasurableMul₂ γ

Equations

• ⋯ = ⋯

instance ContinuousSub.measurableSub₂ {γ : Type u_3} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [SecondCountableTopology γ] [Sub γ] [ContinuousSub γ] : MeasurableSub₂ γ

Equations

• ⋯ = ⋯

instance ContinuousSMul.measurableSMul₂ {M : Type u_7} {α : Type u_8} [TopologicalSpace M] [MeasurableSpace M] [OpensMeasurableSpace M] [TopologicalSpace α] [SecondCountableTopologyEither M α] [MeasurableSpace α] [BorelSpace α] [SMul M α] [ContinuousSMul M α] : MeasurableSMul₂ 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} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] : Prod.instMeasurableSpace ≤ borel (α × β)

instance Pi.borelSpace {ι : Type u_6} {π : ι → Type u_7} [Countable ι] [(i : ι) → TopologicalSpace (π i)] [(i : ι) → MeasurableSpace (π i)] [∀ (i : ι), SecondCountableTopology (π i)] [∀ (i : ι), BorelSpace (π i)] : BorelSpace ((i : ι) → π i)

Equations

• ⋯ = ⋯

instance Prod.borelSpace {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] [SecondCountableTopologyEither α β] : BorelSpace (α × β)

Equations

• ⋯ = ⋯

theorem MeasurableEmbedding.borelSpace {α : Type u_6} {β : Type u_7} [MeasurableSpace α] [TopologicalSpace α] [MeasurableSpace β] [TopologicalSpace β] [hβ : BorelSpace β] {e : α → β} (h'e : MeasurableEmbedding e) (h''e : Inducing e) : BorelSpace α

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} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] : BorelSpace (ULift.{u_6, u_1} α)

Equations

• ⋯ = ⋯

instance DiscreteMeasurableSpace.toBorelSpace {α : Type u_6} [TopologicalSpace α] [DiscreteTopology α] [MeasurableSpace α] [DiscreteMeasurableSpace α] : BorelSpace α

Equations

• ⋯ = ⋯

theorem Embedding.measurableEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] {f : α → β} (h₁ : Embedding f) (h₂ : MeasurableSet (Set.range f)) : MeasurableEmbedding f

theorem ClosedEmbedding.measurableEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] {f : α → β} (h : ClosedEmbedding f) : MeasurableEmbedding f

theorem OpenEmbedding.measurableEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] {f : α → β} (h : OpenEmbedding f) : MeasurableEmbedding f

theorem measurable_of_Iio {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δ → α} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' Set.Iio x)) : Measurable f

theorem UpperSemicontinuous.measurable {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [TopologicalSpace δ] [OpensMeasurableSpace δ] {f : δ → α} (hf : UpperSemicontinuous f) : Measurable f

theorem measurable_of_Ioi {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δ → α} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' Set.Ioi x)) : Measurable f

theorem LowerSemicontinuous.measurable {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [TopologicalSpace δ] [OpensMeasurableSpace δ] {f : δ → α} (hf : LowerSemicontinuous f) : Measurable f

theorem measurable_of_Iic {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δ → α} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' Set.Iic x)) : Measurable f

theorem measurable_of_Ici {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δ → α} (hf : ∀ (x : α), MeasurableSet (f ⁻¹' Set.Ici x)) : Measurable f

theorem Measurable.isLUB {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} [Countable ι] {f : ι → δ → α} {g : δ → α} (hf : ∀ (i : ι), Measurable (f i)) (hg : ∀ (b : δ), IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)) : Measurable g

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} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} [Countable ι] {f : ι → δ → α} {g : δ → α} {g' : δ → α} (hf : ∀ (i : ι), Measurable (f i)) {s : Set δ} (hs : MeasurableSet s) (hg : ∀ b ∈ s, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)) (hg' : Set.EqOn g g' sᶜ) (g'_meas : Measurable g') : Measurable g

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} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} {μ : MeasureTheory.Measure δ} [Countable ι] {f : ι → δ → α} {g : δ → α} (hf : ∀ (i : ι), AEMeasurable (f i) μ) (hg : ∀ᵐ (b : δ) ∂μ, IsLUB {a : α | ∃ (i : ι), f i b = a} (g b)) : AEMeasurable g μ

theorem Measurable.isGLB {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} [Countable ι] {f : ι → δ → α} {g : δ → α} (hf : ∀ (i : ι), Measurable (f i)) (hg : ∀ (b : δ), IsGLB {a : α | ∃ (i : ι), f i b = a} (g b)) : Measurable g

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} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} [Countable ι] {f : ι → δ → α} {g : δ → α} {g' : δ → α} (hf : ∀ (i : ι), Measurable (f i)) {s : Set δ} (hs : MeasurableSet s) (hg : ∀ b ∈ s, IsGLB {a : α | ∃ (i : ι), f i b = a} (g b)) (hg' : Set.EqOn g g' sᶜ) (g'_meas : Measurable g') : Measurable g

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} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} {μ : MeasureTheory.Measure δ} [Countable ι] {f : ι → δ → α} {g : δ → α} (hf : ∀ (i : ι), AEMeasurable (f i) μ) (hg : ∀ᵐ (b : δ) ∂μ, IsGLB {a : α | ∃ (i : ι), f i b = a} (g b)) : AEMeasurable g μ

theorem Monotone.measurable {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [LinearOrder β] [OrderClosedTopology β] {f : β → α} (hf : Monotone f) : Measurable f

theorem aemeasurable_restrict_of_monotoneOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [LinearOrder β] [OrderClosedTopology β] {μ : MeasureTheory.Measure β} {s : Set β} (hs : MeasurableSet s) {f : β → α} (hf : MonotoneOn f s) : AEMeasurable f (MeasureTheory.Measure.restrict μ s)

theorem Antitone.measurable {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [LinearOrder β] [OrderClosedTopology β] {f : β → α} (hf : Antitone f) : Measurable f

theorem aemeasurable_restrict_of_antitoneOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [LinearOrder β] [OrderClosedTopology β] {μ : MeasureTheory.Measure β} {s : Set β} (hs : MeasurableSet s) {f : β → α} (hf : AntitoneOn f s) : AEMeasurable f (MeasureTheory.Measure.restrict μ s)

theorem measurableSet_of_mem_nhdsWithin_Ioi_aux {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {s : Set α} (h : ∀ x ∈ s, s ∈ nhdsWithin x (Set.Ioi x)) (h' : ∀ x ∈ s, ∃ (y : α), x < y) : MeasurableSet s

theorem measurableSet_of_mem_nhdsWithin_Ioi {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {s : Set α} (h : ∀ x ∈ s, s ∈ nhdsWithin x (Set.Ioi x)) : MeasurableSet s

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} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} [Countable ι] {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} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} [Countable ι] {f : ι → δ → α} (hf : ∀ (i : ι), Measurable (f i)) : MeasurableSet {b : δ | BddBelow (Set.range fun (i : ι) => f i b)}

theorem Measurable.iSup_Prop {δ : Type u_5} [MeasurableSpace δ] {α : Type u_6} [MeasurableSpace α] [ConditionallyCompleteLattice α] (p : Prop) {f : δ → α} (hf : Measurable f) : Measurable fun (b : δ) => ⨆ (_ : p), f b

theorem Measurable.iInf_Prop {δ : Type u_5} [MeasurableSpace δ] {α : Type u_6} [MeasurableSpace α] [ConditionallyCompleteLattice α] (p : Prop) {f : δ → α} (hf : Measurable f) : Measurable fun (b : δ) => ⨅ (_ : p), f b

theorem measurable_iSup {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} [Countable ι] {f : ι → δ → α} (hf : ∀ (i : ι), Measurable (f i)) : Measurable fun (b : δ) => ⨆ (i : ι), f i b

theorem aemeasurable_iSup {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} {μ : MeasureTheory.Measure δ} [Countable ι] {f : ι → δ → α} (hf : ∀ (i : ι), AEMeasurable (f i) μ) : AEMeasurable (fun (b : δ) => ⨆ (i : ι), f i b) μ

theorem measurable_iInf {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} [Countable ι] {f : ι → δ → α} (hf : ∀ (i : ι), Measurable (f i)) : Measurable fun (b : δ) => ⨅ (i : ι), f i b

theorem aemeasurable_iInf {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_6} {μ : MeasureTheory.Measure δ} [Countable ι] {f : ι → δ → α} (hf : ∀ (i : ι), AEMeasurable (f i) μ) : AEMeasurable (fun (b : δ) => ⨅ (i : ι), f i b) μ

theorem measurable_sSup {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_6} {f : ι → δ → α} {s : Set ι} (hs : Set.Countable s) (hf : ∀ i ∈ s, Measurable (f i)) : Measurable fun (x : δ) => sSup ((fun (i : ι) => f i x) '' s)

theorem measurable_sInf {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_6} {f : ι → δ → α} {s : Set ι} (hs : Set.Countable s) (hf : ∀ i ∈ s, Measurable (f i)) : Measurable fun (x : δ) => sInf ((fun (i : ι) => f i x) '' s)

theorem measurable_biSup {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_6} (s : Set ι) {f : ι → δ → α} (hs : Set.Countable s) (hf : ∀ i ∈ s, Measurable (f i)) : Measurable fun (b : δ) => ⨆ i ∈ s, f i b

theorem aemeasurable_biSup {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_6} {μ : MeasureTheory.Measure δ} (s : Set ι) {f : ι → δ → α} (hs : Set.Countable s) (hf : ∀ i ∈ s, AEMeasurable (f i) μ) : AEMeasurable (fun (b : δ) => ⨆ i ∈ s, f i b) μ

theorem measurable_biInf {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_6} (s : Set ι) {f : ι → δ → α} (hs : Set.Countable s) (hf : ∀ i ∈ s, Measurable (f i)) : Measurable fun (b : δ) => ⨅ i ∈ s, f i b

theorem aemeasurable_biInf {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_6} {μ : MeasureTheory.Measure δ} (s : Set ι) {f : ι → δ → α} (hs : Set.Countable s) (hf : ∀ i ∈ s, AEMeasurable (f i) μ) : AEMeasurable (fun (b : δ) => ⨅ i ∈ s, f i b) μ

theorem measurable_liminf' {α : Type u_1} {δ : Type u_5} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_6} {ι' : Type u_7} {f : ι → δ → α} {v : Filter ι} (hf : ∀ (i : ι), Measurable (f i)) {p : ι' → Prop} {s : ι' → Set ι} (hv : Filter.HasCountableBasis v p s) (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} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_6} {ι' : Type u_7} {f : ι → δ → α} {u : Filter ι} (hf : ∀ (i : ι), Measurable (f i)) {p : ι' → Prop} {s : ι' → Set ι} (hu : Filter.HasCountableBasis u p s) (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} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {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} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [MeasurableSpace δ] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {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} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] (h : α ≃ₜ β) : α ≃ᵐ β

Convert a Homeomorph to a MeasurableEquiv.

Equations

• Homemorph.toMeasurableEquiv h = { toEquiv := h.toEquiv, measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem IsFiniteMeasureOnCompacts.map {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (f : α ≃ₜ β) : MeasureTheory.IsFiniteMeasureOnCompacts (MeasureTheory.Measure.map (⇑f) μ)

instance Empty.borelSpace : BorelSpace Empty

Equations

• Empty.borelSpace = ⋯

instance Unit.borelSpace : BorelSpace Unit

Equations

• Unit.borelSpace = ⋯

instance Bool.borelSpace : BorelSpace Bool

Equations

• Bool.borelSpace = ⋯

instance Nat.borelSpace : BorelSpace ℕ

Equations

• Nat.borelSpace = ⋯

instance Int.borelSpace : BorelSpace ℤ

Equations

• Int.borelSpace = ⋯

instance Rat.borelSpace : BorelSpace ℚ

Equations

• Rat.borelSpace = ⋯

instance Real.measurableSpace : MeasurableSpace ℝ

Equations

• Real.measurableSpace = borel ℝ

instance Real.borelSpace : BorelSpace ℝ

Equations

• Real.borelSpace = ⋯

instance NNReal.measurableSpace : MeasurableSpace NNReal

Equations

• NNReal.measurableSpace = Subtype.instMeasurableSpace

instance NNReal.borelSpace : BorelSpace NNReal

Equations

• NNReal.borelSpace = ⋯

instance ENNReal.measurableSpace : MeasurableSpace ENNReal

Equations

• ENNReal.measurableSpace = borel ENNReal

instance ENNReal.borelSpace : BorelSpace ENNReal

Equations

• ENNReal.borelSpace = ⋯

instance EReal.measurableSpace : MeasurableSpace EReal

Equations

• EReal.measurableSpace = borel EReal

instance EReal.borelSpace : BorelSpace EReal

Equations

• EReal.borelSpace = ⋯

theorem measure_eq_measure_preimage_add_measure_tsum_Ico_zpow {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → ENNReal} (hf : Measurable f) {s : Set α} (hs : MeasurableSet 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.

theorem measurableSet_ball {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {x : α} {ε : ℝ} : MeasurableSet (Metric.ball x ε)

theorem measurableSet_closedBall {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {x : α} {ε : ℝ} : MeasurableSet (Metric.closedBall x ε)

theorem measurable_infDist {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {s : Set α} : Measurable fun (x : α) => Metric.infDist x s

theorem Measurable.infDist {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : β → α} (hf : Measurable f) {s : Set α} : Measurable fun (x : β) => Metric.infDist (f x) s

theorem measurable_infNndist {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {s : Set α} : Measurable fun (x : α) => Metric.infNndist x s

theorem Measurable.infNndist {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : β → α} (hf : Measurable f) {s : Set α} : Measurable fun (x : β) => Metric.infNndist (f x) s

theorem measurable_dist {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [SecondCountableTopology α] : Measurable fun (p : α × α) => dist p.1 p.2

theorem Measurable.dist {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] [SecondCountableTopology α] {f : β → α} {g : β → α} (hf : Measurable f) (hg : Measurable g) : Measurable fun (b : β) => dist (f b) (g b)

theorem measurable_nndist {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [SecondCountableTopology α] : Measurable fun (p : α × α) => nndist p.1 p.2

theorem Measurable.nndist {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] [SecondCountableTopology α] {f : β → α} {g : β → α} (hf : Measurable f) (hg : Measurable g) : Measurable fun (b : β) => nndist (f b) (g b)

theorem measurableSet_eball {α : Type u_1} [PseudoEMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {x : α} {ε : ENNReal} : MeasurableSet (EMetric.ball x ε)

theorem measurable_edist_right {α : Type u_1} [PseudoEMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {x : α} : Measurable (edist x)

theorem measurable_edist_left {α : Type u_1} [PseudoEMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {x : α} : Measurable fun (y : α) => edist y x

theorem measurable_infEdist {α : Type u_1} [PseudoEMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {s : Set α} : Measurable fun (x : α) => EMetric.infEdist x s

theorem Measurable.infEdist {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : β → α} (hf : Measurable f) {s : Set α} : Measurable fun (x : β) => EMetric.infEdist (f x) s

theorem tendsto_measure_cthickening {α : Type u_1} [PseudoEMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : ∃ R > 0, ↑↑μ (Metric.cthickening R s) ≠ ⊤) : Filter.Tendsto (fun (r : ℝ) => ↑↑μ (Metric.cthickening 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_isClosed {α : Type u_1} [PseudoEMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : ∃ R > 0, ↑↑μ (Metric.cthickening R s) ≠ ⊤) (h's : IsClosed s) : Filter.Tendsto (fun (r : ℝ) => ↑↑μ (Metric.cthickening r s)) (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} [PseudoEMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : ∃ R > 0, ↑↑μ (Metric.thickening R s) ≠ ⊤) : Filter.Tendsto (fun (r : ℝ) => ↑↑μ (Metric.thickening r s)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (↑↑μ (closure s)))

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} [PseudoEMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : ∃ R > 0, ↑↑μ (Metric.thickening R s) ≠ ⊤) (h's : IsClosed s) : Filter.Tendsto (fun (r : ℝ) => ↑↑μ (Metric.thickening r s)) (nhdsWithin 0 (Set.Ioi 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} [PseudoEMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [SecondCountableTopology α] : Measurable fun (p : α × α) => edist p.1 p.2

theorem Measurable.edist {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] [SecondCountableTopology α] {f : β → α} {g : β → α} (hf : Measurable f) (hg : Measurable g) : Measurable fun (b : β) => edist (f b) (g b)

theorem AEMeasurable.edist {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] [SecondCountableTopology α] {f : β → α} {g : β → α} {μ : MeasureTheory.Measure β} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : AEMeasurable (fun (a : β) => edist (f a) (g a)) μ

theorem tendsto_measure_cthickening_of_isCompact {α : Type u_1} [MetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [ProperSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {s : Set α} (hs : IsCompact s) : Filter.Tendsto (fun (r : ℝ) => ↑↑μ (Metric.cthickening 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.

theorem Real.borel_eq_generateFrom_Ioo_rat : borel ℝ = MeasurableSpace.generateFrom (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Set.Ioo ↑a ↑b})

theorem Real.borel_eq_generateFrom_Iio_rat : borel ℝ = MeasurableSpace.generateFrom (⋃ (a : ℚ), {Set.Iio ↑a})

theorem Real.borel_eq_generateFrom_Ioi_rat : borel ℝ = MeasurableSpace.generateFrom (⋃ (a : ℚ), {Set.Ioi ↑a})

theorem Real.borel_eq_generateFrom_Iic_rat : borel ℝ = MeasurableSpace.generateFrom (⋃ (a : ℚ), {Set.Iic ↑a})

theorem Real.borel_eq_generateFrom_Ici_rat : borel ℝ = MeasurableSpace.generateFrom (⋃ (a : ℚ), {Set.Ici ↑a})

theorem Real.isPiSystem_Ioo_rat : IsPiSystem (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Set.Ioo ↑a ↑b})

theorem Real.isPiSystem_Iio_rat : IsPiSystem (⋃ (a : ℚ), {Set.Iio ↑a})

theorem Real.isPiSystem_Ioi_rat : IsPiSystem (⋃ (a : ℚ), {Set.Ioi ↑a})

theorem Real.isPiSystem_Iic_rat : IsPiSystem (⋃ (a : ℚ), {Set.Iic ↑a})

theorem Real.isPiSystem_Ici_rat : IsPiSystem (⋃ (a : ℚ), {Set.Ici ↑a})

def Real.finiteSpanningSetsInIooRat (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsLocallyFiniteMeasure μ] : 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.

theorem Real.measure_ext_Ioo_rat {μ : MeasureTheory.Measure ℝ} {ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] (h : ∀ (a b : ℚ), ↑↑μ (Set.Ioo ↑a ↑b) = ↑↑ν (Set.Ioo ↑a ↑b)) : μ = ν

theorem measurable_real_toNNReal : Measurable Real.toNNReal

theorem Measurable.real_toNNReal {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} (hf : Measurable f) : Measurable fun (x : α) => Real.toNNReal (f x)

theorem AEMeasurable.real_toNNReal {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => Real.toNNReal (f x)) μ

theorem measurable_coe_nnreal_real : Measurable NNReal.toReal

theorem Measurable.coe_nnreal_real {α : Type u_1} [MeasurableSpace α] {f : α → NNReal} (hf : Measurable f) : Measurable fun (x : α) => ↑(f x)

theorem AEMeasurable.coe_nnreal_real {α : Type u_1} [MeasurableSpace α] {f : α → NNReal} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => ↑(f x)) μ

theorem measurable_coe_nnreal_ennreal : Measurable ENNReal.ofNNReal

theorem Measurable.coe_nnreal_ennreal {α : Type u_1} [MeasurableSpace α] {f : α → NNReal} (hf : Measurable f) : Measurable fun (x : α) => ↑(f x)

theorem AEMeasurable.coe_nnreal_ennreal {α : Type u_1} [MeasurableSpace α] {f : α → NNReal} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => ↑(f x)) μ

theorem Measurable.ennreal_ofReal {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} (hf : Measurable f) : Measurable fun (x : α) => ENNReal.ofReal (f x)

theorem AEMeasurable.ennreal_ofReal {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => ENNReal.ofReal (f x)) μ

@[simp]

theorem measurable_coe_nnreal_real_iff {α : Type u_1} [MeasurableSpace α] {f : α → NNReal} : (Measurable fun (x : α) => ↑(f x)) ↔ Measurable f

@[simp]

theorem aemeasurable_coe_nnreal_real_iff {α : Type u_1} [MeasurableSpace α] {f : α → NNReal} {μ : MeasureTheory.Measure α} : AEMeasurable (fun (x : α) => ↑(f x)) μ ↔ AEMeasurable f μ

@[deprecated aemeasurable_coe_nnreal_real_iff]

theorem aEMeasurable_coe_nnreal_real_iff {α : Type u_1} [MeasurableSpace α] {f : α → NNReal} {μ : MeasureTheory.Measure α} : AEMeasurable (fun (x : α) => ↑(f x)) μ ↔ AEMeasurable f μ

Alias of aemeasurable_coe_nnreal_real_iff.

def MeasurableEquiv.ennrealEquivNNReal : ↑{r : ENNReal | r ≠ ⊤} ≃ᵐ NNReal

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

Equations

• MeasurableEquiv.ennrealEquivNNReal = Homeomorph.toMeasurableEquiv ENNReal.neTopHomeomorphNNReal

theorem ENNReal.measurable_of_measurable_nnreal {α : Type u_1} [MeasurableSpace α] {f : ENNReal → α} (h : Measurable fun (p : NNReal) => f ↑p) : Measurable f

def ENNReal.ennrealEquivSum : ENNReal ≃ᵐ NNReal ⊕ Unit

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

Equations

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

theorem ENNReal.measurable_of_measurable_nnreal_prod {β : Type u_2} {γ : Type u_3} [MeasurableSpace β] [MeasurableSpace γ] {f : ENNReal × β → γ} (H₁ : Measurable fun (p : NNReal × β) => f (↑p.1, p.2)) (H₂ : Measurable fun (x : β) => f (⊤, x)) : Measurable f

theorem ENNReal.measurable_of_measurable_nnreal_nnreal {β : Type u_2} [MeasurableSpace β] {f : ENNReal × ENNReal → β} (h₁ : Measurable fun (p : NNReal × NNReal) => f (↑p.1, ↑p.2)) (h₂ : Measurable fun (r : NNReal) => f (⊤, ↑r)) (h₃ : Measurable fun (r : NNReal) => f (↑r, ⊤)) : Measurable f

theorem ENNReal.measurable_ofReal : Measurable ENNReal.ofReal

theorem ENNReal.measurable_toReal : Measurable ENNReal.toReal

theorem ENNReal.measurable_toNNReal : Measurable ENNReal.toNNReal

instance ENNReal.instMeasurableMul₂ : MeasurableMul₂ ENNReal

Equations

• ENNReal.instMeasurableMul₂ = ⋯

instance ENNReal.instMeasurableSub₂ : MeasurableSub₂ ENNReal

Equations

• ENNReal.instMeasurableSub₂ = ⋯

instance ENNReal.instMeasurableInv : MeasurableInv ENNReal

Equations

• ENNReal.instMeasurableInv = ⋯

instance ENNReal.instMeasurableSMulNNRealENNRealToSMulInstNNRealCommSemiringToSemiringToOrderedSemiringToOrderedCommSemiringInstCanonicallyOrderedCommSemiringENNRealInstAlgebraNNRealInstNNRealCommSemiringIdToCommSemiringMeasurableSpaceMeasurableSpace : MeasurableSMul NNReal ENNReal

Equations

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

theorem ENNReal.measurable_of_tendsto' {α : Type u_1} [MeasurableSpace α] {ι : Type u_6} {f : ι → α → ENNReal} {g : α → ENNReal} (u : Filter ι) [Filter.NeBot u] [Filter.IsCountablyGenerated u] (hf : ∀ (i : ι), Measurable (f i)) (lim : Filter.Tendsto f u (nhds g)) : Measurable 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} [MeasurableSpace α] {ι : Type u_6} {f : ι → α → ENNReal} {g : α → ENNReal} (u : Filter ι) [Filter.NeBot u] [Filter.IsCountablyGenerated u] (hf : ∀ (i : ι), Measurable (f i)) (lim : Filter.Tendsto f u (nhds g)) : Measurable 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} [MeasurableSpace α] {f : ℕ → α → ENNReal} {g : α → ENNReal} (hf : ∀ (i : ℕ), Measurable (f i)) (lim : Filter.Tendsto f Filter.atTop (nhds g)) : Measurable g

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

@[deprecated ENNReal.measurable_of_tendsto]

theorem measurable_of_tendsto_ennreal {α : Type u_1} [MeasurableSpace α] {f : ℕ → α → ENNReal} {g : α → ENNReal} (hf : ∀ (i : ℕ), Measurable (f i)) (lim : Filter.Tendsto f Filter.atTop (nhds g)) : Measurable 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} [MeasurableSpace α] {ι : Type u_6} {f : ι → α → ENNReal} {g : α → ENNReal} {μ : MeasureTheory.Measure α} (u : Filter ι) [Filter.NeBot u] [Filter.IsCountablyGenerated u] (hf : ∀ (i : ι), AEMeasurable (f i) μ) (hlim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (i : ι) => f i a) u (nhds (g a))) : AEMeasurable g μ

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} [MeasurableSpace α] {f : ℕ → α → ENNReal} {g : α → ENNReal} {μ : MeasureTheory.Measure α} (hf : ∀ (i : ℕ), AEMeasurable (f i) μ) (hlim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (i : ℕ) => f i a) Filter.atTop (nhds (g a))) : AEMeasurable g μ

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

theorem Measurable.ennreal_toNNReal {α : Type u_1} [MeasurableSpace α] {f : α → ENNReal} (hf : Measurable f) : Measurable fun (x : α) => (f x).toNNReal

theorem AEMeasurable.ennreal_toNNReal {α : Type u_1} [MeasurableSpace α] {f : α → ENNReal} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => (f x).toNNReal) μ

@[simp]

theorem measurable_coe_nnreal_ennreal_iff {α : Type u_1} [MeasurableSpace α] {f : α → NNReal} : (Measurable fun (x : α) => ↑(f x)) ↔ Measurable f

@[simp]

theorem aemeasurable_coe_nnreal_ennreal_iff {α : Type u_1} [MeasurableSpace α] {f : α → NNReal} {μ : MeasureTheory.Measure α} : AEMeasurable (fun (x : α) => ↑(f x)) μ ↔ AEMeasurable f μ

theorem Measurable.ennreal_toReal {α : Type u_1} [MeasurableSpace α] {f : α → ENNReal} (hf : Measurable f) : Measurable fun (x : α) => (f x).toReal

theorem AEMeasurable.ennreal_toReal {α : Type u_1} [MeasurableSpace α] {f : α → ENNReal} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => (f x).toReal) μ

theorem Measurable.ennreal_tsum {α : Type u_1} [MeasurableSpace α] {ι : Type u_6} [Countable ι] {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} [MeasurableSpace α] {ι : Type u_6} [Countable ι] {f : ι → α → ENNReal} (h : ∀ (i : ι), Measurable (f i)) : Measurable (∑' (i : ι), f i)

theorem Measurable.nnreal_tsum {α : Type u_1} [MeasurableSpace α] {ι : Type u_6} [Countable ι] {f : ι → α → NNReal} (h : ∀ (i : ι), Measurable (f i)) : Measurable fun (x : α) => ∑' (i : ι), f i x

theorem AEMeasurable.ennreal_tsum {α : Type u_1} [MeasurableSpace α] {ι : Type u_6} [Countable ι] {f : ι → α → ENNReal} {μ : MeasureTheory.Measure α} (h : ∀ (i : ι), AEMeasurable (f i) μ) : AEMeasurable (fun (x : α) => ∑' (i : ι), f i x) μ

theorem AEMeasurable.nnreal_tsum {α : Type u_6} [MeasurableSpace α] {ι : Type u_7} [Countable ι] {f : ι → α → NNReal} {μ : MeasureTheory.Measure α} (h : ∀ (i : ι), AEMeasurable (f i) μ) : AEMeasurable (fun (x : α) => ∑' (i : ι), f i x) μ

theorem measurable_coe_real_ereal : Measurable Real.toEReal

theorem Measurable.coe_real_ereal {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} (hf : Measurable f) : Measurable fun (x : α) => ↑(f x)

theorem AEMeasurable.coe_real_ereal {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => ↑(f x)) μ

def MeasurableEquiv.erealEquivReal : ↑{⊥, ⊤}ᶜ ≃ᵐ ℝ

The set of finite EReal numbers is MeasurableEquiv to ℝ.

Equations

• MeasurableEquiv.erealEquivReal = Homeomorph.toMeasurableEquiv EReal.neBotTopHomeomorphReal

theorem EReal.measurable_of_measurable_real {α : Type u_1} [MeasurableSpace α] {f : EReal → α} (h : Measurable fun (p : ℝ) => f ↑p) : Measurable f

theorem measurable_ereal_toReal : Measurable EReal.toReal

theorem Measurable.ereal_toReal {α : Type u_1} [MeasurableSpace α] {f : α → EReal} (hf : Measurable f) : Measurable fun (x : α) => EReal.toReal (f x)

theorem AEMeasurable.ereal_toReal {α : Type u_1} [MeasurableSpace α] {f : α → EReal} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => EReal.toReal (f x)) μ

theorem measurable_coe_ennreal_ereal : Measurable ENNReal.toEReal

theorem Measurable.coe_ereal_ennreal {α : Type u_1} [MeasurableSpace α] {f : α → ENNReal} (hf : Measurable f) : Measurable fun (x : α) => ↑(f x)

theorem AEMeasurable.coe_ereal_ennreal {α : Type u_1} [MeasurableSpace α] {f : α → ENNReal} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => ↑(f x)) μ

theorem NNReal.measurable_of_tendsto' {α : Type u_1} [MeasurableSpace α] {ι : Type u_6} {f : ι → α → NNReal} {g : α → NNReal} (u : Filter ι) [Filter.NeBot u] [Filter.IsCountablyGenerated u] (hf : ∀ (i : ι), Measurable (f i)) (lim : Filter.Tendsto f u (nhds g)) : Measurable 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} [MeasurableSpace α] {ι : Type u_6} {f : ι → α → NNReal} {g : α → NNReal} (u : Filter ι) [Filter.NeBot u] [Filter.IsCountablyGenerated u] (hf : ∀ (i : ι), Measurable (f i)) (lim : Filter.Tendsto f u (nhds g)) : Measurable 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} [MeasurableSpace α] {f : ℕ → α → NNReal} {g : α → NNReal} (hf : ∀ (i : ℕ), Measurable (f i)) (lim : Filter.Tendsto f Filter.atTop (nhds g)) : Measurable g

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

@[deprecated NNReal.measurable_of_tendsto]

theorem measurable_of_tendsto_nnreal {α : Type u_1} [MeasurableSpace α] {f : ℕ → α → NNReal} {g : α → NNReal} (hf : ∀ (i : ℕ), Measurable (f i)) (lim : Filter.Tendsto f Filter.atTop (nhds g)) : Measurable 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 : MeasurableSpace α} {f : α → NNReal} (hf : Measurable f) (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : ∃ (s : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (s n) ∧ ↑↑μ (s n) < ⊤ ∧ ∀ x ∈ s 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} [MeasurableSpace α] [NormedAddCommGroup α] [OpensMeasurableSpace α] : Measurable norm

theorem Measurable.norm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [NormedAddCommGroup α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : β → α} (hf : Measurable f) : Measurable fun (a : β) => ‖f a‖

theorem AEMeasurable.norm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [NormedAddCommGroup α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : β → α} {μ : MeasureTheory.Measure β} (hf : AEMeasurable f μ) : AEMeasurable (fun (a : β) => ‖f a‖) μ

theorem measurable_nnnorm {α : Type u_1} [MeasurableSpace α] [NormedAddCommGroup α] [OpensMeasurableSpace α] : Measurable nnnorm

theorem Measurable.nnnorm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [NormedAddCommGroup α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : β → α} (hf : Measurable f) : Measurable fun (a : β) => ‖f a‖₊

theorem AEMeasurable.nnnorm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [NormedAddCommGroup α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : β → α} {μ : MeasureTheory.Measure β} (hf : AEMeasurable f μ) : AEMeasurable (fun (a : β) => ‖f a‖₊) μ

theorem measurable_ennnorm {α : Type u_1} [MeasurableSpace α] [NormedAddCommGroup α] [OpensMeasurableSpace α] : Measurable fun (x : α) => ↑‖x‖₊

theorem Measurable.ennnorm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [NormedAddCommGroup α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : β → α} (hf : Measurable f) : Measurable fun (a : β) => ↑‖f a‖₊

theorem AEMeasurable.ennnorm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [NormedAddCommGroup α] [OpensMeasurableSpace α] [MeasurableSpace β] {f : β → α} {μ : MeasureTheory.Measure β} (hf : AEMeasurable f μ) : AEMeasurable (fun (a : β) => ↑‖f a‖₊) μ