The Krapp–Wirth measurable-target separation holds unconditionally: the analytic non-Borel witness discharges the hypothesis of analytic_nonborel_set_gives_measTarget_separation.
KrappWirthSeparationMeasTarget
- DeclkrappWirthSeparationMeasTarget_holdsDeclaration kindtheorem
KrappWirthSeparationMeasTarget
- Declanalytic_nonborel_set_gives_measTarget_separationDeclaration kindtheorem
Main separation theorem. Given any analytic non-Borel set
A ⊆ ℝ, the concept class obtained by parameterisingsingletonConcept(pluszeroConcept) overAis a concrete witness thatWellBehavedVCMeasTargetis strictly weaker than the Krapp-Wirth Borel condition. The class is constructed asSet.range efor an evaluation mape : Bool × β → Concept ℝ Boolbuilt from a Polish parameterisation ofA; post-construction,Set.range eequalssingletonClassOn (Set.range g)wheregrealisesA.The class satisfies:
MeasurableHypotheses: every individual hypothesis is Borel (singletonClassOn_measurable).WellBehavedVCMeasTarget: the bad event is analytic (planarWitnessEvent_analyticlifted viasingleton_badEvent_eq_preimage_planar), henceNullMeasurableSetby the Choquet bridge.- NOT
KrappWirthWellBehaved: the bad event is not Borel (singleton_badEvent_not_measurable).
The separation is realised by passing through the standard Borel space ℝ as the parameter space; the construction reuses no problem-specific fact beyond the existence of an analytic non-Borel subset of ℝ (Souslin's classical result), supplied in
exists_measTarget_separation. The witness shows that the measurable-target variant proved in this kernel is a genuine improvement over the existing literature, not a restatement.∀ (A : Set ℝ), MeasureTheory.AnalyticSet A → ¬MeasurableSet A → KrappWirthSeparationMeasTarget
ConceptClassEmpiricalErrorFLT.ConceptGhostPairs1KrappWirthSeparationMeasTargetKrappWirthWellBehavedMeasurableHypothesesWellBehavedVCMeasTargetghostGapGridghostGapSupsingletonBadEventsingletonClassOnsingletonConceptzeroConceptzeroOneLossUses
- Declsingleton_badEvent_not_measurableDeclaration kindtheorem
For
Anon-Borel, the singleton bad event is non-Borel. Combinesingleton_badEvent_eq_preimage_planarwithplanarWitnessEvent_not_measurable: the preimage of a non-Borel set under a measurable surjection cannot itself be Borel.∀ (A : Set ℝ), ¬MeasurableSet A → ¬MeasurableSet (singletonBadEvent A)
- Declsingleton_badEvent_eq_preimage_planarDeclaration kindtheorem
The singleton bad event equals
samplePair1ToPlane ⁻¹' planarWitnessEvent. The set equality that transports both analyticity and non-Borelness from the planar witness to the learning-theoretic bad event.∀ (A : Set ℝ), singletonBadEvent A = samplePair1ToPlane ⁻¹' planarWitnessEvent A
- DeclplanarWitnessEvent_not_measurableDeclaration kindtheorem
For
Anon-Borel,planarWitnessEvent Ais non-Borel. The proof picks somea ∉ Aand shows the vertical sectiony ↦ (a, y)pulls the planar event back toAitself: if the planar event were Borel, its preimage under this measurable map would be Borel too, contradicting the hypothesis onA.∀ (A : Set ℝ), ¬MeasurableSet A → ¬MeasurableSet (planarWitnessEvent A)
- DecloneSidedGhostGap_mem_gridDeclaration kindtheorem
∀ {X : Type u} [inst : MeasurableSpace X] (h c : Concept X Bool) (m : ℕ) (p : (Fin m → X) × (Fin m → X)), oneSidedGhostGap h c m p ∈ ghostGapGrid m - DeclempiricalError_mem_empErrGridDeclaration kindtheorem
∀ {X : Type u} [MeasurableSpace X] (h : Concept X Bool) {m : ℕ} (S : Fin m → X × Bool), EmpiricalError X Bool h S (zeroOneLoss Bool) ∈ empErrGrid mUsed by
- Declborel_param_wellBehavedVCMeasTargetDeclaration kindtheorem
Class-level corollary: every Borel-parameterized concept class with a measurable evaluation map satisfies
WellBehavedVCMeasTarget. Composesborel_param_nullMeasurableSet_bad_eventover all measurable targetsc. The measurable-target variant ofWellBehavedVCis what the kernel actually proves; the unrestricted variant remains open and is the subject of the Borel-analytic separation witness inTheorem/BorelAnalyticSeparation.lean.∀ {X : Type u} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [PolishSpace X] [BorelSpace X] {Θ : Type u_1} [inst_4 : MeasurableSpace Θ] [StandardBorelSpace Θ] (e : Θ → Concept X Bool), (Measurable fun p => e p.1 p.2) → WellBehavedVCMeasTarget X (Set.range e) - Declborel_param_nullMeasurableSet_bad_eventDeclaration kindtheorem
Positive bridge. If a concept class is parameterized by a Borel measurable map
Θ → Concept Xfrom a standard Borel spaceΘ, then the symmetrization bad event is analytic, henceNullMeasurableSet. The bad event is a Suslin projection of a Borel witness set (the projection alongΘof{(θ, p) | gap(eval θ, p) ≥ ε / 2}), and projections of Borel sets are analytic by definition. This is the entry point through which Borel parameterization implies the regularity required by the fundamental theorem.∀ {X : Type u} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [PolishSpace X] [BorelSpace X] {Θ : Type u_1} [inst_4 : MeasurableSpace Θ] [StandardBorelSpace Θ] (e : Θ → Concept X Bool), (Measurable fun p => e p.1 p.2) → ∀ (c : Concept X Bool), Measurable c → ∀ (m : ℕ) (ε : ℝ) (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D], MeasureTheory.NullMeasurableSet (paramBadEvent e c m ε) (GhostPairMeasure D m) - Declborel_param_badEvent_analyticDeclaration kindtheorem
The bad event (projection of witness set) is analytic. Projection of a Borel set from a StandardBorelSpace is analytic (Suslin). This is the key step: existential quantification over parameters produces an analytic (Σ₁¹) set, which may not be Borel.
∀ {X : Type u} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [BorelSpace X] [PolishSpace X] {Θ : Type u_1} [inst_4 : MeasurableSpace Θ] [StandardBorelSpace Θ] (e : Θ → Concept X Bool), (Measurable fun p => e p.1 p.2) → ∀ (c : Concept X Bool), Measurable c → ∀ (m : ℕ) (ε : ℝ), MeasureTheory.AnalyticSet (paramBadEvent e c m ε) - DeclparamWitnessSet_measurableDeclaration kindtheorem
The witness set {(θ, p) | ghost-gap ≥ ε/2} is MeasurableSet when the evaluation map e and target c are measurable. This is the Borel half of the Borel-analytic bridge.
∀ {X : Type u} [inst : MeasurableSpace X] {Θ : Type u_1} [inst_1 : MeasurableSpace Θ] (e : Θ → Concept X Bool), (Measurable fun p => e p.1 p.2) → ∀ (c : Concept X Bool), Measurable c → ∀ (m : ℕ) (ε : ℝ), MeasurableSet (paramWitnessSet e c m ε) - DeclanalyticSet_nullMeasurableSet_ghostPairsDeclaration kindtheorem
Analytic subsets of the ghost sample space
(Fin m → X) × (Fin m → X)areNullMeasurableSetunder the product probability measure. A specialisation ofanalyticSet_nullMeasurableSetfromPureMath/AnalyticMeasurability.leanto the type the symmetrization argument actually consumes.∀ {X : Type u} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [BorelSpace X] [PolishSpace X] {m : ℕ} {s : Set ((Fin m → X) × (Fin m → X))}, MeasureTheory.AnalyticSet s → ∀ (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D], MeasureTheory.NullMeasurableSet s (GhostPairMeasure D m) - DeclanalyticSet_nullMeasurableSetDeclaration kindtheorem
Analytic sets are null-measurable for finite Borel measures on Polish spaces. FLT-facing alias of the ZPM-canonical
MeasureTheory.AnalyticSet.nullMeasurableSet.∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] [PolishSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {s : Set α}, MeasureTheory.AnalyticSet s → MeasureTheory.NullMeasurableSet s μ - DeclMeasureTheory.AnalyticSet.nullMeasurableSetDeclaration kindtheorem
Analytic sets are null-measurable. For any finite Borel measure on a Polish space, every analytic set is
NullMeasurableSet. Proof inner- approximates the analytic set by compacts, takes the union of approximators (a Borel set), and shows the difference is contained in a Borel null set.This is the abstract bridge that the entire Borel-analytic measurability layer of downstream learning-theory kernels rests on.
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] [PolishSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {s : Set α}, MeasureTheory.AnalyticSet s → MeasureTheory.NullMeasurableSet s μ - DeclMeasureTheory.AnalyticSet.exists_isCompact_measureReal_gtDeclaration kindtheorem
Inner regularity for analytic sets: any analytic subset of a Polish space can be approximated from inside by a compact subset in measure, by any slack
ε > 0. Specialisation of Choquet capacitability (Kechris 30.13) to the measure-as-capacity instance.∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] [PolishSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {s : Set α}, MeasureTheory.AnalyticSet s → ∀ ε > 0, ∃ K, IsCompact K ∧ K ⊆ s ∧ μ.real s < μ.real K + ε - DeclMeasureTheory.AnalyticSet.compactCap_eqDeclaration kindtheorem
For analytic sets, compact capacity equals measure.
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] [PolishSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {s : Set α}, MeasureTheory.AnalyticSet s → MeasureTheory.compactCap μ s = μ sUses
- DeclcompactCap_eq_iSup_isCompactDeclaration kindtheorem
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α), MeasureTheory.compactCap μ s = ⨆ K, ⨆ (_ : IsCompact K), ⨆ (_ : K ⊆ s), μ K - DeclMeasureTheory.measure_isChoquetCapacityDeclaration kindtheorem
Every finite Borel measure on a Polish space is a Choquet capacity.
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] [PolishSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ], MeasureTheory.IsChoquetCapacity fun s => μ s - DeclMeasureTheory.AnalyticSet.cap_eq_iSup_isCompactDeclaration kindtheorem
Choquet capacitability. For analytic sets, capacity equals the supremum over compact subsets (Kechris 30.13).
∀ {α : 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 KUses
- 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) - DeclKrappWirthWellBehaved.V_measurableDeclaration kindtheorem
∀ {X : Type u} {inst : MeasurableSpace X} {C : ConceptClass X Bool} [self : KrappWirthWellBehaved X C], KrappWirthV X C - DeclMeasureTheory.exists_analyticSet_not_measurableSet_realDeclaration kindtheorem
An analytic non-Borel subset of
ℝ: the image of the Baire-space witness under the continuous injection. Analyticity transfers along the continuous image; non-Borelness transfers back along the injective preimage.∃ A, MeasureTheory.AnalyticSet A ∧ ¬MeasurableSet A
Uses
- DeclMeasureTheory.exists_analyticSet_not_measurableSetDeclaration kindtheorem
An analytic non-Borel subset of Baire space: the projection of the diagonal witness.
∃ A, MeasureTheory.AnalyticSet A ∧ ¬MeasurableSet A
- DeclMeasureTheory.exists_closed_proj_not_measurableSetDeclaration kindtheorem
A closed set with a non-Borel projection. Diagonalize the universal closed set of
(ℕ → ℕ) × (ℕ → ℕ): were the projection Borel, its complement would be analytic, hence the projection of a closed set, hence a section of the universal set — and evaluating that section at its own parameter is contradictory.∃ D, IsClosed D ∧ ¬MeasurableSet {x | ∃ y, (x, y) ∈ D} - DeclMeasureTheory.exists_closed_universal_sectionsDeclaration kindtheorem
A universal closed set. Every second-countable space
Xcarries a closed subset ofX × (ℕ → ℕ)whose sections run through all closed subsets ofX: enumerate a countable basis together with∅, and let the parameter select which basis elements to exclude.∀ (X : Type u_1) [inst : TopologicalSpace X] [SecondCountableTopology X], ∃ S, IsClosed S ∧ ∀ (C : Set X), IsClosed C → ∃ y, {x | (x, y) ∈ S} = C - DeclMeasureTheory.embedBaireReal_injectiveDeclaration kindtheorem
Function.Injective MeasureTheory.embedBaireReal
- DeclMeasureTheory.baireMarkerBits_injectiveDeclaration kindtheorem
Function.Injective MeasureTheory.baireMarkerBits
- DeclMeasureTheory.baireMarkers_strictMonoDeclaration kindtheorem
∀ (x : ℕ → ℕ), StrictMono (MeasureTheory.baireMarkers x)
- DeclMeasureTheory.continuous_embedBaireRealDeclaration kindtheorem
Continuous MeasureTheory.embedBaireReal
- DeclMeasureTheory.continuous_cantorFunction_oneThirdDeclaration kindtheorem
Continuous (Cardinal.cantorFunction (1 / 3))
- DeclMeasureTheory.continuous_baireMarkerBitsDeclaration kindtheorem
Continuous MeasureTheory.baireMarkerBits
- DefinitionBnddef
Bounded functions set:
{g : ℕ → ℕ | ∀ i, g i ≤ N i}.(ℕ → ℕ) → Set (ℕ → ℕ)
- DefinitionConceptClassdef
A concept class is a set of concepts. Used by every paradigm, complexity measure, and criterion.
Primary definition: Set of functions. Used for PAC/agnostic PAC where concept classes are sets over which VC dimension, Rademacher complexity, covering numbers, etc. are measured. Alternative definitions below for contexts requiring decidability, enumerability, or measurability.
Type u → Type v → Type (max v u)
- DefinitionCyldef
Cylinder set:
{g : ℕ → ℕ | ∀ i ≤ n, g i ≤ N i}.(ℕ → ℕ) → ℕ → Set (ℕ → ℕ)
- DefinitionEmpiricalErrordef
Empirical error: average loss on a finite sample.
(X : Type u) → (Y : Type v) → Concept X Y → {m : ℕ} → (Fin m → X × Y) → LossFunction Y → ℝ - DefinitionFLT.Conceptdef
A concept is a function from domain to label. This is the atomic unit that concept classes collect and learners try to approximate.
Type u → Type v → Type (max u v)
- DefinitionGhostPairMeasuredef
{X : Type u} → [inst : MeasurableSpace X] → MeasureTheory.Measure X → (m : ℕ) → MeasureTheory.Measure ((Fin m → X) × (Fin m → X)) - DefinitionGhostPairsdef
Ghost sample pairs: two independent samples of size m.
Type u → ℕ → Type u
- DefinitionGhostPairs1def
The ghost sample space at sample size
m = 1:(Fin 1 → ℝ) × (Fin 1 → ℝ). The smallest sample size at which the singleton-class obstruction is already visible.Type
- DefinitionKrappWirthSeparationMeasTargetdef
OPEN QUESTION (measurable-target version): Does WellBehavedVCMeasTarget separate from KrappWirthWellBehaved? The Borel-analytic bridge (BorelAnalyticBridge.lean) closes this.
Prop
- DefinitionKrappWirthVdef
V-measurability (one-sided): the ghost gap sup map is measurable.
(X : Type u) → [MeasurableSpace X] → ConceptClass X Bool → Prop
- DefinitionKrappWirthWellBehavedstructure
Krapp-Wirth well-behavedness: measurable hypotheses + V + U. Extends MeasurableHypotheses (L1). Strictly stronger than MeasurableConceptClass (our condition).
(X : Type u) → [MeasurableSpace X] → ConceptClass X Bool → Prop
- DefinitionMeasurableHypothesesstructure
Every concept in C is a measurable function. Krapp-Wirth precondition: Γ(h) ∈ Σ_Z for all h ∈ H.
(X : Type u) → [MeasurableSpace X] → ConceptClass X Bool → Prop
- 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 - DefinitionMeasureTheory.baireMarkerBitsdef
The marker bits: the indicator stream of the marker set.
(ℕ → ℕ) → ℕ → Bool
- DefinitionMeasureTheory.baireMarkersdef
The marker sequence of
x : ℕ → ℕ: the strictly increasing sequencen + 1 + ∑_{k ≤ n} x k, whose successive gaps encodex.(ℕ → ℕ) → ℕ → ℕ
- DefinitionMeasureTheory.compactCapdef
Compact capacity of a set
srelative to a measureμ: the supremum ofμ Kover compact subsetsK ⊆ s. The inner-regularity functional whose equality withμ scharacterises measurability for analytic sets.{α : Type u_1} → [TopologicalSpace α] → [inst : MeasurableSpace α] → MeasureTheory.Measure α → Set α → ENNReal - DefinitionMeasureTheory.embedBaireRealdef
The embedding of Baire space into
ℝ: marker bits into the base-3 expansion.(ℕ → ℕ) → ℝ
- DefinitionWellBehavedVCMeasTargetdef
WellBehavedVC restricted to measurable targets. This is the correct target for the Borel-analytic positive bridge: Borel parameterization ⇒ analytic bad event ⇒ NullMeasurableSet, but only when c is measurable (so the ghost-gap map is measurable).
(X : Type u) → [MeasurableSpace X] → ConceptClass X Bool → Prop
- DefinitionchoquetTruncatedef
Truncation: replace
g ibymin (g i) (N i)to bring anyginto the bounded set.(ℕ → ℕ) → (ℕ → ℕ) → ℕ → ℕ
- DefinitionempErrGriddef
ℕ → Finset ℝ
- DefinitionghostGapGriddef
ℕ → Finset ℝ
- DefinitionghostGapSupdef
{X : Type u} → [MeasurableSpace X] → ConceptClass X Bool → Concept X Bool → (m : ℕ) → (Fin m → X) × (Fin m → X) → ℝ - DefinitiononeSidedGhostGapdef
{X : Type u} → [MeasurableSpace X] → Concept X Bool → Concept X Bool → (m : ℕ) → (Fin m → X) × (Fin m → X) → ℝ - DefinitionparamBadEventdef
The bad event in sample space: projection of the witness set. Existential over the parameter: {p | ∃ θ, gap(θ, p) ≥ ε/2}. This is analytic when the witness set is Borel (Theorem B).
{X : Type u} → [MeasurableSpace X] → {Θ : Type u_1} → [MeasurableSpace Θ] → (Θ → Concept X Bool) → Concept X Bool → (m : ℕ) → ℝ → Set (GhostPairs X m) - DefinitionparamWitnessSetdef
The witness set in parameter × sample space: {(θ, p) | EmpErr(h_θ, ghost, c) - EmpErr(h_θ, train, c) ≥ ε/2}. This is Borel when e and c are measurable (Theorem A).
{X : Type u} → [MeasurableSpace X] → {Θ : Type u_1} → [MeasurableSpace Θ] → (Θ → Concept X Bool) → Concept X Bool → (m : ℕ) → ℝ → Set (Θ × GhostPairs X m) - DefinitionplanarWitnessEventdef
The planar witness
{(x, y) ∈ ℝ × ℝ | y ∈ A ∧ x ≠ y}. ForAanalytic non-Borel, this set is itself analytic non-Borel. The geometric core of the separation: the learning-theoretic bad event below is a measurable preimage of this planar set.Set ℝ → Set (ℝ × ℝ)
- DefinitionsamplePair1ToPlanedef
The projection
GhostPairs1 → ℝ × ℝ,p ↦ (p.1 0, p.2 0). Surjective and measurable; non-Borelness of a target set transfers to non-Borelness of its preimage under a measurable surjection.GhostPairs1 → ℝ × ℝ
- DefinitionsingletonBadEventdef
The symmetrization bad event for the singleton class at sample size
m = 1, target conceptzeroConcept, and threshold1/2. Equals the preimage ofplanarWitnessEventundersamplePair1ToPlane(seesingleton_badEvent_eq_preimage_planar), and inherits both analyticity and non-Borelness from the planar set whenAis analytic non-Borel.Set ℝ → Set GhostPairs1
- DefinitionsingletonClassOndef
The singleton class over
A ⊆ ℝ:{zeroConcept} ∪ {singletonConcept a | a ∈ A}. ThezeroConceptdisjunct is the target concept against which the symmetrization bad event is measured. ForAanalytic non-Borel, this is the witness used to separateWellBehavedVCMeasTargetfrom the Krapp-Wirth Borel condition.Set ℝ → ConceptClass ℝ Bool
- DefinitionsingletonConceptdef
The point indicator
singletonConcept a x = (x = a). EachsingletonConcept ais itself Borel measurable; non-Borelness in the singleton-class witness comes from quantifying overa ∈ AforAanalytic non-Borel, not from any individual concept.ℝ → Concept ℝ Bool
- DefinitionzeroConceptdef
The constantly false concept. The base hypothesis of the singleton class, serving both as the target concept and as the
zeroConceptdisjunct ofsingletonClassOn.Concept ℝ Bool
- DefinitionzeroOneLossdef
The 0-1 loss for classification.
(Y : Type v) → [DecidableEq Y] → LossFunction Y
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
- 142a3e7672c2
- Verified
- 2026-09-24T00:00:00Z