Amalgamation Preserves WellBehavedVCMeasTarget

Given two Borel-parameterized concept families e₁ : Θ₁ → Concept X Bool and e₂ : Θ₂ → Concept X Bool, with projection maps π₁ : Θ₁ → S and π₂ : Θ₂ → S into a common StandardBorelSpace S, the amalgamation class - the set of concepts merge(θ₁, θ₂) for (θ₁, θ₂) satisfying π₁ θ₁ = π₂ θ₂ - satisfies WellBehavedVCMeasTarget.

The proof proceeds by:

1. Showing the agreement relation {(θ₁, θ₂) | π₁ θ₁ = π₂ θ₂} is MeasurableSet (via measurableSet_eq_fun + upgradeStandardBorel)
2. Taking the StandardBorelSpace subtype (via MeasurableSet.standardBorel)
3. Reducing to borel_param_wellBehavedVCMeasTarget on the subtype

Main results

• measurableSet_agreementRel: the agreement fiber product is MeasurableSet
• amalgClass_wellBehaved: amalgamation preserves WellBehavedVCMeasTarget
• interpClassFixed_subset_amalgClass: fixed-region interpolation embeds in amalgamation

References

• BorelAnalyticBridge.lean (bridge theorem)
• Interpolation.lean (piecewise concepts, interpClassFixed)

Definitions

def agreementRel {Θ₁ : Type u_1} {Θ₂ : Type u_2} {S : Type u_3} (π₁ : Θ₁ → S) (π₂ : Θ₂ → S) : Set (Θ₁ × Θ₂)

The agreement relation: pairs (θ₁, θ₂) where π₁ θ₁ = π₂ θ₂.

Equations

• agreementRel π₁ π₂ = {p : Θ₁ × Θ₂ | π₁ p.1 = π₂ p.2}

def relParamClass {X : Type u} [MeasurableSpace X] {Θ : Type u_1} (R : Set Θ) (e : Θ → Concept X Bool) : ConceptClass X Bool

Parameterized sub-class: concepts e(θ) for θ restricted to a subset R.

Equations

• relParamClass R e = {h : Concept X Bool | ∃ θ ∈ R, h = e θ}

def amalgClass {X : Type u} [MeasurableSpace X] {Θ₁ : Type u_1} {Θ₂ : Type u_2} {S : Type u_3} (π₁ : Θ₁ → S) (π₂ : Θ₂ → S) (merge : Θ₁ × Θ₂ → Concept X Bool) : ConceptClass X Bool

The amalgamation class: merge(θ₁, θ₂) for (θ₁, θ₂) in the agreement fiber.

Equations

• amalgClass π₁ π₂ merge = relParamClass (agreementRel π₁ π₂) merge

Agreement relation is MeasurableSet

theorem measurableSet_agreementRel {Θ₁ : Type u_1} {Θ₂ : Type u_2} {S : Type u_3} [MeasurableSpace Θ₁] [MeasurableSpace Θ₂] [MeasurableSpace S] [StandardBorelSpace S] (π₁ : Θ₁ → S) (π₂ : Θ₂ → S) (hπ₁ : Measurable π₁) (hπ₂ : Measurable π₂) : MeasurableSet (agreementRel π₁ π₂)

The agreement relation is MeasurableSet when projections are measurable and the codomain is StandardBorelSpace.

Amalgamation preserves WellBehavedVCMeasTarget

theorem amalgClass_wellBehaved {X : Type u} [MeasurableSpace X] [TopologicalSpace X] [PolishSpace X] [BorelSpace X] {Θ₁ : Type u_1} {Θ₂ : Type u_2} {S : Type u_3} [MeasurableSpace Θ₁] [StandardBorelSpace Θ₁] [MeasurableSpace Θ₂] [StandardBorelSpace Θ₂] [MeasurableSpace S] [StandardBorelSpace S] (π₁ : Θ₁ → S) (π₂ : Θ₂ → S) (hπ₁ : Measurable π₁) (hπ₂ : Measurable π₂) (merge : Θ₁ × Θ₂ → Concept X Bool) (hmerge : Measurable fun (p : (Θ₁ × Θ₂) × X) => merge p.1 p.2) : WellBehavedVCMeasTarget X (amalgClass π₁ π₂ merge)

The amalgamation class satisfies WellBehavedVCMeasTarget when all parameter spaces are StandardBorelSpace and merge is jointly measurable.

Fixed-region interpolation embeds in amalgamation

theorem interpClassFixed_subset_amalgClass {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 ⊆ amalgClass (fun (x : Θ₁) => ()) (fun (x : Θ₂) => ()) fun (p : Θ₁ × Θ₂) => piecewiseConcept A (e₁ p.1) (e₂ p.2)

Fixed-region interpolation is a subset of amalgamation with trivial projections.