Interpolation of Concept Classes — Measurability Descent

If C₁ and C₂ are concept classes with Borel parameterizations (StandardBorelSpace parameter spaces, jointly measurable evaluation maps), their interpolation — the class of piecewise concepts agreeing with h₁ ∈ C₁ on region A and h₂ ∈ C₂ on Aᶜ — satisfies WellBehavedVCMeasTarget (NullMeasurableSet bad events).

The interpolated class may NOT preserve KrappWirthWellBehaved (Borel-measurable ghost gap maps). Measurability can only descend, not stay at the Borel level.

Main results

• interpClassFixed_wellBehaved: fixed-region interpolation is well-behaved
• interpClassCountable_wellBehaved: countable-family interpolation is well-behaved
• interpClass_wellBehaved_of_routerCode: conditional interpolation (BorelRouterCode)
• not_KrappWirth_of_nonBorel_badEvent: descent — Borel level can fail

References

• Krapp & Wirth (2024, arXiv:2410.10243)
• BorelAnalyticBridge.lean (this kernel)

Definitions

noncomputable def piecewiseConcept {X : Type u} [MeasurableSpace X] (A : Set X) (h₁ h₂ : Concept X Bool) : Concept X Bool

Piecewise concept: agrees with h₁ on A, with h₂ on Aᶜ.

Equations

• piecewiseConcept A h₁ h₂ x = if x ∈ A then h₁ x else h₂ x

noncomputable def routerOfSet {X : Type u} [MeasurableSpace X] (A : Set X) : Unit → Concept X Bool

Router from a single fixed set: maps Unit × X → Bool.

Equations

• routerOfSet A x✝ x = if x ∈ A then true else false

noncomputable def routerOfSetFamily {X : Type u} [MeasurableSpace X] (A : ℕ → Set X) : ℕ → Concept X Bool

Router from a countable family of sets: maps ℕ × X → Bool.

Equations

• routerOfSetFamily A n x = if x ∈ A n then true else false

Concept Class Definitions

def interpClassFixed {X : Type u} [MeasurableSpace X] (C₁ C₂ : ConceptClass X Bool) (A : Set X) : ConceptClass X Bool

Interpolation with a fixed region A.

Equations

• interpClassFixed C₁ C₂ A = {h : Concept X Bool | ∃ h₁ ∈ C₁, ∃ h₂ ∈ C₂, h = piecewiseConcept A h₁ h₂}

def interpClassCountable {X : Type u} [MeasurableSpace X] (C₁ C₂ : ConceptClass X Bool) (A : ℕ → Set X) : ConceptClass X Bool

Interpolation with a countable family of regions.

Equations

• interpClassCountable C₁ C₂ A = {h : Concept X Bool | ∃ (n : ℕ), ∃ h₁ ∈ C₁, ∃ h₂ ∈ C₂, h = piecewiseConcept (A n) h₁ h₂}

def interpClass {X : Type u} [MeasurableSpace X] (C₁ C₂ : ConceptClass X Bool) : ConceptClass X Bool

Full interpolation: existential over arbitrary measurable regions.

Equations

• interpClass C₁ C₂ = {h : Concept X Bool | ∃ (A : Set X), MeasurableSet A ∧ ∃ h₁ ∈ C₁, ∃ h₂ ∈ C₂, h = piecewiseConcept A h₁ h₂}

Router Measurability

theorem routerOfSet_measurable {X : Type u} [MeasurableSpace X] {A : Set X} (hA : MeasurableSet A) : Measurable fun (p : Unit × X) => routerOfSet A p.1 p.2

The router for a fixed measurable set is jointly measurable.

theorem routerOfSetFamily_measurable {X : Type u} [MeasurableSpace X] {A : ℕ → Set X} (hA : ∀ (n : ℕ), MeasurableSet (A n)) : Measurable fun (p : ℕ × X) => routerOfSetFamily A p.1 p.2

The router for a countable measurable family is jointly measurable.

Set-Equality Bridges

theorem interpClassFixed_eq_range_patchEval {X : Type u} [MeasurableSpace X] {Θ₁ : Type u_1} {Θ₂ : Type u_2} [MeasurableSpace Θ₁] [MeasurableSpace Θ₂] (e₁ : Θ₁ → Concept X Bool) (e₂ : Θ₂ → Concept X Bool) (A : Set X) : interpClassFixed (Set.range e₁) (Set.range e₂) A = Set.range (patchEval e₁ e₂ (routerOfSet A))

interpClassFixed equals the range of patchEval with routerOfSet.

theorem interpClassCountable_eq_range_patchEval {X : Type u} [MeasurableSpace X] {Θ₁ : Type u_1} {Θ₂ : Type u_2} [MeasurableSpace Θ₁] [MeasurableSpace Θ₂] (e₁ : Θ₁ → Concept X Bool) (e₂ : Θ₂ → Concept X Bool) (A : ℕ → Set X) : interpClassCountable (Set.range e₁) (Set.range e₂) A = Set.range (patchEval e₁ e₂ (routerOfSetFamily A))

interpClassCountable equals the range of patchEval with routerOfSetFamily.

WellBehaved Theorems

theorem interpClassFixed_wellBehaved {X : Type u} [MeasurableSpace X] [TopologicalSpace X] [PolishSpace X] [BorelSpace X] {Θ₁ : Type u_1} {Θ₂ : Type u_2} [MeasurableSpace Θ₁] [StandardBorelSpace Θ₁] [MeasurableSpace Θ₂] [StandardBorelSpace Θ₂] (e₁ : Θ₁ → Concept X Bool) (e₂ : Θ₂ → Concept X Bool) (he₁ : Measurable fun (p : Θ₁ × X) => e₁ p.1 p.2) (he₂ : Measurable fun (p : Θ₂ × X) => e₂ p.1 p.2) {A : Set X} (hA : MeasurableSet A) : WellBehavedVCMeasTarget X (interpClassFixed (Set.range e₁) (Set.range e₂) A)

Fixed-region interpolation of Borel-parameterized classes is well-behaved.

theorem interpClassCountable_wellBehaved {X : Type u} [MeasurableSpace X] [TopologicalSpace X] [PolishSpace X] [BorelSpace X] {Θ₁ : Type u_1} {Θ₂ : Type u_2} [MeasurableSpace Θ₁] [StandardBorelSpace Θ₁] [MeasurableSpace Θ₂] [StandardBorelSpace Θ₂] (e₁ : Θ₁ → Concept X Bool) (e₂ : Θ₂ → Concept X Bool) (he₁ : Measurable fun (p : Θ₁ × X) => e₁ p.1 p.2) (he₂ : Measurable fun (p : Θ₂ × X) => e₂ p.1 p.2) {A : ℕ → Set X} (hA : ∀ (n : ℕ), MeasurableSet (A n)) : WellBehavedVCMeasTarget X (interpClassCountable (Set.range e₁) (Set.range e₂) A)

Countable-family interpolation of Borel-parameterized classes is well-behaved.

Measurability Descent

theorem not_KrappWirth_of_nonBorel_badEvent {X : Type u} [MeasurableSpace X] (C : ConceptClass X Bool) (c : Concept X Bool) (m : ℕ) (ε : ℝ) (hC : Set.Nonempty C) (hbad : ¬MeasurableSet {p : (Fin m → X) × (Fin m → X) | ∃ h ∈ C, oneSidedGhostGap h c m p ≥ ε / 2}) : ¬KrappWirthWellBehaved X C

If the one-sided ghost gap bad event is NOT MeasurableSet, then KrappWirthWellBehaved fails. Measurability can only descend.

BorelRouterCode: Conditional Interpolation

structure BorelRouterCode (X : Type u) [MeasurableSpace X] : Type (u + 1)

A Borel router code: a StandardBorelSpace parameter space Ρ with a jointly measurable evaluation map eval : Ρ × X → Bool. This encodes the ability to select regions via a Borel-parameterized family.

• Ρ : Type u

  The router parameter space

• instMeasΡ : MeasurableSpace self.Ρ

  MeasurableSpace instance on Ρ

• instStdΡ : StandardBorelSpace self.Ρ

  StandardBorelSpace instance on Ρ

• eval : self.Ρ → Concept X Bool

  The router evaluation map

• eval_meas : Measurable fun (p : self.Ρ × X) => self.eval p.1 p.2

  Joint measurability of the evaluation map

theorem range_patchEval_sub_interpClass {X : Type u} [MeasurableSpace X] {Θ₁ : Type u_1} {Θ₂ : Type u_2} [MeasurableSpace Θ₁] [MeasurableSpace Θ₂] (e₁ : Θ₁ → Concept X Bool) (e₂ : Θ₂ → Concept X Bool) (R : BorelRouterCode X) : Set.range (patchEval e₁ e₂ R.eval) ⊆ interpClass (Set.range e₁) (Set.range e₂)

The range of patchEval with a BorelRouterCode is contained in interpClass.

theorem interpClass_wellBehaved_of_routerCode {X : Type u} [MeasurableSpace X] [TopologicalSpace X] [PolishSpace X] [BorelSpace X] {Θ₁ : Type u_1} {Θ₂ : Type u_2} [MeasurableSpace Θ₁] [StandardBorelSpace Θ₁] [MeasurableSpace Θ₂] [StandardBorelSpace Θ₂] (e₁ : Θ₁ → Concept X Bool) (e₂ : Θ₂ → Concept X Bool) (he₁ : Measurable fun (p : Θ₁ × X) => e₁ p.1 p.2) (he₂ : Measurable fun (p : Θ₂ × X) => e₂ p.1 p.2) (R : BorelRouterCode X) : WellBehavedVCMeasTarget X (Set.range (patchEval e₁ e₂ R.eval))

Conditional interpolation via BorelRouterCode is well-behaved: the range of patchEval with a Borel router satisfies WellBehavedVCMeasTarget.

Open Question Definition

def HasFullInterpolationRouterCode (X : Type u) [MeasurableSpace X] : Prop

Whether there exists a BorelRouterCode for X — i.e., whether every measurable region can be encoded by a Borel-parameterized router.

Equations

• HasFullInterpolationRouterCode X = Nonempty (BorelRouterCode X)