Cantor

This file defines the Cantor-space and its components.

Main definitions

• B[h]: The subbasic sets of the Cantor space topology (denoted $B_h$ in the paper).
• B{b}: The subbasic sets extended to sets of the Cantor space topology (denoted $B_b$ in the paper).
• ℬ: The smallest σ-algebra generated by the Cantor-open sets.
• ℬ.cantorSpace: The Cantor space topology.
• ℬ.borel: The Borel measurable space generated from the Cantor space topology.
• ℬ{b}: The smallest Set Algebra generated by {B[h] | h ∈ b} (denoted $ℬ_b$ in the paper).
• A{a,b}: The atoms of ℬ{b}.

The subbasic sets B[h] and B{b}

def ProbNetKAT.B_h {H : Type} (h : H) : Set (Set H)

Equation (1.1)

$$B[h] = \{ c ∣ h ∈ c \}$$

Equations

• B[h] = {c : Set H | h ∈ c}

def ProbNetKAT.B_b {H : Type} (b : Set H) : Set (Set H)

Equation (1.1)

$$B\{b\} = \{ c ∣ b ⊆ c \}$$

Equations

• B{b} = {c : Set H | b ⊆ c}

def ProbNetKAT.«termB[_]» : Lean.ParserDescr

Equation (1.1)

$$B[h] = \{ c ∣ h ∈ c \}$$

Equations

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

def ProbNetKAT.«termB{_}» : Lean.ParserDescr

Equation (1.1)

$$B\{b\} = \{ c ∣ b ⊆ c \}$$

Equations

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

@[simp]

theorem ProbNetKAT.B_b_h_eq_B_h {α✝ : Type} {h : α✝} : B{{h}} = B[h]

@[simp]

theorem ProbNetKAT.B_b_subset_iff {α✝ : Type} {c b : Set α✝} : B{c} ⊆ B{b} ↔ b ⊆ c

Lemma 1. (i)

@[simp]

theorem ProbNetKAT.B_b_union_eq_inter {α✝ : Type} {b c : Set α✝} : B{b ∪ c} = B{b} ∩ B{c}

Lemma 1. (ii)

@[simp]

theorem ProbNetKAT.B_b_empty {H : Type} : B{∅} = Set.univ

Lemma 1. (iii)

def ProbNetKAT.ℬ.cantorSpace {H : Type} : TopologicalSpace (Set H)

The sets B[h] and B[h]ᶜ are the subbasic open sets of the Cantor space topology on 2H.

Equations

• ProbNetKAT.ℬ.cantorSpace = TopologicalSpace.generateFrom ({x : Set (Set H) | ∃ (h : H), B[h] = x} ∪ {x : Set (Set H) | ∃ (h : H), B[h]ᶜ = x})

def ProbNetKAT.ℬ.borel {H : Type} : MeasurableSpace (Set H)

The Borel measurable space generated by the Cantor-topology.

Equations

• ProbNetKAT.ℬ.borel = borel (Set H)

The Set Algebra ℬ

def ProbNetKAT.ℬ {H : Type} : Set (Set (Set H))

The family of Borel sets ℬ is the smallest σ-algebra containing the Cantor-open sets.

The theorem ℬ_is_borel establishes this connection.

Equations

• ProbNetKAT.ℬ = MeasureTheory.generateSetAlgebra TopologicalSpace.IsOpen

@[simp]

theorem ProbNetKAT.ℬ_IsSetAlgebra {H : Type} : MeasureTheory.IsSetAlgebra ℬ

@[simp]

theorem ProbNetKAT.ℬ_IsSetRing {H : Type} : MeasureTheory.IsSetRing ℬ

@[simp]

theorem ProbNetKAT.ℬ_IsSetSemiring {H : Type} : MeasureTheory.IsSetSemiring ℬ

@[simp]

theorem ProbNetKAT.ℬ_mem_empty {H : Type} : ∅ ∈ ℬ

@[simp]

theorem ProbNetKAT.ℬ_mem_univ {H : Type} : Set.univ ∈ ℬ

@[simp]

theorem ProbNetKAT.ℬ_mem_compl {H : Type} {s : Set (Set H)} : sᶜ ∈ ℬ ↔ s ∈ ℬ

@[simp]

theorem ProbNetKAT.ℬ_mem_union {H : Type} {s t : Set (Set H)} : s ∈ ℬ ∧ t ∈ ℬ → s ∪ t ∈ ℬ

@[simp]

theorem ProbNetKAT.ℬ_mem_inter {H : Type} {s t : Set (Set H)} : s ∈ ℬ ∧ t ∈ ℬ → s ∩ t ∈ ℬ

@[simp]

theorem ProbNetKAT.B_b_IsOpen_of_mem {α✝ : Type} {b : α✝} : IsOpen B[b]

All set B[b] are open in the Cantor-space topology.

@[simp]

theorem ProbNetKAT.B_b_IsClosed_of_mem {α✝ : Type} {b : α✝} : IsClosed B[b]

All set B[b] are closed in the Cantor-space topology.

@[simp]

theorem ProbNetKAT.ℬ.isClosed_of_isOpen {α✝ : Type} {S : Set (Set α✝)} (h : IsOpen S) : IsClosed S

@[simp]

theorem ProbNetKAT.ℬ.isClosed_iff_isOpen {α✝ : Type} {S : Set (Set α✝)} : IsClosed S ↔ IsOpen S

From Wikipedia:

Using the union and intersection as operations, the clopen subsets of a given topological space X form a Boolean algebra. Every Boolean algebra can be obtained in this way from a suitable topological space: see Stone's representation theorem for Boolean algebras.

theorem ProbNetKAT.ℬ.IsOpen_of_mem {α✝ : Type} {b : Set (Set α✝)} (h : b ∈ ℬ) : IsOpen b

All set in ℬ are open in the Cantor-space topology.

theorem ProbNetKAT.ℬ_is_borel {α✝ : Type} {S : Set (Set α✝)} : S ∈ ℬ ↔ MeasurableSet S

The family of Borel sets ℬ is the smallest σ-algebra containing the Cantor-open sets.

The Set Algebra ℬ{b}

def ProbNetKAT.ℬ_b {H : Type} (b : Set H) : Set (Set (Set H))

Let ℬ{b} be the Boolean subalgebra of ℬ generated by {B[h] | h ∈ b}.

Equations

• ℬ{b} = MeasureTheory.generateSetAlgebra {x : Set (Set H) | ∃ h ∈ b, B[h] = x}

def ProbNetKAT.«termℬ{_}» : Lean.ParserDescr

Let ℬ{b} be the Boolean subalgebra of ℬ generated by {B[h] | h ∈ b}.

Equations

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

@[simp]

theorem ProbNetKAT.ℬ_b_IsSetAlgebra {α✝ : Type} {b : Set α✝} : MeasureTheory.IsSetAlgebra ℬ{b}

@[simp]

theorem ProbNetKAT.ℬ_b_IsSetRing {α✝ : Type} {b : Set α✝} : MeasureTheory.IsSetRing ℬ{b}

@[simp]

theorem ProbNetKAT.ℬ_b_IsSetSemiring {α✝ : Type} {b : Set α✝} : MeasureTheory.IsSetSemiring ℬ{b}

@[simp]

theorem ProbNetKAT.ℬ_b_mem_empty {H : Type} {b : Set H} : ∅ ∈ ℬ{b}

@[simp]

theorem ProbNetKAT.ℬ_b_mem_univ {H : Type} {b : Set H} : Set.univ ∈ ℬ{b}

@[simp]

theorem ProbNetKAT.ℬ_b_mem_compl {H : Type} {s : Set (Set H)} {b : Set H} : sᶜ ∈ ℬ{b} ↔ s ∈ ℬ{b}

@[simp]

theorem ProbNetKAT.ℬ_b_mem_union {H : Type} {s t : Set (Set H)} {b : Set H} : s ∈ ℬ{b} ∧ t ∈ ℬ{b} → s ∪ t ∈ ℬ{b}

@[simp]

theorem ProbNetKAT.ℬ_b_mem_inter {H : Type} {s t : Set (Set H)} {b : Set H} : s ∈ ℬ{b} ∧ t ∈ ℬ{b} → s ∩ t ∈ ℬ{b}

@[simp]

theorem ProbNetKAT.B_h_mem_ℬ_b_univ {α✝ : Type} {i : α✝} : B[i] ∈ ℬ{Set.univ}

@[simp]

theorem ProbNetKAT.B_h_mem_ℬ_b {α✝ : Type} {b : Set α✝} {i : α✝} (hi : i ∈ b) : B[i] ∈ ℬ{b}

@[simp]

theorem ProbNetKAT.B_h_mem_ℬ {α✝ : Type} {i : α✝} : B[i] ∈ ℬ

theorem ProbNetKAT.ℬ_b_finite_of_finite {α✝ : Type} {b : Set α✝} (h : b.Finite) : ℬ{b}.Finite

If b is finite, so is ℬ{b}.

def ProbNetKAT.℘ω {α : Type u_1} (X : Set α) : Set (Set α)

For a set X, we let ℘ω(X) denote the finite subsets of X.

Equations

• ProbNetKAT.℘ω X = {Y : Set α | Y ⊆ X ∧ Y.Finite}

theorem ProbNetKAT.ℬ_b_eq_iUnion {H : Type} : ℬ{Set.univ} = ⋃ b ∈ ℘ω Set.univ, ℬ{b}

Lemma 1. (iv)

theorem ProbNetKAT.ℬ_b_mem_iff_exists {H : Type} {B : Set (Set H)} : B ∈ ℬ{Set.univ} ↔ ∃ (i : Set H), i.Finite ∧ B ∈ ℬ{i}

The atoms A{a,b}

def ProbNetKAT.A_ab {H : Type} (a b : Set H) : Set (Set H)

The atoms of ℬ{b} are in one-to-one correspondence with the subsets a ⊆ b, the subset a determining which B[h] occur positively in the construction of the atom:

A{a,b} = ⋂ h ∈ a, B[h] ∩ ⋂ h ∈ b \ a, B[h]ᶜ = B{a} \ ⋃ a ⊂ c ∧ c ⊆ b, B{c} = {c | a = c ∩ b}

Formulated in in A_ab_eq₁, A_ab_eq₂, and, A_ab_eq₃.

Equations

• A{a,b} = {c : Set H | a = c ∩ b}

def ProbNetKAT.«termA{_,_}» : Lean.ParserDescr

The atoms of ℬ{b} are in one-to-one correspondence with the subsets a ⊆ b, the subset a determining which B[h] occur positively in the construction of the atom:

A{a,b} = ⋂ h ∈ a, B[h] ∩ ⋂ h ∈ b \ a, B[h]ᶜ = B{a} \ ⋃ a ⊂ c ∧ c ⊆ b, B{c} = {c | a = c ∩ b}

Formulated in in A_ab_eq₁, A_ab_eq₂, and, A_ab_eq₃.

Equations

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

def ProbNetKAT.A_ab_eq₁ {α✝ : Type} {a b : Set α✝} (hab : a ⊆ b) : A{a,b} = (⋂ h ∈ a, B[h]) ∩ ⋂ h ∈ b \ a, B[h]ᶜ

Definition (i) of A{a,b}.

Equations

• ⋯ = ⋯

theorem ProbNetKAT.A_ab_eq₂ {α✝ : Type} {a b : Set α✝} (hab : a ⊆ b) : A{a,b} = B{a} \ ⋃ (c : ↑{c : Set α✝ | a ⊂ c ∧ c ⊆ b}), B{↑c}

Definition (ii) of A{a,b}.

theorem ProbNetKAT.A_ab_eq₃ {α✝ : Type} {a b : Set α✝} (_hab : a ⊆ b) : A{a,b} = {c : Set α✝ | a = c ∩ b}

Definition (iii) of A{a,b}.

@[simp]

theorem ProbNetKAT.A_ab_a_mem {α✝ : Type} {a b : Set α✝} (hab : a ⊆ b) : a ∈ A{a,b}

@[simp]

theorem ProbNetKAT.A_ab_same_eq_B_b {α✝ : Type} {b : Set α✝} : A{b,b} = B{b}

theorem ProbNetKAT.A_ab_mem_ℬ_b {H : Type} {a b : Set H} (hb : b.Finite) (hab : a ⊆ b) : A{a,b} ∈ ℬ{b}

theorem ProbNetKAT.A_ab_mem_ℬ {H : Type} {a b : Set H} (hb : b.Finite) (hab : a ⊆ b) : A{a,b} ∈ ℬ

theorem ProbNetKAT.B_b_eq_iUnion_A_ab {α✝ : Type} {a b : Set α✝} (hab : a ⊆ b) : B{a} = ⋃ c ∈ {c : Set α✝ | a ⊆ c ∧ c ⊆ b}, A{c,b}

Lemma 2.

theorem ProbNetKAT.B_h_eq_iUnion_A_ab {α✝ : Type} {b : Set α✝} {a : α✝} (hab : a ∈ b) : B[a] = ⋃ c ∈ {c : Set α✝ | a ∈ c ∧ c ⊆ b}, A{c,b}

Lemma 2. rephrased for B[h]

def ProbNetKAT.ℬ_b_exists_decomposition {H : Type} {b : Set H} {B : Set (Set H)} (hsb : B ∈ ℬ{b}) (hb : b.Finite) : ∃ (q : Set (Set H)), B = ⋃ a ∈ q, A{a,b} ∧ (q.PairwiseDisjoint fun (x : Set H) => A{x,b}) ∧ q.Finite ∧ ∀ a ∈ q, a ⊆ b

For any B ∈ ℬ{b} there exists finite set of subsets of b, call it q, who's disjoint union satisfies B = ⋃ a ∈ q, A{a,b}.

Equations

• ⋯ = ⋯

theorem ProbNetKAT.A_ab_subset_iff {α✝ : Type} {a b a' b' : Set α✝} (hab : a ⊆ b) (hab' : a' ⊆ b') : A{a,b} ⊆ A{a',b'} ↔ a' ⊆ a ∧ b' \ a' ⊆ b \ a

Lemma 3. (i)

theorem ProbNetKAT.A_ab_rel {α✝ : Type} {a b a' b' : Set α✝} (hab : a ⊆ b) (hab' : a' ⊆ b') : A{a,b} ⊆ A{a',b'} ∨ A{a',b'} ⊆ A{a,b} ∨ A{a,b} ∩ A{a',b'} = ∅

Lemma 3. (ii)