class ConcreteSigmaAlgebra (X : Type u_1) extends ConcreteBooleanAlgebra X : Type u_1

Definition 1.4.12 (Sigma algebra)

• measurable : Set X → Prop
• empty_mem : measurable ∅
• compl_mem (E : Set X) : measurable E → measurable Eᶜ
• union_mem (E F : Set X) : measurable E → measurable F → measurable (E ∪ F)
• countable_union_mem (E : ℕ → Set X) : (∀ (n : ℕ), ConcreteBooleanAlgebra.measurable (E n)) → ConcreteBooleanAlgebra.measurable (⋃ (n : ℕ), E n)

def ConcreteBooleanAlgebra.isSigmaAlgebra {X : Type u_1} (B : ConcreteBooleanAlgebra X) : Prop

Equations

• B.isSigmaAlgebra = ∀ (E : ℕ → Set X), (∀ (n : ℕ), ConcreteBooleanAlgebra.measurable (E n)) → ConcreteBooleanAlgebra.measurable (⋃ (n : ℕ), E n)

theorem ConcreteSigmaAlgebra.isSigmaAlgebra {X : Type u_1} (B : ConcreteSigmaAlgebra X) : B.isSigmaAlgebra

def ConcreteBooleanAlgebra.isSigmaAlgebra.toSigmaAlgebra {X : Type u_1} {B : ConcreteBooleanAlgebra X} (h : B.isSigmaAlgebra) : ConcreteSigmaAlgebra X

Equations

• h.toSigmaAlgebra = { toConcreteBooleanAlgebra := B, countable_union_mem := h }

def ConcreteBooleanAlgebra.isAtomic.isSigmaAlgebra {X : Type u_1} {B : ConcreteBooleanAlgebra X} (h : B.isAtomic) : B.isSigmaAlgebra

Exercise 1.4.10

Equations

• ⋯ = ⋯

theorem LebesgueMeasurable.boolean_algebra.isSigmaAlgebra (d : ℕ) : (boolean_algebra d).isSigmaAlgebra

Exercise 1.4.11

def LebesgueMeasurable.sigmaAlgebra (d : ℕ) : ConcreteSigmaAlgebra (EuclideanSpace' d)

Equations

• LebesgueMeasurable.sigmaAlgebra d = ⋯.toSigmaAlgebra

theorem IsNull.boolean_algebra.isSigmaAlgebra (d : ℕ) : (boolean_algebra d).isSigmaAlgebra

def IsNull.sigmaAlgebra (d : ℕ) : ConcreteSigmaAlgebra (EuclideanSpace' d)

Equations

• IsNull.sigmaAlgebra d = ⋯.toSigmaAlgebra

theorem JordanMeasurable.boolean_algebra.not_isSigmaAlgebra (d : ℕ) (hd : d ≥ 1) : ¬(boolean_algebra d).isSigmaAlgebra

theorem ConcreteSigmaAlgebra.restrict_is_sigma {X : Type u_1} (B : ConcreteSigmaAlgebra X) (A : Set X) : (B.restrict A).isSigmaAlgebra

Exercise 1.4.12

def ConcreteSigmaAlgebra.restrict {X : Type u_1} (B : ConcreteSigmaAlgebra X) (A : Set X) : ConcreteSigmaAlgebra ↑A

Equations

• B.restrict A = ⋯.toSigmaAlgebra

@[implicit_reducible]

instance ConcreteSigmaAlgebra.instLE (X : Type u_1) : LE (ConcreteSigmaAlgebra X)

Equations

• ConcreteSigmaAlgebra.instLE X = { le := fun (B1 B2 : ConcreteSigmaAlgebra X) => ∀ (E : Set X), ConcreteBooleanAlgebra.measurable E → ConcreteBooleanAlgebra.measurable E }

@[implicit_reducible]

instance ConcreteSigmaAlgebra.instPartialOrder (X : Type u_1) : PartialOrder (ConcreteSigmaAlgebra X)

Equations

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

@[implicit_reducible]

instance ConcreteSigmaAlgebra.instOrderTop {X : Type u_1} : OrderTop (ConcreteSigmaAlgebra X)

Equations

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

@[implicit_reducible]

instance ConcreteSigmaAlgebra.instOrderBot {X : Type u_1} : OrderBot (ConcreteSigmaAlgebra X)

Equations

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

@[implicit_reducible]

instance ConcreteSigmaAlgebra.instInfSet {X : Type u_1} : InfSet (ConcreteSigmaAlgebra X)

Exercise 1.4.13 (Intersection of sigma-algebras)

Equations

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

def ConcreteSigmaAlgebra.generated_by {X : Type u_1} (F : Set (Set X)) : ConcreteSigmaAlgebra X

Equations

• ConcreteSigmaAlgebra.generated_by F = sInf {B : ConcreteSigmaAlgebra X | ∀ E ∈ F, ConcreteBooleanAlgebra.measurable E}

@[implicit_reducible]

instance ConcreteSigmaAlgebra.instSupSet {X : Type u_1} : SupSet (ConcreteSigmaAlgebra X)

Definition 1.4.14 (Generation of σ-algebras)

Equations

• ConcreteSigmaAlgebra.instSupSet = { sSup := fun (S : Set (ConcreteSigmaAlgebra X)) => ConcreteSigmaAlgebra.generated_by (⋃ B ∈ S, B.measurableSets) }

@[implicit_reducible]

instance ConcreteSigmaAlgebra.instCompleteLattice {X : Type u_1} : CompleteLattice (ConcreteSigmaAlgebra X)

Equations

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

theorem ConcreteSigmaAlgebra.generated_by_le {X : Type u_1} (F : Set (Set X)) : ConcreteBooleanAlgebra.generated_by F ≤ (generated_by F).toConcreteBooleanAlgebra

theorem ConcreteSigmaAlgebra.induction {X : Type u_1} {F : Set (Set X)} {P : Set X → Prop} (h1 : P ∅) (h2 : ∀ E ∈ F, P E) (h3 : ∀ (E : Set X), P E → P Eᶜ) (h4 : ∀ (E : ℕ → Set X), (∀ (n : ℕ), P (E n)) → P (⋃ (n : ℕ), E n)) (E : Set X) : ConcreteBooleanAlgebra.measurable E → P E

Remark 1.4.15

def BorelSigmaAlgebra (X : Type u_1) [TopologicalSpace X] : ConcreteSigmaAlgebra X

Definition 1.4.16 (Borel σ-algebra)

Equations

• BorelSigmaAlgebra X = ConcreteSigmaAlgebra.generated_by {U : Set X | IsOpen U}

theorem BorelSigmaAlgebra.generated_by_open (d : ℕ) : BorelSigmaAlgebra (EuclideanSpace' d) = ConcreteSigmaAlgebra.generated_by {U : Set (EuclideanSpace' d) | IsOpen U}

Exercise 1.4.14 (i)

theorem BorelSigmaAlgebra.generated_by_closed (d : ℕ) : BorelSigmaAlgebra (EuclideanSpace' d) = ConcreteSigmaAlgebra.generated_by {F : Set (EuclideanSpace' d) | IsClosed F}

Exercise 1.4.14 (ii)

theorem BorelSigmaAlgebra.generated_by_compact (d : ℕ) : BorelSigmaAlgebra (EuclideanSpace' d) = ConcreteSigmaAlgebra.generated_by {K : Set (EuclideanSpace' d) | IsCompact K}

Exercise 1.4.14 (iii)

theorem BorelSigmaAlgebra.generated_by_open_balls (d : ℕ) : BorelSigmaAlgebra (EuclideanSpace' d) = ConcreteSigmaAlgebra.generated_by {B : Set (EuclideanSpace' d) | ∃ (x₀ : EuclideanSpace' d) (r : ℝ), B = Metric.ball x₀ r}

Exercise 1.4.14 (iv)

theorem BorelSigmaAlgebra.generated_by_boxes (d : ℕ) : BorelSigmaAlgebra (EuclideanSpace' d) = ConcreteSigmaAlgebra.generated_by (Box.toSet '' Set.univ)

Exercise 1.4.14 (v)

theorem BorelSigmaAlgebra.generated_by_elementary (d : ℕ) : BorelSigmaAlgebra (EuclideanSpace' d) = ConcreteSigmaAlgebra.generated_by {E : Set (EuclideanSpace' d) | IsElementary E}

Exercise 1.4.14 (vi)

def ConcreteSigmaAlgebra.generated_by_eq {X : Type u_1} (F : Set (Set X)) : (generated_by F).measurableSets = ⋃ (α : Ordinal.{u_2}), ⋃ (_ : α < Ordinal.omega 1), Ordinal.limitRecOn α F (fun (n : Ordinal.{u_2}) (G : (fun (x : Ordinal.{u_2}) => Set (Set X)) n) => {E : Set X | (∃ (S : Set ↑G), Countable ↑S ∧ E = ⋃ (H : ↑S), ↑↑H) ∨ ∃ (S : Set ↑G), Countable ↑S ∧ E = (⋃ (H : ↑S), ↑↑H)ᶜ}) fun (α : Ordinal.{u_2}) (x : Order.IsSuccLimit α) (G : (o' : Ordinal.{u_2}) → o' < α → (fun (x : Ordinal.{u_2}) => Set (Set X)) o') => ⋃ (β : Ordinal.{u_2}), ⋃ (h : β < α), G β h

Exercise 1.4.15 (Recursive definition of generated sigma-algebra).

Equations

• ⋯ = ⋯

theorem ConcreteSigmaAlgebra.card_of_generated_by {X : Type u_1} {F : Set (Set X)} [Infinite ↑F] : Cardinal.mk ↑(generated_by F).measurableSets ≤ Cardinal.mk ↑F ^ Cardinal.aleph0

Exercise 1.4.16

theorem BorelSigmaAlgebra.card (d : ℕ) : Cardinal.mk ↑(BorelSigmaAlgebra (EuclideanSpace' d)).measurableSets ≤ 2 ^ Cardinal.aleph0

theorem JordanMeasurable.not_borel {d : ℕ} (hd : d ≥ 1) : ∃ (E : Set (EuclideanSpace' d)), JordanMeasurable E ∧ ¬ConcreteBooleanAlgebra.measurable E

theorem BorelSigmaAlgebra.prod {d₁ d₂ : ℕ} {E : Set (EuclideanSpace' d₁)} {F : Set (EuclideanSpace' d₂)} (hE : ConcreteBooleanAlgebra.measurable E) (hF : ConcreteBooleanAlgebra.measurable F) : ConcreteBooleanAlgebra.measurable (⇑(EuclideanSpace'.prod_equiv d₁ d₂).symm '' E ×ˢ F)

Exercise 1.4.17

theorem BorelSigmaAlgebra.slice_fst {d₁ d₂ : ℕ} {E : Set (EuclideanSpace' (d₁ + d₂))} (hE : ConcreteBooleanAlgebra.measurable E) (x₂ : EuclideanSpace' d₂) : ConcreteBooleanAlgebra.measurable {x₁ : EuclideanSpace' d₁ | (EuclideanSpace'.prod_equiv d₁ d₂).symm (x₁, x₂) ∈ E}

Exercise 1.4.18(i) (slice along first factor).

theorem BorelSigmaAlgebra.slice_snd {d₁ d₂ : ℕ} {E : Set (EuclideanSpace' (d₁ + d₂))} (hE : ConcreteBooleanAlgebra.measurable E) (x₁ : EuclideanSpace' d₁) : ConcreteBooleanAlgebra.measurable {x₂ : EuclideanSpace' d₂ | (EuclideanSpace'.prod_equiv d₁ d₂).symm (x₁, x₂) ∈ E}

Exercise 1.4.18(i) (slice along second factor).

theorem LebesgueMeasurable.sigmaAlgebra_generated_by {d : ℕ} : sigmaAlgebra d = ConcreteSigmaAlgebra.generated_by ((BorelSigmaAlgebra (EuclideanSpace' d)).measurableSets ∪ (IsNull.sigmaAlgebra d).measurableSets)

Exercise 1.4.19

def ConcreteSigmaAlgebra.measurableSpace {X : Type u_1} (B : ConcreteSigmaAlgebra X) : MeasurableSpace X

Equations

• B.measurableSpace = { MeasurableSet' := ConcreteBooleanAlgebra.measurable, measurableSet_empty := ⋯, measurableSet_compl := ⋯, measurableSet_iUnion := ⋯ }

def MeasurableSpace.sigmaAlgebra {X : Type u_1} (M : MeasurableSpace X) : ConcreteSigmaAlgebra X

Equations

• M.sigmaAlgebra = { measurable := MeasurableSpace.MeasurableSet' M, empty_mem := ⋯, compl_mem := ⋯, union_mem := ⋯, countable_union_mem := ⋯ }

theorem BorelSigmaAlgebra.le_LebesgueSigmaAlgebra (d : ℕ) : BorelSigmaAlgebra (EuclideanSpace' d) ≤ LebesgueMeasurable.sigmaAlgebra d

def ConcreteSigmaAlgebra.toMeasurableSpace {X : Type u_1} (B : ConcreteSigmaAlgebra X) : MeasurableSpace X

Equations

• B.toMeasurableSpace = B.measurableSpace

def MeasurableSpace.toConcreteSigmaAlgebra {X : Type u_1} (M : MeasurableSpace X) : ConcreteSigmaAlgebra X

Equations

• M.toConcreteSigmaAlgebra = M.sigmaAlgebra