Documentation

Mathlib.MeasureTheory.MeasurableSpace.Basic

Measurable spaces and measurable functions #

This file provides properties of measurable spaces and the functions and isomorphisms between them. The definition of a measurable space is in Mathlib/MeasureTheory/MeasurableSpace/Defs.lean.

A measurable space is a set equipped with a σ-algebra, a collection of subsets closed under complementation and countable union. A function between measurable spaces is measurable if the preimage of each measurable subset is measurable.

σ-algebras on a fixed set α form a complete lattice. Here we order σ-algebras by writing m₁ ≤ m₂ if every set which is m₁-measurable is also m₂-measurable (that is, m₁ is a subset of m₂). In particular, any collection of subsets of α generates a smallest σ-algebra which contains all of them. A function f : α → β induces a Galois connection between the lattices of σ-algebras on α and β.

A measurable equivalence between measurable spaces is an equivalence which respects the σ-algebras, that is, for which both directions of the equivalence are measurable functions.

We say that a filter f is measurably generated if every set s ∈ f includes a measurable set t ∈ f. This property is useful, e.g., to extract a measurable witness of Filter.Eventually.

Notation #

We write α ≃ᵐ β for measurable equivalences between the measurable spaces α and β. This should not be confused with ≃ₘ which is used for diffeomorphisms between manifolds.

Implementation notes #

Measurability of a function f : α → β between measurable spaces is defined in terms of the Galois connection induced by f.

References #

Tags #

measurable space, σ-algebra, measurable function, measurable equivalence, dynkin system, π-λ theorem, π-system

def MeasurableSpace.map {α : Type u_1} {β : Type u_2} (f : α → β) (m : MeasurableSpace α) :

MeasurableSpace β

The forward image of a measurable space under a function. map f m contains the sets s : Set β whose preimage under f is measurable.

Equations

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

Instances For

theorem MeasurableSpace.map_def {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : α → β} {s : Set β} :

MeasurableSet s ↔ MeasurableSet (f ⁻¹' s)

@[simp]

theorem MeasurableSpace.map_id {α : Type u_1} {m : MeasurableSpace α} :

MeasurableSpace.map id m = m

@[simp]

theorem MeasurableSpace.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {f : α → β} {g : β → γ} :

MeasurableSpace.map g (MeasurableSpace.map f m) = MeasurableSpace.map (g ∘ f) m

def MeasurableSpace.comap {α : Type u_1} {β : Type u_2} (f : α → β) (m : MeasurableSpace β) :

MeasurableSpace α

The reverse image of a measurable space under a function. comap f m contains the sets s : Set α such that s is the f-preimage of a measurable set in β.

Equations

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

Instances For

theorem MeasurableSpace.comap_eq_generateFrom {α : Type u_1} {β : Type u_2} (m : MeasurableSpace β) (f : α → β) :

MeasurableSpace.comap f m = MeasurableSpace.generateFrom {t : Set α | ∃ (s : Set β), MeasurableSet s ∧ f ⁻¹' s = t}

@[simp]

theorem MeasurableSpace.comap_id {α : Type u_1} {m : MeasurableSpace α} :

MeasurableSpace.comap id m = m

@[simp]

theorem MeasurableSpace.comap_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {f : β → α} {g : γ → β} :

MeasurableSpace.comap g (MeasurableSpace.comap f m) = MeasurableSpace.comap (f ∘ g) m

theorem MeasurableSpace.comap_le_iff_le_map {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {m' : MeasurableSpace β} {f : α → β} :

MeasurableSpace.comap f m' ≤ m ↔ m' ≤ MeasurableSpace.map f m

theorem MeasurableSpace.gc_comap_map {α : Type u_1} {β : Type u_2} (f : α → β) :

GaloisConnection (MeasurableSpace.comap f) (MeasurableSpace.map f)

theorem MeasurableSpace.map_mono {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} {f : α → β} (h : m₁ ≤ m₂) :

MeasurableSpace.map f m₁ ≤ MeasurableSpace.map f m₂

theorem MeasurableSpace.monotone_map {α : Type u_1} {β : Type u_2} {f : α → β} :

Monotone (MeasurableSpace.map f)

theorem MeasurableSpace.comap_mono {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} {g : β → α} (h : m₁ ≤ m₂) :

MeasurableSpace.comap g m₁ ≤ MeasurableSpace.comap g m₂

theorem MeasurableSpace.monotone_comap {α : Type u_1} {β : Type u_2} {g : β → α} :

Monotone (MeasurableSpace.comap g)

@[simp]

theorem MeasurableSpace.comap_bot {α : Type u_1} {β : Type u_2} {g : β → α} :

MeasurableSpace.comap g ⊥ = ⊥

@[simp]

theorem MeasurableSpace.comap_sup {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} {g : β → α} :

MeasurableSpace.comap g (m₁ ⊔ m₂) = MeasurableSpace.comap g m₁ ⊔ MeasurableSpace.comap g m₂

@[simp]

theorem MeasurableSpace.comap_iSup {α : Type u_1} {β : Type u_2} {ι : Sort uι} {g : β → α} {m : ι → MeasurableSpace α} :

MeasurableSpace.comap g (⨆ (i : ι), m i) = ⨆ (i : ι), MeasurableSpace.comap g (m i)

@[simp]

theorem MeasurableSpace.map_top {α : Type u_1} {β : Type u_2} {f : α → β} :

MeasurableSpace.map f ⊤ = ⊤

@[simp]

theorem MeasurableSpace.map_inf {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} {f : α → β} :

MeasurableSpace.map f (m₁ ⊓ m₂) = MeasurableSpace.map f m₁ ⊓ MeasurableSpace.map f m₂

@[simp]

theorem MeasurableSpace.map_iInf {α : Type u_1} {β : Type u_2} {ι : Sort uι} {f : α → β} {m : ι → MeasurableSpace α} :

MeasurableSpace.map f (⨅ (i : ι), m i) = ⨅ (i : ι), MeasurableSpace.map f (m i)

theorem MeasurableSpace.comap_map_le {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : α → β} :

MeasurableSpace.comap f (MeasurableSpace.map f m) ≤ m

theorem MeasurableSpace.le_map_comap {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {g : β → α} :

m ≤ MeasurableSpace.map g (MeasurableSpace.comap g m)

@[simp]

theorem MeasurableSpace.map_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} (b : β) :

MeasurableSpace.map (fun (_a : α) => b) m = ⊤

@[simp]

theorem MeasurableSpace.comap_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace β} (b : β) :

MeasurableSpace.comap (fun (_a : α) => b) m = ⊥

theorem MeasurableSpace.comap_generateFrom {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set (Set β)} :

MeasurableSpace.comap f (MeasurableSpace.generateFrom s) = MeasurableSpace.generateFrom (Set.preimage f '' s)

theorem measurable_iff_le_map {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β} :

Measurable f ↔ m₂ ≤ MeasurableSpace.map f m₁

theorem Measurable.le_map {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β} :

Measurable f → m₂ ≤ MeasurableSpace.map f m₁

Alias of the forward direction of measurable_iff_le_map.

theorem Measurable.of_le_map {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β} :

m₂ ≤ MeasurableSpace.map f m₁ → Measurable f

Alias of the reverse direction of measurable_iff_le_map.

theorem measurable_iff_comap_le {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β} :

Measurable f ↔ MeasurableSpace.comap f m₂ ≤ m₁

theorem Measurable.of_comap_le {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β} :

MeasurableSpace.comap f m₂ ≤ m₁ → Measurable f

Alias of the reverse direction of measurable_iff_comap_le.

theorem Measurable.comap_le {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β} :

Measurable f → MeasurableSpace.comap f m₂ ≤ m₁

Alias of the forward direction of measurable_iff_comap_le.

theorem comap_measurable {α : Type u_1} {β : Type u_2} {m : MeasurableSpace β} (f : α → β) :

theorem Measurable.mono {α : Type u_1} {β : Type u_2} {ma : MeasurableSpace α} {ma' : MeasurableSpace α} {mb : MeasurableSpace β} {mb' : MeasurableSpace β} {f : α → β} (hf : Measurable f) (ha : ma ≤ ma') (hb : mb' ≤ mb) :

theorem measurable_id'' {α : Type u_1} {m : MeasurableSpace α} {mα : MeasurableSpace α} (hm : m ≤ mα) :

theorem measurable_from_top {α : Type u_1} {β : Type u_2} [MeasurableSpace β] {f : α → β} :

theorem measurable_generateFrom {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {s : Set (Set β)} {f : α → β} (h : ∀ t ∈ s, MeasurableSet (f ⁻¹' t)) :

theorem Subsingleton.measurable {α : Type u_1} {β : Type u_2} {f : α → β} [MeasurableSpace α] [MeasurableSpace β] [Subsingleton α] :

theorem measurable_of_subsingleton_codomain {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Subsingleton β] (f : α → β) :

theorem measurable_zero {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Zero α] :

theorem measurable_one {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [One α] :

theorem measurable_of_empty {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [IsEmpty α] (f : α → β) :

theorem measurable_of_empty_codomain {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [IsEmpty β] (f : α → β) :

theorem measurable_const' {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : β → α} (hf : ∀ (x y : β), f x = f y) :

A version of measurable_const that assumes f x = f y for all x, y. This version works for functions between empty types.

theorem measurable_natCast {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [NatCast α] (n : ℕ) :

Measurable ↑n

theorem measurable_intCast {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [IntCast α] (n : ℤ) :

Measurable ↑n

theorem measurable_of_countable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] (f : α → β) :

theorem measurable_of_finite {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Finite α] [MeasurableSingletonClass α] (f : α → β) :

theorem Measurable.iterate {α : Type u_1} {m : MeasurableSpace α} {f : α → α} (hf : Measurable f) (n : ℕ) :

Measurable f^[n]

theorem measurableSet_preimage {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {t : Set β} (hf : Measurable f) (ht : MeasurableSet t) :

MeasurableSet (f ⁻¹' t)

theorem MeasurableSet.preimage {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {t : Set β} (ht : MeasurableSet t) (hf : Measurable f) :

MeasurableSet (f ⁻¹' t)

theorem Measurable.piecewise {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {g : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} :

∀ {x : DecidablePred fun (x : α) => x ∈ s}, MeasurableSet s → Measurable f → Measurable g → Measurable (Set.piecewise s f g)

theorem Measurable.ite {α : Type u_1} {β : Type u_2} {f : α → β} {g : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : α → Prop} :

∀ {x : DecidablePred p}, MeasurableSet {a : α | p a} → Measurable f → Measurable g → Measurable fun (x_1 : α) => if p x_1 then f x_1 else g x_1

This is slightly different from Measurable.piecewise. It can be used to show Measurable (ite (x=0) 0 1) by exact Measurable.ite (measurableSet_singleton 0) measurable_const measurable_const, but replacing Measurable.ite by Measurable.piecewise in that example proof does not work.

theorem Measurable.indicator {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [Zero β] (hf : Measurable f) (hs : MeasurableSet s) :

Measurable (Set.indicator s f)

theorem measurable_indicator_const_iff {α : Type u_1} {β : Type u_2} {s : Set α} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [Zero β] [MeasurableSingletonClass β] (b : β) [NeZero b] :

Measurable (Set.indicator s fun (x : α) => b) ↔ MeasurableSet s

The measurability of a set A is equivalent to the measurability of the indicator function which takes a constant value b ≠ 0 on a set A and 0 elsewhere.

theorem measurableSet_support {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [Zero β] [MeasurableSingletonClass β] (hf : Measurable f) :

MeasurableSet (Function.support f)

theorem measurableSet_mulSupport {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [One β] [MeasurableSingletonClass β] (hf : Measurable f) :

MeasurableSet (Function.mulSupport f)

theorem Measurable.measurable_of_countable_ne {α : Type u_1} {β : Type u_2} {f : α → β} {g : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSingletonClass α] (hf : Measurable f) (h : Set.Countable {x : α | f x ≠ g x}) :

If a function coincides with a measurable function outside of a countable set, it is measurable.

instance Empty.instMeasurableSpace :

MeasurableSpace Empty

Equations

Empty.instMeasurableSpace = ⊤

instance PUnit.instMeasurableSpace :

MeasurableSpace PUnit.{u_6 + 1}

Equations

PUnit.instMeasurableSpace = ⊤

instance Bool.instMeasurableSpace :

MeasurableSpace Bool

Equations

Bool.instMeasurableSpace = ⊤

instance Prop.instMeasurableSpace :

MeasurableSpace Prop

Equations

Prop.instMeasurableSpace = ⊤

instance Nat.instMeasurableSpace :

MeasurableSpace ℕ

Equations

Nat.instMeasurableSpace = ⊤

instance Fin.instMeasurableSpace (n : ℕ) :

MeasurableSpace (Fin n)

Equations

Fin.instMeasurableSpace n = ⊤

instance Int.instMeasurableSpace :

MeasurableSpace ℤ

Equations

Int.instMeasurableSpace = ⊤

instance Rat.instMeasurableSpace :

MeasurableSpace ℚ

Equations

Rat.instMeasurableSpace = ⊤

instance Subsingleton.measurableSingletonClass {α : Type u_6} [MeasurableSpace α] [Subsingleton α] :

MeasurableSingletonClass α

Equations

(_ : MeasurableSingletonClass α) = (_ : MeasurableSingletonClass α)

instance Bool.instMeasurableSingletonClass :

MeasurableSingletonClass Bool

Equations

Bool.instMeasurableSingletonClass = (_ : MeasurableSingletonClass Bool)

instance Prop.instMeasurableSingletonClass :

MeasurableSingletonClass Prop

Equations

Prop.instMeasurableSingletonClass = (_ : MeasurableSingletonClass Prop)

instance Nat.instMeasurableSingletonClass :

MeasurableSingletonClass ℕ

Equations

Nat.instMeasurableSingletonClass = (_ : MeasurableSingletonClass ℕ)

instance Fin.instMeasurableSingletonClass (n : ℕ) :

MeasurableSingletonClass (Fin n)

Equations

(_ : MeasurableSingletonClass (Fin n)) = (_ : MeasurableSingletonClass (Fin n))

instance Int.instMeasurableSingletonClass :

MeasurableSingletonClass ℤ

Equations

Int.instMeasurableSingletonClass = (_ : MeasurableSingletonClass ℤ)

instance Rat.instMeasurableSingletonClass :

MeasurableSingletonClass ℚ

Equations

Rat.instMeasurableSingletonClass = (_ : MeasurableSingletonClass ℚ)

theorem measurable_to_countable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Countable α] [MeasurableSpace β] {f : β → α} (h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})) :

theorem measurable_to_countable' {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Countable α] [MeasurableSpace β] {f : β → α} (h : ∀ (x : α), MeasurableSet (f ⁻¹' {x})) :

theorem measurable_unit {α : Type u_1} [MeasurableSpace α] (f : Unit → α) :

instance ULift.instMeasurableSpace {α : Type u_1} [MeasurableSpace α] :

MeasurableSpace (ULift.{u_6, u_1} α)

Equations

ULift.instMeasurableSpace = MeasurableSpace.map ULift.up inst

theorem measurable_down {α : Type u_1} [MeasurableSpace α] :

Measurable ULift.down

theorem measurable_up {α : Type u_1} [MeasurableSpace α] :

Measurable ULift.up

@[simp]

theorem measurableSet_preimage_down {α : Type u_1} [MeasurableSpace α] {s : Set α} :

MeasurableSet (ULift.down ⁻¹' s) ↔ MeasurableSet s

@[simp]

theorem measurableSet_preimage_up {α : Type u_1} [MeasurableSpace α] {s : Set (ULift.{u_6, u_1} α)} :

MeasurableSet (ULift.up ⁻¹' s) ↔ MeasurableSet s

theorem measurable_from_nat {α : Type u_1} [MeasurableSpace α] {f : ℕ → α} :

theorem measurable_to_nat {α : Type u_1} [MeasurableSpace α] {f : α → ℕ} :

(∀ (y : α), MeasurableSet (f ⁻¹' {f y})) → Measurable f

theorem measurable_to_bool {α : Type u_1} [MeasurableSpace α] {f : α → Bool} (h : MeasurableSet (f ⁻¹' {true})) :

theorem measurable_to_prop {α : Type u_1} [MeasurableSpace α] {f : α → Prop} (h : MeasurableSet (f ⁻¹' {True})) :

theorem measurable_findGreatest' {α : Type u_1} [MeasurableSpace α] {p : α → ℕ → Prop} [(x : α) → DecidablePred (p x)] {N : ℕ} (hN : ∀ k ≤ N, MeasurableSet {x : α | Nat.findGreatest (p x) N = k}) :

Measurable fun (x : α) => Nat.findGreatest (p x) N

theorem measurable_findGreatest {α : Type u_1} [MeasurableSpace α] {p : α → ℕ → Prop} [(x : α) → DecidablePred (p x)] {N : ℕ} (hN : ∀ k ≤ N, MeasurableSet {x : α | p x k}) :

Measurable fun (x : α) => Nat.findGreatest (p x) N

theorem measurable_find {α : Type u_1} [MeasurableSpace α] {p : α → ℕ → Prop} [(x : α) → DecidablePred (p x)] (hp : ∀ (x : α), ∃ (N : ℕ), p x N) (hm : ∀ (k : ℕ), MeasurableSet {x : α | p x k}) :

Measurable fun (x : α) => Nat.find (_ : ∃ (N : ℕ), p x N)

instance Quot.instMeasurableSpace {α : Type u_6} {r : α → α → Prop} [m : MeasurableSpace α] :

MeasurableSpace (Quot r)

Equations

Quot.instMeasurableSpace = MeasurableSpace.map (Quot.mk r) m

instance Quotient.instMeasurableSpace {α : Type u_6} {s : Setoid α} [m : MeasurableSpace α] :

MeasurableSpace (Quotient s)

Equations

Quotient.instMeasurableSpace = MeasurableSpace.map Quotient.mk'' m

instance QuotientAddGroup.measurableSpace {G : Type u_6} [AddGroup G] [MeasurableSpace G] (S : AddSubgroup G) :

MeasurableSpace (G ⧸ S)

Equations

QuotientAddGroup.measurableSpace S = Quotient.instMeasurableSpace

instance QuotientGroup.measurableSpace {G : Type u_6} [Group G] [MeasurableSpace G] (S : Subgroup G) :

MeasurableSpace (G ⧸ S)

Equations

QuotientGroup.measurableSpace S = Quotient.instMeasurableSpace

theorem measurableSet_quotient {α : Type u_1} [MeasurableSpace α] {s : Setoid α} {t : Set (Quotient s)} :

MeasurableSet t ↔ MeasurableSet (Quotient.mk'' ⁻¹' t)

theorem measurable_from_quotient {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {s : Setoid α} {f : Quotient s → β} :

Measurable f ↔ Measurable (f ∘ Quotient.mk'')

theorem measurable_quotient_mk' {α : Type u_1} [MeasurableSpace α] [s : Setoid α] :

Measurable Quotient.mk'

theorem measurable_quotient_mk'' {α : Type u_1} [MeasurableSpace α] {s : Setoid α} :

Measurable Quotient.mk''

theorem measurable_quot_mk {α : Type u_1} [MeasurableSpace α] {r : α → α → Prop} :

Measurable (Quot.mk r)

theorem QuotientAddGroup.measurable_coe {G : Type u_6} [AddGroup G] [MeasurableSpace G] {S : AddSubgroup G} :

Measurable QuotientAddGroup.mk

theorem QuotientGroup.measurable_coe {G : Type u_6} [Group G] [MeasurableSpace G] {S : Subgroup G} :

Measurable QuotientGroup.mk

theorem QuotientAddGroup.measurable_from_quotient {α : Type u_1} [MeasurableSpace α] {G : Type u_6} [AddGroup G] [MeasurableSpace G] {S : AddSubgroup G} {f : G ⧸ S → α} :

Measurable f ↔ Measurable (f ∘ QuotientAddGroup.mk)

theorem QuotientGroup.measurable_from_quotient {α : Type u_1} [MeasurableSpace α] {G : Type u_6} [Group G] [MeasurableSpace G] {S : Subgroup G} {f : G ⧸ S → α} :

Measurable f ↔ Measurable (f ∘ QuotientGroup.mk)

instance Subtype.instMeasurableSpace {α : Type u_6} {p : α → Prop} [m : MeasurableSpace α] :

MeasurableSpace (Subtype p)

Equations

Subtype.instMeasurableSpace = MeasurableSpace.comap Subtype.val m

theorem measurable_subtype_coe {α : Type u_1} [MeasurableSpace α] {p : α → Prop} :

Measurable Subtype.val

instance Subtype.instMeasurableSingletonClass {α : Type u_1} [MeasurableSpace α] {p : α → Prop} [MeasurableSingletonClass α] :

MeasurableSingletonClass (Subtype p)

Equations

(_ : MeasurableSingletonClass (Subtype p)) = (_ : MeasurableSingletonClass (Subtype p))

theorem MeasurableSet.of_subtype_image {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set ↑s} (h : MeasurableSet (Subtype.val '' t)) :

MeasurableSet t

theorem MeasurableSet.subtype_image {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set ↑s} (hs : MeasurableSet s) :

MeasurableSet t → MeasurableSet (Subtype.val '' t)

theorem Measurable.subtype_coe {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : β → Prop} {f : α → Subtype p} (hf : Measurable f) :

Measurable fun (a : α) => ↑(f a)

theorem Measurable.subtype_val {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : β → Prop} {f : α → Subtype p} (hf : Measurable f) :

Measurable fun (a : α) => ↑(f a)

Alias of Measurable.subtype_coe.

theorem Measurable.subtype_mk {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : β → Prop} {f : α → β} (hf : Measurable f) {h : ∀ (x : α), p (f x)} :

Measurable fun (x : α) => { val := f x, property := (_ : p (f x)) }

theorem Measurable.rangeFactorization {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : Measurable f) :

Measurable (Set.rangeFactorization f)

theorem Measurable.subtype_map {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} {p : α → Prop} {q : β → Prop} (hf : Measurable f) (hpq : ∀ (x : α), p x → q (f x)) :

Measurable (Subtype.map f hpq)

theorem measurable_inclusion {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set α} (h : s ⊆ t) :

Measurable (Set.inclusion h)

theorem MeasurableSet.image_inclusion' {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set α} (h : s ⊆ t) {u : Set ↑s} (hs : MeasurableSet (Subtype.val ⁻¹' s)) (hu : MeasurableSet u) :

MeasurableSet (Set.inclusion h '' u)

theorem MeasurableSet.image_inclusion {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set α} (h : s ⊆ t) {u : Set ↑s} (hs : MeasurableSet s) (hu : MeasurableSet u) :

MeasurableSet (Set.inclusion h '' u)

theorem MeasurableSet.of_union_cover {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set α} {u : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) (h : Set.univ ⊆ s ∪ t) (hsu : MeasurableSet (Subtype.val ⁻¹' u)) (htu : MeasurableSet (Subtype.val ⁻¹' u)) :

MeasurableSet u

theorem measurable_of_measurable_union_cover {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (s : Set α) (t : Set α) (hs : MeasurableSet s) (ht : MeasurableSet t) (h : Set.univ ⊆ s ∪ t) (hc : Measurable fun (a : ↑s) => f ↑a) (hd : Measurable fun (a : ↑t) => f ↑a) :

theorem measurable_of_restrict_of_restrict_compl {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} {s : Set α} (hs : MeasurableSet s) (h₁ : Measurable (Set.restrict s f)) (h₂ : Measurable (Set.restrict sᶜ f)) :

theorem Measurable.dite {α : Type u_1} {β : Type u_2} {s : Set α} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [(x : α) → Decidable (x ∈ s)] {f : ↑s → β} (hf : Measurable f) {g : ↑sᶜ → β} (hg : Measurable g) (hs : MeasurableSet s) :

Measurable fun (x : α) => if hx : x ∈ s then f { val := x, property := hx } else g { val := x, property := hx }

theorem measurable_of_measurable_on_compl_finite {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSingletonClass α] {f : α → β} (s : Set α) (hs : Set.Finite s) (hf : Measurable (Set.restrict sᶜ f)) :

theorem measurable_of_measurable_on_compl_singleton {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSingletonClass α] {f : α → β} (a : α) (hf : Measurable (Set.restrict {x : α | x ≠ a} f)) :

def MeasurableSpace.prod {α : Type u_6} {β : Type u_7} (m₁ : MeasurableSpace α) (m₂ : MeasurableSpace β) :

MeasurableSpace (α × β)

A MeasurableSpace structure on the product of two measurable spaces.

Equations

MeasurableSpace.prod m₁ m₂ = MeasurableSpace.comap Prod.fst m₁ ⊔ MeasurableSpace.comap Prod.snd m₂

Instances For

instance Prod.instMeasurableSpace {α : Type u_6} {β : Type u_7} [m₁ : MeasurableSpace α] [m₂ : MeasurableSpace β] :

MeasurableSpace (α × β)

Equations

Prod.instMeasurableSpace = MeasurableSpace.prod m₁ m₂

theorem measurable_fst {α : Type u_1} {β : Type u_2} :

∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β}, Measurable Prod.fst

theorem measurable_snd {α : Type u_1} {β : Type u_2} :

∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β}, Measurable Prod.snd

theorem Measurable.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β × γ} (hf : Measurable f) :

Measurable fun (a : α) => (f a).1

theorem Measurable.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β × γ} (hf : Measurable f) :

Measurable fun (a : α) => (f a).2

theorem Measurable.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β × γ} (hf₁ : Measurable fun (a : α) => (f a).1) (hf₂ : Measurable fun (a : α) => (f a).2) :

theorem Measurable.prod_mk {α : Type u_1} {m : MeasurableSpace α} {β : Type u_6} {γ : Type u_7} :

∀ {x : MeasurableSpace β} {x_1 : MeasurableSpace γ} {f : α → β} {g : α → γ}, Measurable f → Measurable g → Measurable fun (a : α) => (f a, g a)

theorem Measurable.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace δ] {f : α → β} {g : γ → δ} (hf : Measurable f) (hg : Measurable g) :

Measurable (Prod.map f g)

theorem measurable_prod_mk_left {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α} :

Measurable (Prod.mk x)

theorem measurable_prod_mk_right {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {y : β} :

Measurable fun (x : α) => (x, y)

theorem Measurable.of_uncurry_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β → γ} (hf : Measurable (Function.uncurry f)) {x : α} :

Measurable (f x)

theorem Measurable.of_uncurry_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β → γ} (hf : Measurable (Function.uncurry f)) {y : β} :

Measurable fun (x : α) => f x y

theorem measurable_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β × γ} :

Measurable f ↔ (Measurable fun (a : α) => (f a).1) ∧ Measurable fun (a : α) => (f a).2

theorem measurable_swap {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} :

Measurable Prod.swap

theorem measurable_swap_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} :

∀ {x : MeasurableSpace γ} {f : α × β → γ}, Measurable (f ∘ Prod.swap) ↔ Measurable f

theorem MeasurableSet.prod {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} {t : Set β} (hs : MeasurableSet s) (ht : MeasurableSet t) :

MeasurableSet (s ×ˢ t)

theorem measurableSet_prod_of_nonempty {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} {t : Set β} (h : Set.Nonempty (s ×ˢ t)) :

MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t

theorem measurableSet_prod {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} {t : Set β} :

MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅

theorem measurableSet_swap_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set (α × β)} :

MeasurableSet (Prod.swap ⁻¹' s) ↔ MeasurableSet s

instance Prod.instMeasurableSingletonClass {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSingletonClass α] [MeasurableSingletonClass β] :

MeasurableSingletonClass (α × β)

Equations

(_ : MeasurableSingletonClass (α × β)) = (_ : MeasurableSingletonClass (α × β))

theorem measurable_from_prod_countable {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable β] [MeasurableSingletonClass β] :

∀ {x : MeasurableSpace γ} {f : α × β → γ}, (∀ (y : β), Measurable fun (x : α) => f (x, y)) → Measurable f

theorem Measurable.find {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} :

∀ {x : MeasurableSpace α} {f : ℕ → α → β} {p : ℕ → α → Prop} [inst : (n : ℕ) → DecidablePred (p n)], (∀ (n : ℕ), Measurable (f n)) → (∀ (n : ℕ), MeasurableSet {x : α | p n x}) → ∀ (h : ∀ (x : α), ∃ (n : ℕ), p n x), Measurable fun (x : α) => f (Nat.find (_ : ∃ (n : ℕ), p n x)) x

A piecewise function on countably many pieces is measurable if all the data is measurable.

theorem measurable_iUnionLift {α : Type u_1} {β : Type u_2} {ι : Sort uι} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] {t : ι → Set α} {f : (i : ι) → ↑(t i) → β} (htf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i { val := x, property := hxi } = f j { val := x, property := hxj }) {T : Set α} (hT : T ⊆ ⋃ (i : ι), t i) (htm : ∀ (i : ι), MeasurableSet (t i)) (hfm : ∀ (i : ι), Measurable (f i)) :

Measurable (Set.iUnionLift t f htf T hT)

Let t i be a countable covering of a set T by measurable sets. Let f i : t i → β be a family of functions that agree on the intersections t i ∩ t j. Then the function Set.iUnionLift t f _ _ : T → β, defined as f i ⟨x, hx⟩ for hx : x ∈ t i, is measurable.

theorem measurable_liftCover {α : Type u_1} {β : Type u_2} {ι : Sort uι} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] (t : ι → Set α) (htm : ∀ (i : ι), MeasurableSet (t i)) (f : (i : ι) → ↑(t i) → β) (hfm : ∀ (i : ι), Measurable (f i)) (hf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i { val := x, property := hxi } = f j { val := x, property := hxj }) (htU : ⋃ (i : ι), t i = Set.univ) :

Measurable (Set.liftCover t f hf htU)

Let t i be a countable covering of α by measurable sets. Let f i : t i → β be a family of functions that agree on the intersections t i ∩ t j. Then the function Set.liftCover t f _ _, defined as f i ⟨x, hx⟩ for hx : x ∈ t i, is measurable.

theorem exists_measurable_piecewise {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {ι : Type u_6} [Countable ι] [Nonempty ι] (t : ι → Set α) (t_meas : ∀ (n : ι), MeasurableSet (t n)) (g : ι → α → β) (hg : ∀ (n : ι), Measurable (g n)) (ht : Pairwise fun (i j : ι) => Set.EqOn (g i) (g j) (t i ∩ t j)) :

∃ (f : α → β), Measurable f ∧ ∀ (n : ι), Set.EqOn f (g n) (t n)

Let t i be a nonempty countable family of measurable sets in α. Let g i : α → β be a family of measurable functions such that g i agrees with g j on t i ∩ t j. Then there exists a measurable function f : α → β that agrees with each g i on t i.

We only need the assumption [Nonempty ι] to prove [Nonempty (α → β)].

@[deprecated exists_measurable_piecewise]

theorem exists_measurable_piecewise_nat {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} {m : MeasurableSpace α} (t : ℕ → Set β) (t_meas : ∀ (n : ℕ), MeasurableSet (t n)) (t_disj : Pairwise (Disjoint on t)) (g : ℕ → β → α) (hg : ∀ (n : ℕ), Measurable (g n)) :

∃ (f : β → α), Measurable f ∧ ∀ (n : ℕ), ∀ x ∈ t n, f x = g n x

Given countably many disjoint measurable sets t n and countably many measurable functions g n, one can construct a measurable function that coincides with g n on t n.

instance MeasurableSpace.pi {δ : Type u_4} {π : δ → Type u_6} [m : (a : δ) → MeasurableSpace (π a)] :

MeasurableSpace ((a : δ) → π a)

Equations

MeasurableSpace.pi = ⨆ (a : δ), MeasurableSpace.comap (fun (b : (a : δ) → π a) => b a) (m a)

theorem measurable_pi_iff {α : Type u_1} {δ : Type u_4} {π : δ → Type u_6} [MeasurableSpace α] [(a : δ) → MeasurableSpace (π a)] {g : α → (a : δ) → π a} :

Measurable g ↔ ∀ (a : δ), Measurable fun (x : α) => g x a

theorem measurable_pi_apply {δ : Type u_4} {π : δ → Type u_6} [(a : δ) → MeasurableSpace (π a)] (a : δ) :

Measurable fun (f : (a : δ) → π a) => f a

theorem Measurable.eval {α : Type u_1} {δ : Type u_4} {π : δ → Type u_6} [MeasurableSpace α] [(a : δ) → MeasurableSpace (π a)] {a : δ} {g : α → (a : δ) → π a} (hg : Measurable g) :

Measurable fun (x : α) => g x a

theorem measurable_pi_lambda {α : Type u_1} {δ : Type u_4} {π : δ → Type u_6} [MeasurableSpace α] [(a : δ) → MeasurableSpace (π a)] (f : α → (a : δ) → π a) (hf : ∀ (a : δ), Measurable fun (c : α) => f c a) :

theorem measurable_update' {δ : Type u_4} {π : δ → Type u_6} [(a : δ) → MeasurableSpace (π a)] {a : δ} [DecidableEq δ] :

Measurable fun (p : ((i : δ) → π i) × π a) => Function.update p.1 a p.2

The function (f, x) ↦ update f a x : (Π a, π a) × π a → Π a, π a is measurable.

theorem measurable_uniqueElim {δ : Type u_4} {π : δ → Type u_6} [Unique δ] [(i : δ) → MeasurableSpace (π i)] :

Measurable uniqueElim

theorem measurable_updateFinset {δ : Type u_4} {π : δ → Type u_6} [(a : δ) → MeasurableSpace (π a)] [DecidableEq δ] {s : Finset δ} {x : (i : δ) → π i} :

Measurable (Function.updateFinset x s)

theorem measurable_update {δ : Type u_4} {π : δ → Type u_6} [(a : δ) → MeasurableSpace (π a)] (f : (a : δ) → π a) {a : δ} [DecidableEq δ] :

Measurable (Function.update f a)

The function update f a : π a → Π a, π a is always measurable. This doesn't require f to be measurable. This should not be confused with the statement that update f a x is measurable.

theorem measurable_update_left {δ : Type u_4} {π : δ → Type u_6} [(a : δ) → MeasurableSpace (π a)] {a : δ} [DecidableEq δ] {x : π a} :

Measurable fun (x_1 : (a : δ) → π a) => Function.update x_1 a x

theorem measurable_eq_mp {δ : Type u_4} (π : δ → Type u_6) [(a : δ) → MeasurableSpace (π a)] {i : δ} {i' : δ} (h : i = i') :

Measurable (Eq.mp (_ : π i = π i'))

theorem Measurable.eq_mp {δ : Type u_4} (π : δ → Type u_6) [(a : δ) → MeasurableSpace (π a)] {β : Type u_7} [MeasurableSpace β] {i : δ} {i' : δ} (h : i = i') {f : β → π i} (hf : Measurable f) :

Measurable fun (x : β) => Eq.mp (_ : π i = π i') (f x)

theorem measurable_piCongrLeft {δ : Type u_4} {δ' : Type u_5} {π : δ → Type u_6} [(a : δ) → MeasurableSpace (π a)] (f : δ' ≃ δ) :

Measurable ⇑(Equiv.piCongrLeft π f)

theorem MeasurableSet.pi {δ : Type u_4} {π : δ → Type u_6} [(a : δ) → MeasurableSpace (π a)] {s : Set δ} {t : (i : δ) → Set (π i)} (hs : Set.Countable s) (ht : ∀ i ∈ s, MeasurableSet (t i)) :

MeasurableSet (Set.pi s t)

theorem MeasurableSet.univ_pi {δ : Type u_4} {π : δ → Type u_6} [(a : δ) → MeasurableSpace (π a)] [Countable δ] {t : (i : δ) → Set (π i)} (ht : ∀ (i : δ), MeasurableSet (t i)) :

MeasurableSet (Set.pi Set.univ t)

theorem measurableSet_pi_of_nonempty {δ : Type u_4} {π : δ → Type u_6} [(a : δ) → MeasurableSpace (π a)] {s : Set δ} {t : (i : δ) → Set (π i)} (hs : Set.Countable s) (h : Set.Nonempty (Set.pi s t)) :

MeasurableSet (Set.pi s t) ↔ ∀ i ∈ s, MeasurableSet (t i)

theorem measurableSet_pi {δ : Type u_4} {π : δ → Type u_6} [(a : δ) → MeasurableSpace (π a)] {s : Set δ} {t : (i : δ) → Set (π i)} (hs : Set.Countable s) :

MeasurableSet (Set.pi s t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ Set.pi s t = ∅

instance Pi.instMeasurableSingletonClass {δ : Type u_4} {π : δ → Type u_6} [(a : δ) → MeasurableSpace (π a)] [Countable δ] [∀ (a : δ), MeasurableSingletonClass (π a)] :

MeasurableSingletonClass ((a : δ) → π a)

Equations

(_ : MeasurableSingletonClass ((a : δ) → π a)) = (_ : MeasurableSingletonClass ((a : δ) → π a))

theorem measurable_piEquivPiSubtypeProd_symm {δ : Type u_4} (π : δ → Type u_6) [(a : δ) → MeasurableSpace (π a)] (p : δ → Prop) [DecidablePred p] :

Measurable ⇑(Equiv.piEquivPiSubtypeProd p π).symm

theorem measurable_piEquivPiSubtypeProd {δ : Type u_4} (π : δ → Type u_6) [(a : δ) → MeasurableSpace (π a)] (p : δ → Prop) [DecidablePred p] :

Measurable ⇑(Equiv.piEquivPiSubtypeProd p π)

instance TProd.instMeasurableSpace {δ : Type u_4} (π : δ → Type u_6) [(x : δ) → MeasurableSpace (π x)] (l : List δ) :

MeasurableSpace (List.TProd π l)

Equations

TProd.instMeasurableSpace π [] = PUnit.instMeasurableSpace
TProd.instMeasurableSpace π (head :: is) = Prod.instMeasurableSpace

theorem measurable_tProd_mk {δ : Type u_4} {π : δ → Type u_6} [(x : δ) → MeasurableSpace (π x)] (l : List δ) :

Measurable (List.TProd.mk l)

theorem measurable_tProd_elim {δ : Type u_4} {π : δ → Type u_6} [(x : δ) → MeasurableSpace (π x)] [DecidableEq δ] {l : List δ} {i : δ} (hi : i ∈ l) :

Measurable fun (v : List.TProd π l) => List.TProd.elim v hi

theorem measurable_tProd_elim' {δ : Type u_4} {π : δ → Type u_6} [(x : δ) → MeasurableSpace (π x)] [DecidableEq δ] {l : List δ} (h : ∀ (i : δ), i ∈ l) :

Measurable (List.TProd.elim' h)

theorem MeasurableSet.tProd {δ : Type u_4} {π : δ → Type u_6} [(x : δ) → MeasurableSpace (π x)] (l : List δ) {s : (i : δ) → Set (π i)} (hs : ∀ (i : δ), MeasurableSet (s i)) :

MeasurableSet (Set.tprod l s)

instance Sum.instMeasurableSpace {α : Type u_6} {β : Type u_7} [m₁ : MeasurableSpace α] [m₂ : MeasurableSpace β] :

MeasurableSpace (α ⊕ β)

Equations

Sum.instMeasurableSpace = MeasurableSpace.map Sum.inl m₁ ⊓ MeasurableSpace.map Sum.inr m₂

theorem measurable_inl {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :

Measurable Sum.inl

theorem measurable_inr {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :

Measurable Sum.inr

theorem measurableSet_sum_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set (α ⊕ β)} :

MeasurableSet s ↔ MeasurableSet (Sum.inl ⁻¹' s) ∧ MeasurableSet (Sum.inr ⁻¹' s)

theorem measurable_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} :

∀ {x : MeasurableSpace γ} {f : α ⊕ β → γ}, Measurable (f ∘ Sum.inl) → Measurable (f ∘ Sum.inr) → Measurable f

theorem Measurable.sumElim {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} :

∀ {x : MeasurableSpace γ} {f : α → γ} {g : β → γ}, Measurable f → Measurable g → Measurable (Sum.elim f g)

theorem Measurable.sumMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m : MeasurableSpace α} {mβ : MeasurableSpace β} :

∀ {x : MeasurableSpace γ} {x_1 : MeasurableSpace δ} {f : α → β} {g : γ → δ}, Measurable f → Measurable g → Measurable (Sum.map f g)

@[simp]

theorem measurableSet_inl_image {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} :

MeasurableSet (Sum.inl '' s) ↔ MeasurableSet s

theorem MeasurableSet.inl_image {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α} :

MeasurableSet s → MeasurableSet (Sum.inl '' s)

Alias of the reverse direction of measurableSet_inl_image.

@[simp]

theorem measurableSet_inr_image {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} :

MeasurableSet (Sum.inr '' s) ↔ MeasurableSet s

theorem MeasurableSet.inr_image {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β} :

MeasurableSet s → MeasurableSet (Sum.inr '' s)

Alias of the reverse direction of measurableSet_inr_image.

theorem measurableSet_range_inl {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} [MeasurableSpace α] :

MeasurableSet (Set.range Sum.inl)

theorem measurableSet_range_inr {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} [MeasurableSpace α] :

MeasurableSet (Set.range Sum.inr)

instance Sigma.instMeasurableSpace {α : Type u_7} {β : α → Type u_6} [m : (a : α) → MeasurableSpace (β a)] :

MeasurableSpace (Sigma β)

Equations

Sigma.instMeasurableSpace = ⨅ (a : α), MeasurableSpace.map (Sigma.mk a) (m a)

@[simp]

theorem measurableSet_setOf {α : Type u_1} [MeasurableSpace α] {p : α → Prop} :

MeasurableSet {a : α | p a} ↔ Measurable p

@[simp]

theorem measurable_mem {α : Type u_1} {s : Set α} [MeasurableSpace α] :

(Measurable fun (x : α) => x ∈ s) ↔ MeasurableSet s

theorem Measurable.setOf {α : Type u_1} [MeasurableSpace α] {p : α → Prop} :

Measurable p → MeasurableSet {a : α | p a}

Alias of the reverse direction of measurableSet_setOf.

theorem MeasurableSet.mem {α : Type u_1} {s : Set α} [MeasurableSpace α] :

MeasurableSet s → Measurable fun (x : α) => x ∈ s

Alias of the reverse direction of measurable_mem.

theorem Measurable.not {α : Type u_1} [MeasurableSpace α] {p : α → Prop} (hp : Measurable p) :

Measurable fun (x : α) => ¬p x

theorem Measurable.and {α : Type u_1} [MeasurableSpace α] {p : α → Prop} {q : α → Prop} (hp : Measurable p) (hq : Measurable q) :

Measurable fun (a : α) => p a ∧ q a

theorem Measurable.or {α : Type u_1} [MeasurableSpace α] {p : α → Prop} {q : α → Prop} (hp : Measurable p) (hq : Measurable q) :

Measurable fun (a : α) => p a ∨ q a

theorem Measurable.imp {α : Type u_1} [MeasurableSpace α] {p : α → Prop} {q : α → Prop} (hp : Measurable p) (hq : Measurable q) :

Measurable fun (a : α) => p a → q a

theorem Measurable.iff {α : Type u_1} [MeasurableSpace α] {p : α → Prop} {q : α → Prop} (hp : Measurable p) (hq : Measurable q) :

Measurable fun (a : α) => p a ↔ q a

theorem Measurable.forall {α : Type u_1} {ι : Sort uι} [MeasurableSpace α] [Countable ι] {p : ι → α → Prop} (hp : ∀ (i : ι), Measurable (p i)) :

Measurable fun (a : α) => ∀ (i : ι), p i a

theorem Measurable.exists {α : Type u_1} {ι : Sort uι} [MeasurableSpace α] [Countable ι] {p : ι → α → Prop} (hp : ∀ (i : ι), Measurable (p i)) :

Measurable fun (a : α) => ∃ (i : ι), p i a

instance Set.instMeasurableSpace {α : Type u_1} :

MeasurableSpace (Set α)

This instance is useful when talking about Bernoulli sequences of random variables or binomial random graphs.

Equations

Set.instMeasurableSpace = id inferInstance

instance Set.instMeasurableSingletonClass {α : Type u_1} [Countable α] :

MeasurableSingletonClass (Set α)

Equations

(_ : MeasurableSingletonClass (Set α)) = (_ : MeasurableSingletonClass (Set α))

theorem measurable_set_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace β] {g : β → Set α} :

Measurable g ↔ ∀ (a : α), Measurable fun (x : β) => a ∈ g x

theorem measurable_set_mem {α : Type u_1} (a : α) :

Measurable fun (s : Set α) => a ∈ s

theorem measurable_set_not_mem {α : Type u_1} (a : α) :

Measurable fun (s : Set α) => a ∉ s

theorem measurableSet_mem {α : Type u_1} (a : α) :

MeasurableSet {s : Set α | a ∈ s}

theorem measurableSet_not_mem {α : Type u_1} (a : α) :

MeasurableSet {s : Set α | a ∉ s}

theorem measurable_compl {α : Type u_1} :

Measurable fun (x : Set α) => xᶜ

@[simp]

theorem MeasurableSpace.generateFrom_singleton {α : Type u_1} (s : Set α) :

MeasurableSpace.generateFrom {s} = MeasurableSpace.comap (fun (x : α) => x ∈ s) ⊤

The sigma-algebra generated by a single set s is {∅, s, sᶜ, univ}.

structure MeasurableEmbedding {α : Type u_6} {β : Type u_7} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) :

A map f : α → β is called a measurable embedding if it is injective, measurable, and sends measurable sets to measurable sets. The latter assumption can be replaced with “f has measurable inverse g : Set.range f → α”, see MeasurableEmbedding.measurable_rangeSplitting, MeasurableEmbedding.of_measurable_inverse_range, and MeasurableEmbedding.of_measurable_inverse.

One more interpretation: f is a measurable embedding if it defines a measurable equivalence to its range and the range is a measurable set. One implication is formalized as MeasurableEmbedding.equivRange; the other one follows from MeasurableEquiv.measurableEmbedding, MeasurableEmbedding.subtype_coe, and MeasurableEmbedding.comp.

injective : Function.Injective f
A measurable embedding is injective.
measurable : Measurable f
A measurable embedding is a measurable function.
measurableSet_image' : ∀ ⦃s : Set α⦄, MeasurableSet s → MeasurableSet (f '' s)
The image of a measurable set under a measurable embedding is a measurable set.

Instances For

theorem MeasurableEmbedding.measurableSet_image {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [MeasurableSpace β] {f : α → β} (hf : MeasurableEmbedding f) {s : Set α} :

MeasurableSet (f '' s) ↔ MeasurableSet s

theorem MeasurableEmbedding.id {α : Type u_1} {mα : MeasurableSpace α} :

MeasurableEmbedding id

theorem MeasurableEmbedding.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {f : α → β} {g : β → γ} (hg : MeasurableEmbedding g) (hf : MeasurableEmbedding f) :

MeasurableEmbedding (g ∘ f)

theorem MeasurableEmbedding.subtype_coe {α : Type u_1} {mα : MeasurableSpace α} {s : Set α} (hs : MeasurableSet s) :

MeasurableEmbedding Subtype.val

theorem MeasurableEmbedding.measurableSet_range {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [MeasurableSpace β] {f : α → β} (hf : MeasurableEmbedding f) :

MeasurableSet (Set.range f)

theorem MeasurableEmbedding.measurableSet_preimage {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [MeasurableSpace β] {f : α → β} (hf : MeasurableEmbedding f) {s : Set β} :

MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ Set.range f)

theorem MeasurableEmbedding.measurable_rangeSplitting {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [MeasurableSpace β] {f : α → β} (hf : MeasurableEmbedding f) :

Measurable (Set.rangeSplitting f)

theorem MeasurableEmbedding.measurable_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {f : α → β} (hf : MeasurableEmbedding f) {g : α → γ} {g' : β → γ} (hg : Measurable g) (hg' : Measurable g') :

Measurable (Function.extend f g g')

theorem MeasurableEmbedding.exists_measurable_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {f : α → β} (hf : MeasurableEmbedding f) {g : α → γ} (hg : Measurable g) (hne : β → Nonempty γ) :

∃ (g' : β → γ), Measurable g' ∧ g' ∘ f = g

theorem MeasurableEmbedding.measurable_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ] {f : α → β} {g : β → γ} (hg : MeasurableEmbedding g) :

Measurable (g ∘ f) ↔ Measurable f

theorem MeasurableSet.exists_measurable_proj {α : Type u_1} :

∀ {x : MeasurableSpace α} {s : Set α}, MeasurableSet s → Set.Nonempty s → ∃ (f : α → ↑s), Measurable f ∧ ∀ (x : ↑s), f ↑x = x

structure MeasurableEquiv (α : Type u_6) (β : Type u_7) [MeasurableSpace α] [MeasurableSpace β] extends Equiv :

Type (max u_6 u_7)

Equivalences between measurable spaces. Main application is the simplification of measurability statements along measurable equivalences.

toFun : α → β
invFun : β → α
left_inv : Function.LeftInverse self.invFun self.toFun
right_inv : Function.RightInverse self.invFun self.toFun
measurable_toFun : Measurable ⇑self.toEquiv
The forward function of a measurable equivalence is measurable.
measurable_invFun : Measurable ⇑self.symm
The inverse function of a measurable equivalence is measurable.

Instances For

def «term_≃ᵐ_» :

Lean.TrailingParserDescr

Equivalences between measurable spaces. Main application is the simplification of measurability statements along measurable equivalences.

Equations

«term_≃ᵐ_» = Lean.ParserDescr.trailingNode `term_≃ᵐ_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ᵐ ") (Lean.ParserDescr.cat `term 26))

Instances For

theorem MeasurableEquiv.toEquiv_injective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :

Function.Injective MeasurableEquiv.toEquiv

instance MeasurableEquiv.instEquivLike {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :

EquivLike (α ≃ᵐ β) α β

Equations

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

@[simp]

theorem MeasurableEquiv.coe_toEquiv {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :

⇑e.toEquiv = ⇑e

theorem MeasurableEquiv.measurable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :

Measurable ⇑e

@[simp]

theorem MeasurableEquiv.coe_mk {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ β) (h1 : Measurable ⇑e) (h2 : Measurable ⇑e.symm) :

⇑{ toEquiv := e, measurable_toFun := h1, measurable_invFun := h2 } = ⇑e

def MeasurableEquiv.refl (α : Type u_6) [MeasurableSpace α] :

α ≃ᵐ α

Any measurable space is equivalent to itself.

Equations

MeasurableEquiv.refl α = { toEquiv := Equiv.refl α, measurable_toFun := (_ : Measurable id), measurable_invFun := (_ : Measurable id) }

Instances For

instance MeasurableEquiv.instInhabited {α : Type u_1} [MeasurableSpace α] :

Inhabited (α ≃ᵐ α)

Equations

MeasurableEquiv.instInhabited = { default := MeasurableEquiv.refl α }

def MeasurableEquiv.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ) :

α ≃ᵐ γ

The composition of equivalences between measurable spaces.

Equations

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

Instances For

theorem MeasurableEquiv.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ) :

⇑(ab.trans bc) = ⇑bc ∘ ⇑ab

def MeasurableEquiv.symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (ab : α ≃ᵐ β) :

β ≃ᵐ α

The inverse of an equivalence between measurable spaces.

Equations

ab.symm = { toEquiv := ab.symm, measurable_toFun := (_ : Measurable ⇑ab.symm), measurable_invFun := (_ : Measurable ⇑ab.toEquiv) }

Instances For

@[simp]

theorem MeasurableEquiv.coe_toEquiv_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :

⇑e.symm = ⇑e.symm

def MeasurableEquiv.Simps.apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (h : α ≃ᵐ β) :

α → β

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations

MeasurableEquiv.Simps.apply h = ⇑h

Instances For

def MeasurableEquiv.Simps.symm_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (h : α ≃ᵐ β) :

β → α

See Note [custom simps projection]

Equations

MeasurableEquiv.Simps.symm_apply h = ⇑h.symm

Instances For

theorem MeasurableEquiv.ext {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {e₁ : α ≃ᵐ β} {e₂ : α ≃ᵐ β} (h : ⇑e₁ = ⇑e₂) :

e₁ = e₂

@[simp]

theorem MeasurableEquiv.symm_mk {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ β) (h1 : Measurable ⇑e) (h2 : Measurable ⇑e.symm) :

{ toEquiv := e, measurable_toFun := h1, measurable_invFun := h2 }.symm = { toEquiv := e.symm, measurable_toFun := h2, measurable_invFun := h1 }

@[simp]

theorem MeasurableEquiv.refl_apply (α : Type u_6) [MeasurableSpace α] (a : α) :

(MeasurableEquiv.refl α) a = a

@[simp]

theorem MeasurableEquiv.trans_toEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ) :

(ab.trans bc).toEquiv = ab.trans bc.toEquiv

@[simp]

theorem MeasurableEquiv.refl_toEquiv (α : Type u_6) [MeasurableSpace α] :

(MeasurableEquiv.refl α).toEquiv = Equiv.refl α

@[simp]

theorem MeasurableEquiv.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ) :

∀ (a : α), (ab.trans bc) a = bc (ab a)

@[simp]

theorem MeasurableEquiv.symm_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :

e.symm.symm = e

theorem MeasurableEquiv.symm_bijective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :

Function.Bijective MeasurableEquiv.symm

@[simp]

theorem MeasurableEquiv.symm_refl (α : Type u_6) [MeasurableSpace α] :

(MeasurableEquiv.refl α).symm = MeasurableEquiv.refl α

@[simp]

theorem MeasurableEquiv.symm_comp_self {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :

⇑e.symm ∘ ⇑e = id

@[simp]

theorem MeasurableEquiv.self_comp_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :

⇑e ∘ ⇑e.symm = id

@[simp]

theorem MeasurableEquiv.apply_symm_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (y : β) :

e (e.symm y) = y

@[simp]

theorem MeasurableEquiv.symm_apply_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (x : α) :

e.symm (e x) = x

@[simp]

theorem MeasurableEquiv.symm_trans_self {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :

e.symm.trans e = MeasurableEquiv.refl β

@[simp]

theorem MeasurableEquiv.self_trans_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :

e.trans e.symm = MeasurableEquiv.refl α

theorem MeasurableEquiv.surjective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :

Function.Surjective ⇑e

theorem MeasurableEquiv.bijective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :

Function.Bijective ⇑e

theorem MeasurableEquiv.injective {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :

Function.Injective ⇑e

@[simp]

theorem MeasurableEquiv.symm_preimage_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set β) :

⇑e.symm ⁻¹' (⇑e ⁻¹' s) = s

theorem MeasurableEquiv.image_eq_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set α) :

⇑e '' s = ⇑e.symm ⁻¹' s

theorem MeasurableEquiv.preimage_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set α) :

⇑e.symm ⁻¹' s = ⇑e '' s

theorem MeasurableEquiv.image_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set β) :

⇑e.symm '' s = ⇑e ⁻¹' s

theorem MeasurableEquiv.eq_image_iff_symm_image_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set β) (t : Set α) :

s = ⇑e '' t ↔ ⇑e.symm '' s = t

@[simp]

theorem MeasurableEquiv.image_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set β) :

⇑e '' (⇑e ⁻¹' s) = s

@[simp]

theorem MeasurableEquiv.preimage_image {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (s : Set α) :

⇑e ⁻¹' (⇑e '' s) = s

@[simp]

theorem MeasurableEquiv.measurableSet_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) {s : Set β} :

MeasurableSet (⇑e ⁻¹' s) ↔ MeasurableSet s

@[simp]

theorem MeasurableEquiv.measurableSet_image {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) {s : Set α} :

MeasurableSet (⇑e '' s) ↔ MeasurableSet s

@[simp]

theorem MeasurableEquiv.map_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :

MeasurableSpace.map (⇑e) inst✝¹ = inst✝

theorem MeasurableEquiv.measurableEmbedding {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) :

MeasurableEmbedding ⇑e

A measurable equivalence is a measurable embedding.

def MeasurableEquiv.cast {α : Type u_6} {β : Type u_6} [i₁ : MeasurableSpace α] [i₂ : MeasurableSpace β] (h : α = β) (hi : HEq i₁ i₂) :

α ≃ᵐ β

Equal measurable spaces are equivalent.

Equations

MeasurableEquiv.cast h hi = { toEquiv := Equiv.cast h, measurable_toFun := (_ : Measurable ⇑(Equiv.cast h)), measurable_invFun := (_ : Measurable ⇑(Equiv.cast h).symm) }

Instances For

def MeasurableEquiv.ulift {α : Type u} [MeasurableSpace α] :

ULift.{v, u} α ≃ᵐ α

Measurable equivalence between ULift α and α.

Equations

MeasurableEquiv.ulift = { toEquiv := Equiv.ulift, measurable_toFun := (_ : Measurable ULift.down), measurable_invFun := (_ : Measurable ULift.up) }

Instances For

theorem MeasurableEquiv.measurable_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {f : β → γ} (e : α ≃ᵐ β) :

Measurable (f ∘ ⇑e) ↔ Measurable f

def MeasurableEquiv.ofUniqueOfUnique (α : Type u_6) (β : Type u_7) [MeasurableSpace α] [MeasurableSpace β] [Unique α] [Unique β] :

α ≃ᵐ β

Any two types with unique elements are measurably equivalent.

Equations

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

Instances For

def MeasurableEquiv.prodCongr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] (ab : α ≃ᵐ β) (cd : γ ≃ᵐ δ) :

α × γ ≃ᵐ β × δ

Products of equivalent measurable spaces are equivalent.

Equations

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

Instances For

def MeasurableEquiv.prodComm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :

α × β ≃ᵐ β × α

Products of measurable spaces are symmetric.

Equations

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

Instances For

def MeasurableEquiv.prodAssoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] :

(α × β) × γ ≃ᵐ α × β × γ

Products of measurable spaces are associative.

Equations

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

Instances For

def MeasurableEquiv.sumCongr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] (ab : α ≃ᵐ β) (cd : γ ≃ᵐ δ) :

α ⊕ γ ≃ᵐ β ⊕ δ

Sums of measurable spaces are symmetric.

Equations

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

Instances For

def MeasurableEquiv.Set.prod {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (s : Set α) (t : Set β) :

↑(s ×ˢ t) ≃ᵐ ↑s × ↑t

s ×ˢ t ≃ (s × t) as measurable spaces.

Equations

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

Instances For

def MeasurableEquiv.Set.univ (α : Type u_6) [MeasurableSpace α] :

↑Set.univ ≃ᵐ α

univ α ≃ α as measurable spaces.

Equations

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

Instances For

def MeasurableEquiv.Set.singleton {α : Type u_1} [MeasurableSpace α] (a : α) :

↑{a} ≃ᵐ Unit

{a} ≃ Unit as measurable spaces.

Equations

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

Instances For

def MeasurableEquiv.Set.rangeInl {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :

↑(Set.range Sum.inl) ≃ᵐ α

α is equivalent to its image in α ⊕ β as measurable spaces.

Equations

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

Instances For

def MeasurableEquiv.Set.rangeInr {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] :

↑(Set.range Sum.inr) ≃ᵐ β

β is equivalent to its image in α ⊕ β as measurable spaces.

Equations

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

Instances For

def MeasurableEquiv.sumProdDistrib (α : Type u_6) (β : Type u_7) (γ : Type u_8) [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] :

(α ⊕ β) × γ ≃ᵐ α × γ ⊕ β × γ

Products distribute over sums (on the right) as measurable spaces.

Equations

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

Instances For

def MeasurableEquiv.prodSumDistrib (α : Type u_6) (β : Type u_7) (γ : Type u_8) [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] :

α × (β ⊕ γ) ≃ᵐ α × β ⊕ α × γ

Products distribute over sums (on the left) as measurable spaces.

Equations

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

Instances For

def MeasurableEquiv.sumProdSum (α : Type u_6) (β : Type u_7) (γ : Type u_8) (δ : Type u_9) [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] :

(α ⊕ β) × (γ ⊕ δ) ≃ᵐ (α × γ ⊕ α × δ) ⊕ β × γ ⊕ β × δ

Products distribute over sums as measurable spaces.

Equations

MeasurableEquiv.sumProdSum α β γ δ = (MeasurableEquiv.sumProdDistrib α β (γ ⊕ δ)).trans (MeasurableEquiv.sumCongr (MeasurableEquiv.prodSumDistrib α γ δ) (MeasurableEquiv.prodSumDistrib β γ δ))

Instances For

def MeasurableEquiv.piCongrRight {δ' : Type u_5} {π : δ' → Type u_6} {π' : δ' → Type u_7} [(x : δ') → MeasurableSpace (π x)] [(x : δ') → MeasurableSpace (π' x)] (e : (a : δ') → π a ≃ᵐ π' a) :

((a : δ') → π a) ≃ᵐ ((a : δ') → π' a)

A family of measurable equivalences Π a, β₁ a ≃ᵐ β₂ a generates a measurable equivalence between Π a, β₁ a and Π a, β₂ a.

Equations

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

Instances For

def MeasurableEquiv.piCongrLeft {δ : Type u_4} {δ' : Type u_5} (π : δ' → Type u_6) [(x : δ') → MeasurableSpace (π x)] (f : δ ≃ δ') :

((b : δ) → π (f b)) ≃ᵐ ((a : δ') → π a)

Moving a dependent type along an equivalence of coordinates, as a measurable equivalence.

Equations

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

Instances For

theorem MeasurableEquiv.coe_piCongrLeft {δ : Type u_4} {δ' : Type u_5} {π : δ' → Type u_6} [(x : δ') → MeasurableSpace (π x)] (f : δ ≃ δ') :

⇑(MeasurableEquiv.piCongrLeft π f) = ⇑(Equiv.piCongrLeft π f)

@[simp]

theorem MeasurableEquiv.piMeasurableEquivTProd_symm_apply {δ' : Type u_5} {π : δ' → Type u_6} [(x : δ') → MeasurableSpace (π x)] [DecidableEq δ'] {l : List δ'} (hnd : List.Nodup l) (h : ∀ (i : δ'), i ∈ l) :

⇑(MeasurableEquiv.piMeasurableEquivTProd hnd h).symm = List.TProd.elim' h

@[simp]

theorem MeasurableEquiv.piMeasurableEquivTProd_apply {δ' : Type u_5} {π : δ' → Type u_6} [(x : δ') → MeasurableSpace (π x)] [DecidableEq δ'] {l : List δ'} (hnd : List.Nodup l) (h : ∀ (i : δ'), i ∈ l) :

⇑(MeasurableEquiv.piMeasurableEquivTProd hnd h) = List.TProd.mk l

def MeasurableEquiv.piMeasurableEquivTProd {δ' : Type u_5} {π : δ' → Type u_6} [(x : δ') → MeasurableSpace (π x)] [DecidableEq δ'] {l : List δ'} (hnd : List.Nodup l) (h : ∀ (i : δ'), i ∈ l) :

((i : δ') → π i) ≃ᵐ List.TProd π l

Pi-types are measurably equivalent to iterated products.

Equations

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

Instances For

@[simp]

theorem MeasurableEquiv.piUnique_apply {δ' : Type u_5} (π : δ' → Type u_6) [(x : δ') → MeasurableSpace (π x)] [Unique δ'] :

⇑(MeasurableEquiv.piUnique π) = fun (f : (i : δ') → π i) => f default

@[simp]

theorem MeasurableEquiv.piUnique_symm_apply {δ' : Type u_5} (π : δ' → Type u_6) [(x : δ') → MeasurableSpace (π x)] [Unique δ'] :

⇑(MeasurableEquiv.piUnique π).symm = uniqueElim

def MeasurableEquiv.piUnique {δ' : Type u_5} (π : δ' → Type u_6) [(x : δ') → MeasurableSpace (π x)] [Unique δ'] :

((i : δ') → π i) ≃ᵐ π default

The measurable equivalence (∀ i, π i) ≃ᵐ π ⋆ when the domain of π only contains ⋆

Equations

MeasurableEquiv.piUnique π = { toEquiv := Equiv.piUnique π, measurable_toFun := (_ : Measurable fun (f : (a : δ') → π a) => f default), measurable_invFun := (_ : Measurable uniqueElim) }

Instances For

@[simp]

theorem MeasurableEquiv.funUnique_apply (α : Type u_8) (β : Type u_9) [Unique α] [MeasurableSpace β] :

⇑(MeasurableEquiv.funUnique α β) = fun (f : α → β) => f default

@[simp]

theorem MeasurableEquiv.funUnique_symm_apply (α : Type u_8) (β : Type u_9) [Unique α] [MeasurableSpace β] :

⇑(MeasurableEquiv.funUnique α β).symm = uniqueElim

def MeasurableEquiv.funUnique (α : Type u_8) (β : Type u_9) [Unique α] [MeasurableSpace β] :

(α → β) ≃ᵐ β

If α has a unique term, then the type of function α → β is measurably equivalent to β.

Equations

MeasurableEquiv.funUnique α β = MeasurableEquiv.piUnique fun (a : α) => β

Instances For

@[simp]

theorem MeasurableEquiv.piFinTwo_apply (α : Fin 2 → Type u_8) [(i : Fin 2) → MeasurableSpace (α i)] :

⇑(MeasurableEquiv.piFinTwo α) = fun (f : (i : Fin 2) → α i) => (f 0, f 1)

@[simp]

theorem MeasurableEquiv.piFinTwo_symm_apply (α : Fin 2 → Type u_8) [(i : Fin 2) → MeasurableSpace (α i)] :

⇑(MeasurableEquiv.piFinTwo α).symm = fun (p : α 0 × α 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)

def MeasurableEquiv.piFinTwo (α : Fin 2 → Type u_8) [(i : Fin 2) → MeasurableSpace (α i)] :

((i : Fin 2) → α i) ≃ᵐ α 0 × α 1

The space Π i : Fin 2, α i is measurably equivalent to α 0 × α 1.

Equations

MeasurableEquiv.piFinTwo α = { toEquiv := piFinTwoEquiv α, measurable_toFun := (_ : Measurable ⇑(piFinTwoEquiv α)), measurable_invFun := (_ : Measurable ⇑(piFinTwoEquiv α).symm) }

Instances For

@[simp]

theorem MeasurableEquiv.finTwoArrow_apply {α : Type u_1} [MeasurableSpace α] :

⇑MeasurableEquiv.finTwoArrow = fun (f : Fin 2 → α) => (f 0, f 1)

@[simp]

theorem MeasurableEquiv.finTwoArrow_symm_apply {α : Type u_1} [MeasurableSpace α] :

⇑MeasurableEquiv.finTwoArrow.symm = fun (p : α × α) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)

def MeasurableEquiv.finTwoArrow {α : Type u_1} [MeasurableSpace α] :

(Fin 2 → α) ≃ᵐ α × α

The space Fin 2 → α is measurably equivalent to α × α.

Equations

MeasurableEquiv.finTwoArrow = MeasurableEquiv.piFinTwo fun (x : Fin 2) => α

Instances For

@[simp]

theorem MeasurableEquiv.piFinSuccAbove_apply {n : ℕ} (α : Fin (n + 1) → Type u_8) [(i : Fin (n + 1)) → MeasurableSpace (α i)] (i : Fin (n + 1)) :

⇑(MeasurableEquiv.piFinSuccAbove α i) = fun (f : (j : Fin (n + 1)) → α j) => (f i, fun (j : Fin n) => f (Fin.succAbove i j))

@[simp]

theorem MeasurableEquiv.piFinSuccAbove_symm_apply {n : ℕ} (α : Fin (n + 1) → Type u_8) [(i : Fin (n + 1)) → MeasurableSpace (α i)] (i : Fin (n + 1)) :

⇑(MeasurableEquiv.piFinSuccAbove α i).symm = fun (f : α i × ((j : Fin n) → α (Fin.succAbove i j))) => Fin.insertNth i f.1 f.2

def MeasurableEquiv.piFinSuccAbove {n : ℕ} (α : Fin (n + 1) → Type u_8) [(i : Fin (n + 1)) → MeasurableSpace (α i)] (i : Fin (n + 1)) :

((j : Fin (n + 1)) → α j) ≃ᵐ α i × ((j : Fin n) → α (Fin.succAbove i j))

Measurable equivalence between Π j : Fin (n + 1), α j and α i × Π j : Fin n, α (Fin.succAbove i j).

Equations

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

Instances For

@[simp]

theorem MeasurableEquiv.piEquivPiSubtypeProd_symm_apply {δ' : Type u_5} (π : δ' → Type u_6) [(x : δ') → MeasurableSpace (π x)] (p : δ' → Prop) [DecidablePred p] :

⇑(MeasurableEquiv.piEquivPiSubtypeProd π p).symm = fun (f : ((i : { x : δ' // p x }) → π ↑i) × ((i : { x : δ' // ¬p x }) → π ↑i)) (x : δ') => if h : p x then f.1 { val := x, property := h } else f.2 { val := x, property := h }

@[simp]

theorem MeasurableEquiv.piEquivPiSubtypeProd_apply {δ' : Type u_5} (π : δ' → Type u_6) [(x : δ') → MeasurableSpace (π x)] (p : δ' → Prop) [DecidablePred p] :

⇑(MeasurableEquiv.piEquivPiSubtypeProd π p) = fun (f : (i : δ') → π i) => (fun (x : { x : δ' // p x }) => f ↑x, fun (x : { x : δ' // ¬p x }) => f ↑x)

def MeasurableEquiv.piEquivPiSubtypeProd {δ' : Type u_5} (π : δ' → Type u_6) [(x : δ') → MeasurableSpace (π x)] (p : δ' → Prop) [DecidablePred p] :

((i : δ') → π i) ≃ᵐ ((i : Subtype p) → π ↑i) × ((i : { i : δ' // ¬p i }) → π ↑i)

Measurable equivalence between (dependent) functions on a type and pairs of functions on {i // p i} and {i // ¬p i}. See also Equiv.piEquivPiSubtypeProd.

Equations

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

Instances For

def MeasurableEquiv.sumPiEquivProdPi {δ : Type u_4} {δ' : Type u_5} (α : δ ⊕ δ' → Type u_8) [(i : δ ⊕ δ') → MeasurableSpace (α i)] :

((i : δ ⊕ δ') → α i) ≃ᵐ ((i : δ) → α (Sum.inl i)) × ((i' : δ') → α (Sum.inr i'))

The measurable equivalence between the pi type over a sum type and a product of pi-types. This is similar to MeasurableEquiv.piEquivPiSubtypeProd.

Equations

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

Instances For

theorem MeasurableEquiv.coe_sumPiEquivProdPi {δ : Type u_4} {δ' : Type u_5} (α : δ ⊕ δ' → Type u_8) [(i : δ ⊕ δ') → MeasurableSpace (α i)] :

⇑(MeasurableEquiv.sumPiEquivProdPi α) = ⇑(Equiv.sumPiEquivProdPi α)

theorem MeasurableEquiv.coe_sumPiEquivProdPi_symm {δ : Type u_4} {δ' : Type u_5} (α : δ ⊕ δ' → Type u_8) [(i : δ ⊕ δ') → MeasurableSpace (α i)] :

⇑(MeasurableEquiv.sumPiEquivProdPi α).symm = ⇑(Equiv.sumPiEquivProdPi α).symm

def MeasurableEquiv.piFinsetUnion {δ' : Type u_5} (π : δ' → Type u_6) [(x : δ') → MeasurableSpace (π x)] [DecidableEq δ'] {s : Finset δ'} {t : Finset δ'} (h : Disjoint s t) :

((i : { x : δ' // x ∈ s }) → π ↑i) × ((i : { x : δ' // x ∈ t }) → π ↑i) ≃ᵐ ((i : { x : δ' // x ∈ s ∪ t }) → π ↑i)

The measurable equivalence (∀ i : s, π i) × (∀ i : t, π i) ≃ᵐ (∀ i : s ∪ t, π i) for disjoint finsets s and t. Equiv.piFinsetUnion as a measurable equivalence.

Equations

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

Instances For

def MeasurableEquiv.sumCompl {α : Type u_1} [MeasurableSpace α] {s : Set α} [DecidablePred fun (x : α) => x ∈ s] (hs : MeasurableSet s) :

↑s ⊕ ↑sᶜ ≃ᵐ α

If s is a measurable set in a measurable space, that space is equivalent to the sum of s and sᶜ.

Equations

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

Instances For

@[simp]

theorem MeasurableEquiv.ofInvolutive_toEquiv {α : Type u_1} [MeasurableSpace α] (f : α → α) (hf : Function.Involutive f) (hf' : Measurable f) :

(MeasurableEquiv.ofInvolutive f hf hf').toEquiv = Function.Involutive.toPerm f hf

def MeasurableEquiv.ofInvolutive {α : Type u_1} [MeasurableSpace α] (f : α → α) (hf : Function.Involutive f) (hf' : Measurable f) :

α ≃ᵐ α

Convert a measurable involutive function f to a measurable permutation with toFun = invFun = f. See also Function.Involutive.toPerm.

Equations

MeasurableEquiv.ofInvolutive f hf hf' = { toEquiv := Function.Involutive.toPerm f hf, measurable_toFun := hf', measurable_invFun := hf' }

Instances For

@[simp]

theorem MeasurableEquiv.ofInvolutive_apply {α : Type u_1} [MeasurableSpace α] (f : α → α) (hf : Function.Involutive f) (hf' : Measurable f) (a : α) :

(MeasurableEquiv.ofInvolutive f hf hf') a = f a

@[simp]

theorem MeasurableEquiv.ofInvolutive_symm {α : Type u_1} [MeasurableSpace α] (f : α → α) (hf : Function.Involutive f) (hf' : Measurable f) :

(MeasurableEquiv.ofInvolutive f hf hf').symm = MeasurableEquiv.ofInvolutive f hf hf'

@[simp]

theorem MeasurableEmbedding.comap_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} (hf : MeasurableEmbedding f) :

MeasurableSpace.comap f inst✝ = inst✝¹

theorem MeasurableEmbedding.iff_comap_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} :

MeasurableEmbedding f ↔ Function.Injective f ∧ MeasurableSpace.comap f inst✝ = inst✝¹ ∧ MeasurableSet (Set.range f)

noncomputable def MeasurableEmbedding.equivImage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} (s : Set α) (hf : MeasurableEmbedding f) :

↑s ≃ᵐ ↑(f '' s)

A set is equivalent to its image under a function f as measurable spaces, if f is a measurable embedding

Equations

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

Instances For

noncomputable def MeasurableEmbedding.equivRange {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} (hf : MeasurableEmbedding f) :

α ≃ᵐ ↑(Set.range f)

The domain of f is equivalent to its range as measurable spaces, if f is a measurable embedding

Equations

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

Instances For

theorem MeasurableEmbedding.of_measurable_inverse_on_range {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} {g : ↑(Set.range f) → α} (hf₁ : Measurable f) (hf₂ : MeasurableSet (Set.range f)) (hg : Measurable g) (H : Function.LeftInverse g (Set.rangeFactorization f)) :

MeasurableEmbedding f

theorem MeasurableEmbedding.of_measurable_inverse {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} {g : β → α} (hf₁ : Measurable f) (hf₂ : MeasurableSet (Set.range f)) (hg : Measurable g) (H : Function.LeftInverse g f) :

MeasurableEmbedding f

noncomputable def MeasurableEmbedding.schroederBernstein {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} {g : β → α} (hf : MeasurableEmbedding f) (hg : MeasurableEmbedding g) :

α ≃ᵐ β

The measurable Schröder-Bernstein Theorem: given measurable embeddings α → β and β → α, we can find a measurable equivalence α ≃ᵐ β.

Equations

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

Instances For

theorem MeasurableSpace.comap_compl {α : Type u_1} {β : Type u_2} {m' : MeasurableSpace β} [BooleanAlgebra β] (h : Measurable compl) (f : α → β) :

MeasurableSpace.comap (fun (a : α) => (f a)ᶜ) inferInstance = MeasurableSpace.comap f inferInstance

@[simp]

theorem MeasurableSpace.comap_not {α : Type u_1} (p : α → Prop) :

MeasurableSpace.comap (fun (a : α) => ¬p a) inferInstance = MeasurableSpace.comap p inferInstance

class MeasurableSpace.CountablyGenerated (α : Type u_1) [m : MeasurableSpace α] :

We say a measurable space is countably generated if it can be generated by a countable set of sets.

isCountablyGenerated : ∃ (b : Set (Set α)), Set.Countable b ∧ m = MeasurableSpace.generateFrom b

Instances

theorem MeasurableSpace.CountablyGenerated.comap {α : Type u_1} {β : Type u_2} [m : MeasurableSpace β] [h : MeasurableSpace.CountablyGenerated β] (f : α → β) :

MeasurableSpace.CountablyGenerated α

theorem MeasurableSpace.CountablyGenerated.sup {β : Type u_2} {m₁ : MeasurableSpace β} {m₂ : MeasurableSpace β} (h₁ : MeasurableSpace.CountablyGenerated β) (h₂ : MeasurableSpace.CountablyGenerated β) :

MeasurableSpace.CountablyGenerated β

instance MeasurableSpace.instCountablyGenerated {α : Type u_1} [MeasurableSpace α] [Finite α] :

MeasurableSpace.CountablyGenerated α

Equations

(_ : MeasurableSpace.CountablyGenerated α) = (_ : MeasurableSpace.CountablyGenerated α)

instance MeasurableSpace.instCountablyGeneratedSubtypeInstMeasurableSpace {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] {p : α → Prop} :

MeasurableSpace.CountablyGenerated { x : α // p x }

Equations

(_ : MeasurableSpace.CountablyGenerated { x : α // p x }) = (_ : MeasurableSpace.CountablyGenerated { x : α // p x })

instance MeasurableSpace.instCountablyGeneratedProdInstMeasurableSpace {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] [MeasurableSpace β] [MeasurableSpace.CountablyGenerated β] :

MeasurableSpace.CountablyGenerated (α × β)

Equations

(_ : MeasurableSpace.CountablyGenerated (α × β)) = (_ : MeasurableSpace.CountablyGenerated (α × β))

instance MeasurableSpace.instHasCountableSeparatingOnMeasurableSet {α : Type u_1} [MeasurableSpace α] {s : Set α} [h : MeasurableSpace.CountablyGenerated ↑s] [MeasurableSingletonClass ↑s] :

HasCountableSeparatingOn α MeasurableSet s

Equations

(_ : HasCountableSeparatingOn α MeasurableSet s) = (_ : HasCountableSeparatingOn α MeasurableSet s)

theorem MeasurableSpace.measurable_injection_nat_bool_of_countablyGenerated (α : Type u_1) [MeasurableSpace α] [HasCountableSeparatingOn α MeasurableSet Set.univ] :

∃ (f : α → ℕ → Bool), Measurable f ∧ Function.Injective f

If a measurable space is countably generated and separates points, it admits a measurable injection into the Cantor space ℕ → Bool (equipped with the product sigma algebra).

class Filter.IsMeasurablyGenerated {α : Type u_1} [MeasurableSpace α] (f : Filter α) :

A filter f is measurably generates if each s ∈ f includes a measurable t ∈ f.

exists_measurable_subset : ∀ ⦃s : Set α⦄, s ∈ f → ∃ t ∈ f, MeasurableSet t ∧ t ⊆ s

Instances

instance Filter.isMeasurablyGenerated_bot {α : Type u_1} [MeasurableSpace α] :

Filter.IsMeasurablyGenerated ⊥

Equations

(_ : Filter.IsMeasurablyGenerated ⊥) = (_ : Filter.IsMeasurablyGenerated ⊥)

instance Filter.isMeasurablyGenerated_top {α : Type u_1} [MeasurableSpace α] :

Filter.IsMeasurablyGenerated ⊤

Equations

(_ : Filter.IsMeasurablyGenerated ⊤) = (_ : Filter.IsMeasurablyGenerated ⊤)

theorem Filter.Eventually.exists_measurable_mem {α : Type u_1} [MeasurableSpace α] {f : Filter α} [Filter.IsMeasurablyGenerated f] {p : α → Prop} (h : ∀ᶠ (x : α) in f, p x) :

∃ s ∈ f, MeasurableSet s ∧ ∀ x ∈ s, p x

theorem Filter.Eventually.exists_measurable_mem_of_smallSets {α : Type u_1} [MeasurableSpace α] {f : Filter α} [Filter.IsMeasurablyGenerated f] {p : Set α → Prop} (h : ∀ᶠ (s : Set α) in Filter.smallSets f, p s) :

∃ s ∈ f, MeasurableSet s ∧ p s

instance Filter.inf_isMeasurablyGenerated {α : Type u_1} [MeasurableSpace α] (f : Filter α) (g : Filter α) [Filter.IsMeasurablyGenerated f] [Filter.IsMeasurablyGenerated g] :

Filter.IsMeasurablyGenerated (f ⊓ g)

Equations

(_ : Filter.IsMeasurablyGenerated (f ⊓ g)) = (_ : Filter.IsMeasurablyGenerated (f ⊓ g))

theorem Filter.principal_isMeasurablyGenerated_iff {α : Type u_1} [MeasurableSpace α] {s : Set α} :

Filter.IsMeasurablyGenerated (Filter.principal s) ↔ MeasurableSet s

theorem MeasurableSet.principal_isMeasurablyGenerated {α : Type u_1} [MeasurableSpace α] {s : Set α} :

MeasurableSet s → Filter.IsMeasurablyGenerated (Filter.principal s)

Alias of the reverse direction of Filter.principal_isMeasurablyGenerated_iff.

instance Filter.iInf_isMeasurablyGenerated {α : Type u_1} {ι : Sort uι} [MeasurableSpace α] {f : ι → Filter α} [∀ (i : ι), Filter.IsMeasurablyGenerated (f i)] :

Filter.IsMeasurablyGenerated (⨅ (i : ι), f i)

Equations

(_ : Filter.IsMeasurablyGenerated (⨅ (i : ι), f i)) = (_ : Filter.IsMeasurablyGenerated (⨅ (i : ι), f i))

def IsCountablySpanning {α : Type u_1} (C : Set (Set α)) :

We say that a collection of sets is countably spanning if a countable subset spans the whole type. This is a useful condition in various parts of measure theory. For example, it is a needed condition to show that the product of two collections generate the product sigma algebra, see generateFrom_prod_eq.

Equations

IsCountablySpanning C = ∃ (s : ℕ → Set α), (∀ (n : ℕ), s n ∈ C) ∧ ⋃ (n : ℕ), s n = Set.univ

Instances For

theorem isCountablySpanning_measurableSet {α : Type u_1} [MeasurableSpace α] :

IsCountablySpanning {s : Set α | MeasurableSet s}

Typeclasses on `Subtype MeasurableSet` #

instance MeasurableSet.Subtype.instMembership {α : Type u_1} [MeasurableSpace α] :

Membership α (Subtype MeasurableSet)

Equations

MeasurableSet.Subtype.instMembership = { mem := fun (a : α) (s : Subtype MeasurableSet) => a ∈ ↑s }

@[simp]

theorem MeasurableSet.mem_coe {α : Type u_1} [MeasurableSpace α] (a : α) (s : Subtype MeasurableSet) :

a ∈ ↑s ↔ a ∈ s

instance MeasurableSet.Subtype.instEmptyCollection {α : Type u_1} [MeasurableSpace α] :

EmptyCollection (Subtype MeasurableSet)

Equations

MeasurableSet.Subtype.instEmptyCollection = { emptyCollection := { val := ∅, property := (_ : MeasurableSet ∅) } }

@[simp]

theorem MeasurableSet.coe_empty {α : Type u_1} [MeasurableSpace α] :

instance MeasurableSet.Subtype.instInsert {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] :

Insert α (Subtype MeasurableSet)

Equations

MeasurableSet.Subtype.instInsert = { insert := fun (a : α) (s : Subtype MeasurableSet) => { val := insert a ↑s, property := (_ : MeasurableSet (insert a ↑s)) } }

@[simp]

theorem MeasurableSet.coe_insert {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) (s : Subtype MeasurableSet) :

↑(insert a s) = insert a ↑s

instance MeasurableSet.Subtype.instSingleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] :

Singleton α (Subtype MeasurableSet)

Equations

MeasurableSet.Subtype.instSingleton = { singleton := fun (a : α) => { val := {a}, property := (_ : MeasurableSet {a}) } }

@[simp]

theorem MeasurableSet.coe_singleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) :

↑{a} = {a}

instance MeasurableSet.Subtype.instIsLawfulSingleton {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] :

IsLawfulSingleton α (Subtype MeasurableSet)

Equations

(_ : IsLawfulSingleton α (Subtype MeasurableSet)) = (_ : IsLawfulSingleton α (Subtype MeasurableSet))

instance MeasurableSet.Subtype.instHasCompl {α : Type u_1} [MeasurableSpace α] :

HasCompl (Subtype MeasurableSet)

Equations

MeasurableSet.Subtype.instHasCompl = { compl := fun (x : Subtype MeasurableSet) => { val := (↑x)ᶜ, property := (_ : MeasurableSet (↑x)ᶜ) } }

@[simp]

theorem MeasurableSet.coe_compl {α : Type u_1} [MeasurableSpace α] (s : Subtype MeasurableSet) :

↑sᶜ = (↑s)ᶜ

instance MeasurableSet.Subtype.instUnion {α : Type u_1} [MeasurableSpace α] :

Union (Subtype MeasurableSet)

Equations

MeasurableSet.Subtype.instUnion = { union := fun (x y : Subtype MeasurableSet) => { val := ↑x ∪ ↑y, property := (_ : MeasurableSet (↑x ∪ ↑y)) } }

@[simp]

theorem MeasurableSet.coe_union {α : Type u_1} [MeasurableSpace α] (s : Subtype MeasurableSet) (t : Subtype MeasurableSet) :

↑(s ∪ t) = ↑s ∪ ↑t

instance MeasurableSet.Subtype.instSup {α : Type u_1} [MeasurableSpace α] :

Sup (Subtype MeasurableSet)

Equations

MeasurableSet.Subtype.instSup = { sup := fun (x y : Subtype MeasurableSet) => x ∪ y }

@[simp]

theorem MeasurableSet.sup_eq_union {α : Type u_1} [MeasurableSpace α] (s : { s : Set α // MeasurableSet s }) (t : { s : Set α // MeasurableSet s }) :

s ⊔ t = s ∪ t

instance MeasurableSet.Subtype.instInter {α : Type u_1} [MeasurableSpace α] :

Inter (Subtype MeasurableSet)

Equations

MeasurableSet.Subtype.instInter = { inter := fun (x y : Subtype MeasurableSet) => { val := ↑x ∩ ↑y, property := (_ : MeasurableSet (↑x ∩ ↑y)) } }

@[simp]

theorem MeasurableSet.coe_inter {α : Type u_1} [MeasurableSpace α] (s : Subtype MeasurableSet) (t : Subtype MeasurableSet) :

↑(s ∩ t) = ↑s ∩ ↑t

instance MeasurableSet.Subtype.instInf {α : Type u_1} [MeasurableSpace α] :

Inf (Subtype MeasurableSet)

Equations

MeasurableSet.Subtype.instInf = { inf := fun (x y : Subtype MeasurableSet) => x ∩ y }

@[simp]

theorem MeasurableSet.inf_eq_inter {α : Type u_1} [MeasurableSpace α] (s : { s : Set α // MeasurableSet s }) (t : { s : Set α // MeasurableSet s }) :

s ⊓ t = s ∩ t

instance MeasurableSet.Subtype.instSDiff {α : Type u_1} [MeasurableSpace α] :

SDiff (Subtype MeasurableSet)

Equations

MeasurableSet.Subtype.instSDiff = { sdiff := fun (x y : Subtype MeasurableSet) => { val := ↑x \ ↑y, property := (_ : MeasurableSet (↑x \ ↑y)) } }

@[simp]

theorem MeasurableSet.coe_sdiff {α : Type u_1} [MeasurableSpace α] (s : Subtype MeasurableSet) (t : Subtype MeasurableSet) :

↑(s \ t) = ↑s \ ↑t

instance MeasurableSet.Subtype.instBot {α : Type u_1} [MeasurableSpace α] :

Bot (Subtype MeasurableSet)

Equations

MeasurableSet.Subtype.instBot = { bot := ∅ }

@[simp]

theorem MeasurableSet.coe_bot {α : Type u_1} [MeasurableSpace α] :

instance MeasurableSet.Subtype.instTop {α : Type u_1} [MeasurableSpace α] :

Top (Subtype MeasurableSet)

Equations

MeasurableSet.Subtype.instTop = { top := { val := Set.univ, property := (_ : MeasurableSet Set.univ) } }

@[simp]

theorem MeasurableSet.coe_top {α : Type u_1} [MeasurableSpace α] :

instance MeasurableSet.Subtype.instBooleanAlgebra {α : Type u_1} [MeasurableSpace α] :

BooleanAlgebra (Subtype MeasurableSet)

Equations

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

theorem MeasurableSet.measurableSet_blimsup {α : Type u_1} [MeasurableSpace α] {s : ℕ → Set α} {p : ℕ → Prop} (h : ∀ (n : ℕ), p n → MeasurableSet (s n)) :

MeasurableSet (Filter.blimsup s Filter.atTop p)

theorem MeasurableSet.measurableSet_bliminf {α : Type u_1} [MeasurableSpace α] {s : ℕ → Set α} {p : ℕ → Prop} (h : ∀ (n : ℕ), p n → MeasurableSet (s n)) :

MeasurableSet (Filter.bliminf s Filter.atTop p)

theorem MeasurableSet.measurableSet_limsup {α : Type u_1} [MeasurableSpace α] {s : ℕ → Set α} (hs : ∀ (n : ℕ), MeasurableSet (s n)) :

MeasurableSet (Filter.limsup s Filter.atTop)

theorem MeasurableSet.measurableSet_liminf {α : Type u_1} [MeasurableSpace α] {s : ℕ → Set α} (hs : ∀ (n : ℕ), MeasurableSet (s n)) :

MeasurableSet (Filter.liminf s Filter.atTop)