Borel-Analytic Separation: Counterexample Chain

The singleton class over an analytic non-Borel set A ⊆ ℝ witnesses that WellBehavedVCMeasTarget (NullMeasurableSet) is strictly weaker than KrappWirthWellBehaved (MeasurableSet/Borel).

Main results

• singletonClassOn_measurable: every hypothesis in the singleton class is measurable
• singleton_badEvent_eq_preimage_planar: bad event = preimage of planar witness
• planarWitnessEvent_analytic: the planar witness is analytic
• planarWitnessEvent_not_measurable: the planar witness is NOT Borel
• singleton_badEvent_not_measurable: the sample-space bad event is NOT Borel

Definitions

noncomputable def zeroConcept : Concept ℝ Bool

The constantly false concept. The base hypothesis of the singleton class, serving both as the target concept and as the zeroConcept disjunct of singletonClassOn.

Equations

• zeroConcept x✝ = false

noncomputable def singletonConcept (a : ℝ) : Concept ℝ Bool

The point indicator singletonConcept a x = (x = a). Each singletonConcept a is itself Borel measurable; non-Borelness in the singleton-class witness comes from quantifying over a ∈ A for A analytic non-Borel, not from any individual concept.

Equations

• singletonConcept a x = if x = a then true else false

def singletonClassOn (A : Set ℝ) : ConceptClass ℝ Bool

The singleton class over A ⊆ ℝ: {zeroConcept} ∪ {singletonConcept a | a ∈ A}. The zeroConcept disjunct is the target concept against which the symmetrization bad event is measured. For A analytic non-Borel, this is the witness used to separate WellBehavedVCMeasTarget from the Krapp-Wirth Borel condition.

Equations

• singletonClassOn A = {h : Concept ℝ Bool | h = zeroConcept ∨ ∃ a ∈ A, h = singletonConcept a}

def planarWitnessEvent (A : Set ℝ) : Set (ℝ × ℝ)

The planar witness {(x, y) ∈ ℝ × ℝ | y ∈ A ∧ x ≠ y}. For A analytic 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.

Equations

• planarWitnessEvent A = {q : ℝ × ℝ | q.2 ∈ A ∧ q.1 ≠ q.2}

@[reducible, inline]

abbrev GhostPairs1 : Type

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.

Equations

• GhostPairs1 = ((Fin 1 → ℝ) × (Fin 1 → ℝ))

def samplePair1ToPlane : GhostPairs1 → ℝ × ℝ

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.

Equations

• samplePair1ToPlane p = (p.1 0, p.2 0)

def singletonBadEvent (A : Set ℝ) : Set GhostPairs1

The symmetrization bad event for the singleton class at sample size m = 1, target concept zeroConcept, and threshold 1/2. Equals the preimage of planarWitnessEvent under samplePair1ToPlane (see singleton_badEvent_eq_preimage_planar), and inherits both analyticity and non-Borelness from the planar set when A is analytic non-Borel.

Equations

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

Theorem G

theorem singletonClassOn_measurable (A : Set ℝ) (h : Concept ℝ Bool) : h ∈ singletonClassOn A → Measurable h

Every hypothesis in singletonClassOn A is Borel measurable: zeroConcept is constant, and each singletonConcept a factors through measurableSet_singleton. The class is regular at the level of individual hypotheses; non-measurability enters only through the existential over A.

Theorem H

theorem singleton_badEvent_eq_preimage_planar (A : Set ℝ) : singletonBadEvent A = samplePair1ToPlane ⁻¹' planarWitnessEvent A

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.

Theorem I

theorem planarWitnessEvent_analytic (A : Set ℝ) (hA : MeasureTheory.AnalyticSet A) : MeasureTheory.AnalyticSet (planarWitnessEvent A)

For A analytic, planarWitnessEvent A is analytic. The proof presents it as the intersection of Prod.snd ⁻¹' A (analytic, by preimage of analytic under a continuous map) with the Borel set {(x, y) | x ≠ y} (the complement of the diagonal). Analytic sets are closed under intersection with Borel sets.

Theorem J

theorem planarWitnessEvent_not_measurable (A : Set ℝ) (hA_non : ¬MeasurableSet A) : ¬MeasurableSet (planarWitnessEvent A)

For A non-Borel, planarWitnessEvent A is non-Borel. The proof picks some a ∉ A and shows the vertical section y ↦ (a, y) pulls the planar event back to A itself: if the planar event were Borel, its preimage under this measurable map would be Borel too, contradicting the hypothesis on A.

Theorem K

theorem singleton_badEvent_not_measurable (A : Set ℝ) (hA_non : ¬MeasurableSet A) : ¬MeasurableSet (singletonBadEvent A)

For A non-Borel, the singleton bad event is non-Borel. Combine singleton_badEvent_eq_preimage_planar with planarWitnessEvent_not_measurable: the preimage of a non-Borel set under a measurable surjection cannot itself be Borel.

Theorem L: Relative separation theorem

theorem analytic_nonborel_set_gives_measTarget_separation (A : Set ℝ) (hA_an : MeasureTheory.AnalyticSet A) (hA_non : ¬MeasurableSet A) : KrappWirthSeparationMeasTarget

Main separation theorem. Given any analytic non-Borel set A ⊆ ℝ, the concept class obtained by parameterising singletonConcept (plus zeroConcept) over A is a concrete witness that WellBehavedVCMeasTarget is strictly weaker than the Krapp-Wirth Borel condition. The class is constructed as Set.range e for an evaluation map e : Bool × β → Concept ℝ Bool built from a Polish parameterisation of A; post-construction, Set.range e equals singletonClassOn (Set.range g) where g realises A.

The class satisfies:

• MeasurableHypotheses: every individual hypothesis is Borel (singletonClassOn_measurable).
• WellBehavedVCMeasTarget: the bad event is analytic (planarWitnessEvent_analytic lifted via singleton_badEvent_eq_preimage_planar), hence NullMeasurableSet by 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.

theorem exists_measTarget_separation (hex : ∃ (A : Set ℝ), MeasureTheory.AnalyticSet A ∧ ¬MeasurableSet A) : KrappWirthSeparationMeasTarget

Existence form: provided an analytic non-Borel set in ℝ is available, the separation in analytic_nonborel_set_gives_measTarget_separation is realised. The unconditional form (with no hypothesis) requires supplying Souslin's classical analytic non-Borel set; this theorem packages the reduction.