Part I: Bounded branch sets in Baire space

def capBelow (β : ℕ → ℕ) : Set (ℕ → ℕ)

Branches bounded by β everywhere: the compact set Σ(β).

Equations

• capBelow β = {σ : ℕ → ℕ | ∀ (i : ℕ), σ i ≤ β i}

def capBelowN (β : ℕ → ℕ) (n : ℕ) : Set (ℕ → ℕ)

Branches bounded by β on the first n coordinates.

Equations

• capBelowN β n = {σ : ℕ → ℕ | ∀ i < n, σ i ≤ β i}

theorem capBelowN_zero (β : ℕ → ℕ) : capBelowN β 0 = Set.univ

theorem capBelowN_congr {β β' : ℕ → ℕ} {n : ℕ} (h : ∀ i < n, β i = β' i) : capBelowN β n = capBelowN β' n

theorem capBelowN_update_subset (β : ℕ → ℕ) (n k : ℕ) : capBelowN (Function.update β n k) (n + 1) ⊆ capBelowN β n

theorem capBelowN_eq_iUnion_update (β : ℕ → ℕ) (n : ℕ) : capBelowN β n = ⋃ (k : ℕ), capBelowN (Function.update β n k) (n + 1)

theorem monotone_capBelowN_update (β : ℕ → ℕ) (n : ℕ) : Monotone fun (k : ℕ) => capBelowN (Function.update β n k) (n + 1)

theorem capBelow_eq_pi (β : ℕ → ℕ) : capBelow β = Set.univ.pi fun (i : ℕ) => Set.Iic (β i)

theorem isCompact_capBelow (β : ℕ → ℕ) : IsCompact (capBelow β)

def capTrunc (σ : ℕ → ℕ) (n : ℕ) : ℕ → ℕ

Truncation: keep the first n values, zero out the rest.

Equations

• capTrunc σ n i = if i < n then σ i else 0

def capSeqs (β : ℕ → ℕ) (n : ℕ) : Set (ℕ → ℕ)

Normalized representatives of prefixes bounded by β: finitely many.

Equations

• capSeqs β n = {s : ℕ → ℕ | (∀ i < n, s i ≤ β i) ∧ ∀ (i : ℕ), n ≤ i → s i = 0}

theorem capTrunc_mem_capSeqs {β : ℕ → ℕ} {n : ℕ} {σ : ℕ → ℕ} (h : σ ∈ capBelowN β n) : capTrunc σ n ∈ capSeqs β n

theorem capSeqs_finite (β : ℕ → ℕ) (n : ℕ) : (capSeqs β n).Finite

theorem capSeqs_congr {β β' : ℕ → ℕ} {n : ℕ} (h : ∀ i < n, β i = β' i) : capSeqs β n = capSeqs β' n

Part II: The Souslin scheme of a continuous map

def capScheme {Z : Type u_1} [TopologicalSpace Z] (π : (ℕ → ℕ) → Z) (f : ℕ → ℕ) (n : ℕ) : Set Z

The Souslin scheme piece: closure of the image of the cylinder N_{f|n}.

Equations

• capScheme π f n = closure (π '' PiNat.cylinder f n)

theorem capScheme_antitone {Z : Type u_1} [TopologicalSpace Z] (π : (ℕ → ℕ) → Z) (f : ℕ → ℕ) {m n : ℕ} (h : m ≤ n) : capScheme π f n ⊆ capScheme π f m

theorem capScheme_congr {Z : Type u_1} [TopologicalSpace Z] (π : (ℕ → ℕ) → Z) {f g : ℕ → ℕ} {n : ℕ} (h : ∀ i < n, f i = g i) : capScheme π f n = capScheme π g n

theorem capScheme_trunc {Z : Type u_1} [TopologicalSpace Z] (π : (ℕ → ℕ) → Z) (σ : ℕ → ℕ) (n : ℕ) : capScheme π (capTrunc σ n) n = capScheme π σ n

def capW {Z : Type u_1} [TopologicalSpace Z] (π : (ℕ → ℕ) → Z) (β : ℕ → ℕ) (n : ℕ) : Set Z

The n-th bounded approximation: finite union of scheme pieces with prefix bounded by β. Closed.

Equations

• capW π β n = ⋃ s ∈ capSeqs β n, capScheme π s n

theorem isClosed_capW {Z : Type u_1} [TopologicalSpace Z] (π : (ℕ → ℕ) → Z) (β : ℕ → ℕ) (n : ℕ) : IsClosed (capW π β n)

theorem capW_antitone {Z : Type u_1} [TopologicalSpace Z] (π : (ℕ → ℕ) → Z) (β : ℕ → ℕ) : Antitone (capW π β)

theorem capW_congr {Z : Type u_1} [TopologicalSpace Z] (π : (ℕ → ℕ) → Z) {β β' : ℕ → ℕ} {n : ℕ} (h : ∀ i < n, β i = β' i) : capW π β n = capW π β' n

Part III: The core topological lemma

theorem iInter_capW_subset {Z : Type u_2} [TopologicalSpace Z] [PolishSpace Z] {π : (ℕ → ℕ) → Z} (hπ : Continuous π) (β : ℕ → ℕ) : ⋂ (n : ℕ), capW π β n ⊆ π '' capBelow β

Core lemma. For continuous π and any bound β, the decreasing intersection of the bounded approximations is contained in the compact set π '' Σ(β). Proved by subsequence extraction in Σ(β).

Part IV: Branches and the Souslin kernel

def capBranch {Z : Type u_1} [TopologicalSpace Z] (π : (ℕ → ℕ) → Z) (σ : ℕ → ℕ) : Set Z

The branch set along σ: decreasing intersection of scheme pieces.

Equations

• capBranch π σ = ⋂ (n : ℕ), capScheme π σ n

def capKernel {Z : Type u_1} [TopologicalSpace Z] (π : (ℕ → ℕ) → Z) : Set Z

The Souslin kernel 𝒜(G) of the scheme.

Equations

• capKernel π = ⋃ (σ : ℕ → ℕ), capBranch π σ

def capR {Z : Type u_1} [TopologicalSpace Z] (π : (ℕ → ℕ) → Z) (β : ℕ → ℕ) (n : ℕ) : Set Z

Branches whose first n coordinates are bounded by β.

Equations

• capR π β n = ⋃ σ ∈ capBelowN β n, capBranch π σ

theorem capR_zero {Z : Type u_1} [TopologicalSpace Z] (π : (ℕ → ℕ) → Z) (β : ℕ → ℕ) : capR π β 0 = capKernel π

theorem capR_congr {Z : Type u_1} [TopologicalSpace Z] (π : (ℕ → ℕ) → Z) {β β' : ℕ → ℕ} {n : ℕ} (h : ∀ i < n, β i = β' i) : capR π β n = capR π β' n

theorem capR_eq_iUnion_update {Z : Type u_1} [TopologicalSpace Z] (π : (ℕ → ℕ) → Z) (β : ℕ → ℕ) (n : ℕ) : capR π β n = ⋃ (k : ℕ), capR π (Function.update β n k) (n + 1)

theorem monotone_capR_update {Z : Type u_1} [TopologicalSpace Z] (π : (ℕ → ℕ) → Z) (β : ℕ → ℕ) (n : ℕ) : Monotone fun (k : ℕ) => capR π (Function.update β n k) (n + 1)

theorem capR_subset_capW {Z : Type u_1} [TopologicalSpace Z] (π : (ℕ → ℕ) → Z) (β : ℕ → ℕ) (n : ℕ) : capR π β n ⊆ capW π β n

theorem range_subset_capKernel {Z : Type u_1} [TopologicalSpace Z] (π : (ℕ → ℕ) → Z) : Set.range π ⊆ capKernel π

theorem capKernel_eq_range {Z : Type u_2} [TopologicalSpace Z] [PolishSpace Z] {π : (ℕ → ℕ) → Z} (hπ : Continuous π) : capKernel π = Set.range π

The Souslin kernel of the canonical scheme recovers exactly the range: the nontrivial inclusion is via the core lemma with β := σ.

Part V: The bounded recursion

Given a monotone set functional m continuous along increasing countable unions (e.g. an outer measure, or S ↦ κ x (Prod.mk x ⁻¹' S)), if c < m (capKernel π) then one can recursively choose a bound β with c < m (capW π β n) for all n. Mirrors leftmostAuxG from Tree.lean.

theorem cap_exists_ext {Z : Type u_2} [TopologicalSpace Z] (π : (ℕ → ℕ) → Z) (m : Set Z → ENNReal) (hsup : ∀ (s : ℕ → Set Z), Monotone s → m (⋃ (k : ℕ), s k) = ⨆ (k : ℕ), m (s k)) {c : ENNReal} {b : ℕ → ℕ} {n : ℕ} (hb : c < m (capR π b n)) : ∃ (k : ℕ), c < m (capR π (Function.update b n k) (n + 1))

def capAux {Z : Type u_2} [TopologicalSpace Z] (π : (ℕ → ℕ) → Z) (m : Set Z → ENNReal) (hsup : ∀ (s : ℕ → Set Z), Monotone s → m (⋃ (k : ℕ), s k) = ⨆ (k : ℕ), m (s k)) {c : ENNReal} (h0 : c < m (capKernel π)) (n : ℕ) : { b : ℕ → ℕ // c < m (capR π b n) }

Recursive construction of the bound, one coordinate at a time.

Equations

• capAux π m hsup h0 0 = ⟨fun (x : ℕ) => 0, ⋯⟩
• capAux π m hsup h0 n.succ = ⟨Function.update (↑(capAux π m hsup h0 n)) n ⋯.choose, ⋯⟩

noncomputable def capBound {Z : Type u_2} [TopologicalSpace Z] (π : (ℕ → ℕ) → Z) (m : Set Z → ENNReal) (hsup : ∀ (s : ℕ → Set Z), Monotone s → m (⋃ (k : ℕ), s k) = ⨆ (k : ℕ), m (s k)) {c : ENNReal} (h0 : c < m (capKernel π)) (n : ℕ) : ℕ

The diagonal bound.

Equations

• capBound π m hsup h0 n = ↑(capAux π m hsup h0 (n + 1)) n

theorem capAux_eq {Z : Type u_2} [TopologicalSpace Z] (π : (ℕ → ℕ) → Z) (m : Set Z → ENNReal) (hsup : ∀ (s : ℕ → Set Z), Monotone s → m (⋃ (k : ℕ), s k) = ⨆ (k : ℕ), m (s k)) {c : ENNReal} (h0 : c < m (capKernel π)) (n i : ℕ) : i < n → ↑(capAux π m hsup h0 n) i = capBound π m hsup h0 i

theorem cap_exists_bound {Z : Type u_2} [TopologicalSpace Z] (π : (ℕ → ℕ) → Z) (m : Set Z → ENNReal) (hmono : ∀ ⦃S T : Set Z⦄, S ⊆ T → m S ≤ m T) (hsup : ∀ (s : ℕ → Set Z), Monotone s → m (⋃ (k : ℕ), s k) = ⨆ (k : ℕ), m (s k)) {c : ENNReal} (h0 : c < m (capKernel π)) : ∃ (β : ℕ → ℕ), ∀ (n : ℕ), c < m (capW π β n)

Bounded recursion. From c < m (𝒜(G)) produce a bound β with c < m (W(β, n)) for every n.

Part VI: Choquet capacitability for a single finite measure

theorem MeasureTheory.AnalyticSet.measure_eq_iSup_isCompact {X : Type u_2} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] {A : Set X} (hA : AnalyticSet A) (μ : Measure X) [IsFiniteMeasure μ] : μ A = ⨆ (K : Set X), ⨆ (_ : IsCompact K), ⨆ (_ : K ⊆ A), μ K

Choquet capacitability (Kechris 30.13, measure case; BS Prop 7.42): for a finite Borel measure on a Polish space, the (outer) measure of an analytic set is the supremum of the measures of its compact subsets.

theorem MeasureTheory.AnalyticSet.nullMeasurableSet {X : Type u_2} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] {A : Set X} (hA : AnalyticSet A) (μ : Measure X) [IsFiniteMeasure μ] : NullMeasurableSet A μ

Analytic sets are universally measurable (Lusin; BS Prop 7.42): null-measurable with respect to every finite Borel measure.

Part VII: Parametrized capacitability — the kernel key lemma

theorem cap_kernel_exists_bound {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [TopologicalSpace Y] [PolishSpace Y] [MeasurableSpace Y] {π : (ℕ → ℕ) → X × Y} (hπ : Continuous π) (κ : ProbabilityTheory.Kernel X Y) {x : X} {c : ENNReal} (hc : c < (κ x) (Prod.mk x ⁻¹' Set.range π)) : ∃ (β : ℕ → ℕ), ∀ (n : ℕ), c < (κ x) (Prod.mk x ⁻¹' capW π β n)

(b) direction, pointwise: from c < κ x (A_x) produce a bound β controlling all bounded approximations.

theorem cap_kernel_le_of_bound {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [TopologicalSpace Y] [PolishSpace Y] [MeasurableSpace Y] [BorelSpace Y] {π : (ℕ → ℕ) → X × Y} (hπ : Continuous π) (κ : ProbabilityTheory.Kernel X Y) [ProbabilityTheory.IsFiniteKernel κ] {x : X} {c : ENNReal} {β : ℕ → ℕ} (h : ∀ (n : ℕ), c < (κ x) (Prod.mk x ⁻¹' capW π β n)) : c ≤ (κ x) (Prod.mk x ⁻¹' Set.range π)

(a) direction, pointwise: a bound β controlling all approximations forces c ≤ κ x (A_x) (via the core lemma and continuity from above).

def capPad (n : ℕ) (b : Fin n → ℕ) : ℕ → ℕ

Padding a finite tuple into an ℕ-indexed bound.

Equations

• capPad n b i = if h : i < n then b ⟨i, h⟩ else 0

theorem cap_measurable_layer {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [PolishSpace Y] [MeasurableSpace Y] [BorelSpace Y] (π : (ℕ → ℕ) → X × Y) (κ : ProbabilityTheory.Kernel X Y) [ProbabilityTheory.IsSFiniteKernel κ] (q : ENNReal) (n : ℕ) : MeasurableSet {p : X × (ℕ → ℕ) | q < (κ p.1) (Prod.mk p.1 ⁻¹' capW π p.2 n)}

Borel measurability of one layer of the parametrized construction: the bound β acts through finitely many coordinates, so the layer is a countable union of measurable rectangles.

theorem MeasureTheory.AnalyticSet.kernel_section_gt {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [PolishSpace Y] [MeasurableSpace Y] [BorelSpace Y] {A : Set (X × Y)} (hA : AnalyticSet A) (κ : ProbabilityTheory.Kernel X Y) [ProbabilityTheory.IsFiniteKernel κ] (c : ENNReal) : AnalyticSet {x : X | c < (κ x) (Prod.mk x ⁻¹' A)}

Analytic superlevel sets for finite-kernel sections. For A analytic in X × Y and a finite Borel kernel κ, the function x ↦ κ x (A_x) is upper semianalytic: its strict superlevel sets are analytic. This parametrized finite-kernel variant is proved below. For the related probability-measure statement, see Bertsekas–Shreve, Stochastic Optimal Control: The Discrete-Time Case, Corollary 7.43.1, p. 170.