class ConcreteBooleanAlgebra (X : Type u_1) : Type u_1

Definition 1.4.1

• 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)

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

def ConcreteBooleanAlgebra.measurableSets {X : Type u_1} (B : ConcreteBooleanAlgebra X) : Set (Set X)

Equations

• B.measurableSets = {E : Set X | ConcreteBooleanAlgebra.measurable E}

@[implicit_reducible]

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

Example 1.4.3 (the largest algebra)

Equations

• ConcreteBooleanAlgebra.instOrderTop = { top := { measurable := fun (x : Set X) => True, empty_mem := trivial, compl_mem := ⋯, union_mem := ⋯ }, le_top := ⋯ }

@[implicit_reducible]

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

Example 1.4.3 (the smallest algebra)

Equations

• ConcreteBooleanAlgebra.instOrderBot = { bot := { measurable := fun (E : Set X) => E = ∅ ∨ E = Set.univ, empty_mem := ⋯, compl_mem := ⋯, union_mem := ⋯ }, bot_le := ⋯ }

def EuclideanSpace'.elementary_boolean_algebra (d : ℕ) : ConcreteBooleanAlgebra (EuclideanSpace' d)

Exercise 1.4.1 (Elementary algebra)

Equations

• EuclideanSpace'.elementary_boolean_algebra d = { measurable := fun (E : Set (EuclideanSpace' d)) => IsElementary E ∨ IsElementary Eᶜ, empty_mem := ⋯, compl_mem := ⋯, union_mem := ⋯ }

def JordanMeasurable.boolean_algebra (d : ℕ) : ConcreteBooleanAlgebra (EuclideanSpace' d)

Example 1.4.4 (Jordan algebra)

Equations

• JordanMeasurable.boolean_algebra d = { measurable := fun (E : Set (EuclideanSpace' d)) => JordanMeasurable E ∨ JordanMeasurable Eᶜ, empty_mem := ⋯, compl_mem := ⋯, union_mem := ⋯ }

def JordanMeasurable.gt_elementary_boolean_algebra (d : ℕ) : boolean_algebra d ≥ EuclideanSpace'.elementary_boolean_algebra d

Equations

• ⋯ = ⋯

def LebesgueMeasurable.boolean_algebra (d : ℕ) : ConcreteBooleanAlgebra (EuclideanSpace' d)

Example 1.4.5 (Lebesgue algebra)

Equations

• LebesgueMeasurable.boolean_algebra d = { measurable := fun (E : Set (EuclideanSpace' d)) => LebesgueMeasurable E, empty_mem := ⋯, compl_mem := ⋯, union_mem := ⋯ }

def LebesgueMeasurable.gt_jordan_boolean_algebra (d : ℕ) : boolean_algebra d ≥ JordanMeasurable.boolean_algebra d

Equations

• ⋯ = ⋯

def IsNull.boolean_algebra (d : ℕ) : ConcreteBooleanAlgebra (EuclideanSpace' d)

Example 1.4.6 (Null algebra)

Equations

• IsNull.boolean_algebra d = { measurable := fun (E : Set (EuclideanSpace' d)) => IsNull E ∨ IsNull Eᶜ, empty_mem := ⋯, compl_mem := ⋯, union_mem := ⋯ }

def IsNull.lt_lebesgue_boolean_algebra (d : ℕ) : boolean_algebra d ≤ LebesgueMeasurable.boolean_algebra d

Equations

• ⋯ = ⋯

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

Exercise 1.4.2 (Restriction)

Equations

• B.restrict A = { measurable := fun (E : Set ↑A) => ∃ (E' : Set X), ConcreteBooleanAlgebra.measurable E' ∧ E = Subtype.val ⁻¹' E', empty_mem := ⋯, compl_mem := ⋯, union_mem := ⋯ }

def ConcreteBooleanAlgebra.restrict_iff {X : Type u_1} {B : ConcreteBooleanAlgebra X} {A : Set X} (h : measurable A) (E : Set ↑A) : measurable E ↔ measurable (Subtype.val '' E)

Equations

• ⋯ = ⋯

def ConcreteBooleanAlgebra.toBooleanAlgebra {X : Type u_1} (B : ConcreteBooleanAlgebra X) : BooleanAlgebra ↑B.measurableSets

Remark 1.4.2: ConcreteBooleanAlgebras are BooleanAlgebras

Equations

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

def IsPartition {I : Type u_1} {X : Type u_2} (parts : I → Set X) : Prop

Equations

• IsPartition parts = (Set.univ.PairwiseDisjoint parts ∧ ⋃ (i : I), parts i = Set.univ)

def IsPartition.to_ConcreteBooleanAlgebra {I : Type u_1} {X : Type u_2} {atoms : I → Set X} (h_part : IsPartition atoms) : ConcreteBooleanAlgebra X

Example 1.4.7 (Atomic algebra)

Equations

• h_part.to_ConcreteBooleanAlgebra = { measurable := fun (E : Set X) => ∃ (J : Set I), E = ⋃ i ∈ J, atoms i, empty_mem := ⋯, compl_mem := ⋯, union_mem := ⋯ }

def IsPartition.discrete (X : Type u_1) : IsPartition fun (x : X) => {x}

Equations

• ⋯ = ⋯

def ConcreteBooleanAlgebra.top_atomic (X : Type u_1) : ⋯.to_ConcreteBooleanAlgebra = ⊤

Equations

• ⋯ = ⋯

def IsPartition.trivial (X : Type u_1) : IsPartition fun (x : Unit) => Set.univ

Equations

• ⋯ = ⋯

def ConcreteBooleanAlgebra.bot_atomic (X : Type u_1) : ⋯.to_ConcreteBooleanAlgebra = ⊥

Equations

• ⋯ = ⋯

def IsPartition.finer_than {I : Type u_1} {J : Type u_2} {X : Type u_3} {parts_I : I → Set X} {parts_J : J → Set X} : IsPartition parts_I → IsPartition parts_J → Prop

Equations

• x✝¹.finer_than x✝ = ∀ (i : I), ∃ (j : J), parts_I i ⊆ parts_J j

def IsPartition.mono {I : Type u_1} {J : Type u_2} {X : Type u_3} {parts_I : I → Set X} {parts_J : J → Set X} (hI : IsPartition parts_I) (hJ : IsPartition parts_J) (h_finer : hI.finer_than hJ) : hI.to_ConcreteBooleanAlgebra ≥ hJ.to_ConcreteBooleanAlgebra

Equations

• ⋯ = ⋯

def IsPartition.remove_empty {I : Type u_1} {X : Type u_2} {parts : I → Set X} (h_part : IsPartition parts) : IsPartition fun (i : { i : I // parts i ≠ ∅ }) => parts ↑i

Equations

• ⋯ = ⋯

def IsPartition.remove_empty_to_ConcreteBooleanAlgebra {I : Type u_1} {X : Type u_2} {parts : I → Set X} (h_part : IsPartition parts) : h_part.to_ConcreteBooleanAlgebra = ⋯.to_ConcreteBooleanAlgebra

Equations

• ⋯ = ⋯

noncomputable def DyadicCube' {d : ℕ} (n : ℤ) (a : Fin d → ℤ) : Box d

A variant of DyadicCube with BoundedInterval.Ico intervals

Equations

• DyadicCube' n a = { side := fun (i : Fin d) => BoundedInterval.Ico (↑(a i) / 2 ^ n) ((↑(a i) + 1) / 2 ^ n) }

def DyadicCube'.partition (d n : ℕ) : IsPartition fun (a : Fin d → ℤ) => ↑(DyadicCube' (↑n) a)

Example 1.4.8

Equations

• ⋯ = ⋯

def DyadicCube'.boolean_algebra (d n : ℕ) : ConcreteBooleanAlgebra (EuclideanSpace' d)

Equations

• DyadicCube'.boolean_algebra d n = ⋯.to_ConcreteBooleanAlgebra

def DyadicCube'.boolean_algebra_mono (d : ℕ) {m n : ℕ} (h : m ≤ n) : boolean_algebra d m ≤ boolean_algebra d n

Equations

• ⋯ = ⋯

def IsPartition.relabels {I : Type u_1} {J : Type u_2} {X : Type u_3} {parts_I : I → Set X} : IsPartition parts_I → {parts_J : J → Set X} → IsPartition parts_J → Prop

Equations

• x✝¹.relabels x✝ = ∃ (e : I ≃ J), ∀ (i : I), parts_I i = parts_J (e i)

def IsPartition.boolean_algebra_eq_iff {I : Type u_1} {J : Type u_2} {X : Type u_3} {parts_I : I → Set X} {parts_J : J → Set X} (hI : IsPartition parts_I) (hJ : IsPartition parts_J) : hI.to_ConcreteBooleanAlgebra = hJ.to_ConcreteBooleanAlgebra ↔ ⋯.relabels ⋯

Exercise 1.4.3 (Non-empty atoms of an atomic algebra determined up to relabeling)

Equations

• ⋯ = ⋯

def IsPartition.no_empty {I : Type u_1} {X : Type u_2} {parts : I → Set X} : IsPartition parts → Prop

Equations

• x✝.no_empty = ∀ (i : I), parts i ≠ ∅

def IsPartition.boolean_algebra_eq_iff' {I : Type u_1} {J : Type u_2} {X : Type u_3} {parts_I : I → Set X} {parts_J : J → Set X} (hI : IsPartition parts_I) (hJ : IsPartition parts_J) (hIn : hI.no_empty) (hJn : hJ.no_empty) : hI.to_ConcreteBooleanAlgebra = hJ.to_ConcreteBooleanAlgebra ↔ hI.relabels hJ

Equations

• ⋯ = ⋯

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

Equations

• B.isAtomic = ∃ (I : Type ?u.15) (parts : I → Set X) (hI : IsPartition parts), B = hI.to_ConcreteBooleanAlgebra

def ConcreteBooleanAlgebra.atomic_of_finite {X : Type u_1} (B : ConcreteBooleanAlgebra X) (h_fin : B.measurableSets.Finite) : B.isAtomic

Exercise 1.4.4 (Finite boolean algebras are atomic)

Equations

• ⋯ = ⋯

def ConcreteBooleanAlgebra.card_of_finite {X : Type u_1} (B : ConcreteBooleanAlgebra X) (h_fin : B.measurableSets.Finite) : ∃ (n : ℕ), B.measurableSets.ncard = 2 ^ n

Equations

• ⋯ = ⋯

def EuclideanSpace'.elementary_boolean_algebra_not_atomic (d : ℕ) (hd : d ≥ 1) : ¬(elementary_boolean_algebra d).isAtomic

Exercise 1.4.5 (elementary algebra not atomic)

Equations

• ⋯ = ⋯

def JordanMeasurable.boolean_algebra_not_atomic (d : ℕ) (hd : d ≥ 1) : ¬(boolean_algebra d).isAtomic

Exercise 1.4.5 (Jordan algebra not atomic)

Equations

• ⋯ = ⋯

def LebesgueMeasurable.boolean_algebra_not_atomic (d : ℕ) (hd : d ≥ 1) : ¬(boolean_algebra d).isAtomic

Exercise 1.4.5 (Lebesgue algebra not atomic)

Equations

• ⋯ = ⋯

def IsNull.boolean_algebra_not_atomic (d : ℕ) (hd : d ≥ 1) : ¬(boolean_algebra d).isAtomic

Exercise 1.4.5 (Null algebra not atomic)

Equations

• ⋯ = ⋯

@[implicit_reducible]

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

Exercise 1.4.6 (Intersection of algebras)

Equations

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

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

Equations

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

@[implicit_reducible]

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

Definition 1.4.10 (Generation of algebras)

Equations

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

@[implicit_reducible]

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

Equations

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

def ConcreteBooleanAlgebra.generated_by_eq {X : Type u_1} (F : Set (Set X)) : (generated_by F).measurableSets = ⋃ (n : ℕ), Nat.rec F (fun (n : ℕ) (G : (fun (x : ℕ) => Set (Set X)) n) => {E : Set X | (∃ (S : Finset ↑G), E = ⋃ (H : ↥S), ↑↑H) ∨ ∃ (S : Finset ↑G), E = (⋃ (H : ↥S), ↑↑H)ᶜ}) n

Exercise 1.4.9 (Recursive definition of generated Boolean algebra).

Equations

• ⋯ = ⋯