Cylinder machinery for the Choquet capacitability proof

Pure combinatorics / topology on ℕ → ℕ: cylinder sets Cyl N n, bounded sets Bnd N, truncation, and the key compactness lemma iInter_closure_image_cyl_eq that says the intersection of closures of cylinder images equals the compact image.

This file is infrastructure for Capacitability.lean.

@[reducible, inline]

abbrev Cyl (N : ℕ → ℕ) (n : ℕ) : Set (ℕ → ℕ)

Cylinder set: {g : ℕ → ℕ | ∀ i ≤ n, g i ≤ N i}.

Equations

• Cyl N n = {g : ℕ → ℕ | ∀ i ≤ n, g i ≤ N i}

@[reducible, inline]

abbrev Bnd (N : ℕ → ℕ) : Set (ℕ → ℕ)

Bounded functions set: {g : ℕ → ℕ | ∀ i, g i ≤ N i}.

Equations

• Bnd N = {g : ℕ → ℕ | ∀ (i : ℕ), g i ≤ N i}

theorem isCompact_bnd (N : ℕ → ℕ) : IsCompact (Bnd N)

theorem bnd_subset_cyl (N : ℕ → ℕ) (n : ℕ) : Bnd N ⊆ Cyl N n

theorem cyl_succ_eq (N : ℕ → ℕ) (n : ℕ) : Cyl N n = ⋃ (k : ℕ), Cyl N n ∩ {g : ℕ → ℕ | g (n + 1) ≤ k}

theorem monotone_cyl_split (N : ℕ → ℕ) (n : ℕ) : Monotone fun (k : ℕ) => Cyl N n ∩ {g : ℕ → ℕ | g (n + 1) ≤ k}

theorem cyl_inter_eq_cyl_update (N : ℕ → ℕ) (n k : ℕ) : Cyl N n ∩ {g : ℕ → ℕ | g (n + 1) ≤ k} = Cyl (Function.update N (n + 1) k) (n + 1)

theorem cyl_ext (N N' : ℕ → ℕ) (n : ℕ) (h : ∀ i ≤ n, N i = N' i) : Cyl N n = Cyl N' n

noncomputable def truncate (N g : ℕ → ℕ) : ℕ → ℕ

Truncation: replace g i by min (g i) (N i) to bring any g into the bounded set.

Equations

• truncate N g i = min (g i) (N i)

theorem truncate_mem_bnd (N g : ℕ → ℕ) : truncate N g ∈ Bnd N

theorem truncate_agree_on_cyl (N : ℕ → ℕ) (n : ℕ) (g : ℕ → ℕ) (hg : g ∈ Cyl N n) (i : ℕ) : i ≤ n → truncate N g i = g i

theorem iInter_closure_image_cyl_eq {α : Type u_1} [TopologicalSpace α] [PolishSpace α] {f : (ℕ → ℕ) → α} (hf : Continuous f) (N : ℕ → ℕ) : ⋂ (n : ℕ), closure (f '' Cyl N n) = f '' Bnd N

The intersection of closures of cylinder images equals the compact image. Key lemma for the capacitability proof: uses truncation and sequential compactness.