Choquet capacitability. For analytic sets, capacity equals the supremum over compact subsets (Kechris 30.13).
DeclMeasureTheory.AnalyticSet.cap_eq_iSup_isCompact
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] [PolishSpace α]
{cap : Set α → ENNReal},
MeasureTheory.IsChoquetCapacity cap →
∀ {s : Set α}, MeasureTheory.AnalyticSet s → cap s = ⨆ K, ⨆ (_ : IsCompact K), ⨆ (_ : K ⊆ s), cap KTopicAnalytic sets
ThesisStepHypothesisDefinition
- DeclMeasureTheory.AnalyticSet.cap_eq_iSup_isCompactDeclaration kindtheorem
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] [PolishSpace α] {cap : Set α → ENNReal}, MeasureTheory.IsChoquetCapacity cap → ∀ {s : Set α}, MeasureTheory.AnalyticSet s → cap s = ⨆ K, ⨆ (_ : IsCompact K), ⨆ (_ : K ⊆ s), cap K - Declmonotone_cyl_splitDeclaration kindtheorem
∀ (N : ℕ → ℕ) (n : ℕ), Monotone fun k => Cyl N n ∩ {g | g (n + 1) ≤ k} - DecliInter_closure_image_cyl_eqDeclaration kindtheorem
The intersection of closures of cylinder images equals the compact image. Key lemma for the capacitability proof: uses truncation and sequential compactness.
∀ {α : Type u_1} [inst : TopologicalSpace α] [PolishSpace α] {f : (ℕ → ℕ) → α}, Continuous f → ∀ (N : ℕ → ℕ), ⋂ n, closure (f '' Cyl N n) = f '' Bnd N - Decltruncate_mem_bndDeclaration kindtheorem
∀ (N g : ℕ → ℕ), choquetTruncate N g ∈ Bnd N
Used by
- Decltruncate_agree_on_cylDeclaration kindtheorem
∀ (N : ℕ → ℕ) (n : ℕ), ∀ g ∈ Cyl N n, ∀ i ≤ n, choquetTruncate N g i = g i
Used by
- DeclisCompact_bndDeclaration kindtheorem
∀ (N : ℕ → ℕ), IsCompact (Bnd N)
- Declbnd_subset_cylDeclaration kindtheorem
∀ (N : ℕ → ℕ) (n : ℕ), Bnd N ⊆ Cyl N n
Used by
- Declcyl_succ_eqDeclaration kindtheorem
∀ (N : ℕ → ℕ) (n : ℕ), Cyl N n = ⋃ k, Cyl N n ∩ {g | g (n + 1) ≤ k} - Declcyl_inter_eq_cyl_updateDeclaration kindtheorem
∀ (N : ℕ → ℕ) (n k : ℕ), Cyl N n ∩ {g | g (n + 1) ≤ k} = Cyl (Function.update N (n + 1) k) (n + 1) - Declcyl_extDeclaration kindtheorem
∀ (N N' : ℕ → ℕ) (n : ℕ), (∀ i ≤ n, N i = N' i) → Cyl N n = Cyl N' n
- DeclMeasureTheory.IsChoquetCapacity.monoDeclaration kindtheorem
∀ {α : Type u_1} [inst : TopologicalSpace α] {cap : Set α → ENNReal}, MeasureTheory.IsChoquetCapacity cap → ∀ {s t : Set α}, s ⊆ t → cap s ≤ cap t - DeclMeasureTheory.IsChoquetCapacity.iUnion_natDeclaration kindtheorem
∀ {α : Type u_1} [inst : TopologicalSpace α] {cap : Set α → ENNReal}, MeasureTheory.IsChoquetCapacity cap → ∀ (f : ℕ → Set α), Monotone f → cap (⋃ n, f n) = ⨆ n, cap (f n) - DeclMeasureTheory.IsChoquetCapacity.iInter_closedDeclaration kindtheorem
∀ {α : Type u_1} [inst : TopologicalSpace α] {cap : Set α → ENNReal}, MeasureTheory.IsChoquetCapacity cap → ∀ (f : ℕ → Set α), Antitone f → (∀ (n : ℕ), IsClosed (f n)) → cap (⋂ n, f n) = ⨅ n, cap (f n) - Hypothesishcap
MeasureTheory.IsChoquetCapacity cap
- Hypothesishs
MeasureTheory.AnalyticSet s
- DefinitionBnddef
Bounded functions set:
{g : ℕ → ℕ | ∀ i, g i ≤ N i}.(ℕ → ℕ) → Set (ℕ → ℕ)
- DefinitionCyldef
Cylinder set:
{g : ℕ → ℕ | ∀ i ≤ n, g i ≤ N i}.(ℕ → ℕ) → ℕ → Set (ℕ → ℕ)
- DefinitionMeasureTheory.IsChoquetCapacitystructure
Bundled record of the three Choquet capacity axioms: monotonicity, sequential continuity from below along increasing unions, and sequential continuity from above along decreasing intersections of closed sets. The third axiom distinguishes a capacity from a general outer measure.
{α : Type u_1} → [TopologicalSpace α] → (Set α → ENNReal) → Prop - DefinitionchoquetTruncatedef
Truncation: replace
g ibymin (g i) (N i)to bring anyginto the bounded set.(ℕ → ℕ) → (ℕ → ℕ) → ℕ → ℕ
DOIMTH.R-2026-6018
Cite
Verification
- Replay
- accepted
- Axioms
- Classical.choiceQuot.soundpropext
- Statement identity
- not-applicable
- Substrate
- Lean 4 kernel v4.31.0
- Dictionary pin
- design-lab@5802df4 · initial
- Frozen export
- ca3c5a9d0ba4
- Verified
- 2026-09-24T00:00:00Z