Coarse-graining support: Support.Probability.RegCoeffField.RestrictionBridge

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

The local-to-restriction σ-algebra bridge

This file supplies the σ-algebra comparison

LocalSigmaR U ≤ RestrictionSigmaR U hU

(localSigmaR_le_restrictionSigmaR), the P5 gate of the carrier redesign. It is the missing link between the two local carrier σ-algebras:

• LocalSigmaR U — generated by entry-test preimages against probes supported in U — is where the honest AEE-slice measurability lives (SliceMeasurability.lean);
• RestrictionSigmaR U hU — the comap along the restriction endomorphism restrictReg U hU — is the measurable local σ-algebra defining IsRestrictionLocalRandomVariable.

The comparison holds because a localized entry-test generator factors through the restriction endomorphism: for a probe supported in U, the restriction leaves the entry test unchanged (entryTestR_eq_restrictReg_of_support), so the generator is RestrictionSigmaR-measurable. Consequently every LocalSigmaR U-measurable observable is a genuine restriction-local random variable — in particular the AEE slice event, and (once its raw measurability machinery is re-aimed onto the carrier) the coarse-grained energy Mu.

The final section connects the entry-test generators to the set-integral form ∫_U w · a(·)_{ij} in which the raw Mu/toHilbertMatrixL2 measurability machinery expresses its dense-probe inner products (entryTestR_eq_setIntegral_of_support), so that those inner products are LocalSigmaR U-measurable — hence restriction-local — functions of the carrier field.

Reference: the paper (Armstrong–Kuusi–Loher, to appear).

Restriction leaves supported entry tests unchanged

theorem HCPolySupport.entryTestR_eq_restrictReg_of_support {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (i j : Fin d) {φ : Vec d → ℝ} (hsupp : Function.support φ ⊆ U) (a : RegCoeffField d) : entryTestR i j φ a = entryTestR i j φ (restrictReg U hU a)

For a probe supported in U, the restriction endomorphism leaves the entry test unchanged: the entry integrand a(·)_{ij} · φ only sees the values of a on U, where restrictReg U hU a agrees with a.

theorem HCPolySupport.measurable_entryTestR_restrictionSigmaR {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (i j : Fin d) {φ : Vec d → ℝ} (hφ : IsProbeR φ) (hsupp : Function.support φ ⊆ U) : Measurable (entryTestR i j φ)

A localized entry-test generator is RestrictionSigmaR U hU-measurable: it factors through the (restriction-local-measurable) restriction endomorphism.

The bridge

theorem HCPolySupport.localSigmaR_le_restrictionSigmaR {d : ℕ} (U : Set (Vec d)) (hU : MeasurableSet U) : LocalSigmaR U ≤ RestrictionSigmaR U hU

The local entry-test σ-algebra is coarser than the restriction σ-algebra. Each LocalSigmaR U generator is a supported entry-test preimage, hence RestrictionSigmaR U hU-measurable. This is the P5 gate: every LocalSigmaR U-measurable observable is a restriction-local random variable.

theorem HCPolySupport.measurable_restrictionSigmaR_of_measurable_localSigmaR {d : ℕ} {β : Type u_1} [MeasurableSpace β] {U : Set (Vec d)} (hU : MeasurableSet U) {X : RegCoeffField d → β} (hX : Measurable X) : Measurable X

A carrier observable that is LocalSigmaR U-measurable is RestrictionSigmaR U hU-measurable. (For β = ℝ this is exactly the IsRestrictionLocalRandomVariable predicate of Chapter 4.)

Entry tests as set integrals (the Mu/toHilbertMatrixL2 orientation)

theorem HCPolySupport.entryTestR_eq_setIntegral_of_support {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (i j : Fin d) {φ : Vec d → ℝ} (hsupp : Function.support φ ⊆ U) (a : RegCoeffField d) : entryTestR i j φ a = ∫ (x : Vec d) in U, φ x * a.toFun x i j

For a probe supported in U, the entry test equals the set integral ∫_U φ · a(·)_{ij} — the exact orientation in which the raw Mu/toHilbertMatrixL2 measurability machinery expresses its dense-probe inner products (inner_toScalarL2_hilbertMatrixL2Entry_eq_setIntegral). Hence each such inner product is a LocalSigmaR U-measurable — and so restriction-local — function of the carrier field.

theorem HCPolySupport.measurable_setIntegral_restrictionSigmaR {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (i j : Fin d) {φ : Vec d → ℝ} (hφ : IsProbeR φ) (hsupp : Function.support φ ⊆ U) : Measurable fun (a : RegCoeffField d) => ∫ (x : Vec d) in U, φ x * a.toFun x i j

The supported set-integral functional a ↦ ∫_U φ · a(·)_{ij} is RestrictionSigmaR U hU-measurable.