Coarse-graining support: Support.Book.Ch04.MuLocalityGate

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

The LocalSigmaR → IsRestrictionLocalRandomVariable gate (Packet P4b, P5 input)

This file exposes the σ-algebra bridge localSigmaR_le_restrictionSigmaR at the Chapter 4 observable interface: a carrier observable that is measurable for the local entry-test σ-algebra LocalSigmaR U is a genuine restriction-local random variable IsRestrictionLocalRandomVariable U hU.

This is the P5 gate for carrier Mu locality. The plan's route for the coarse observable Mu is:

1. re-aim the raw Mu/toHilbertMatrixL2 measurability machinery (measurable_toHilbertMatrixL2_of_dense_inner and the dense-probe inner products, which are set integrals ∫_U w · a(·)_{ij} — the entry-test generators, via entryTestR_eq_setIntegral_of_support) so that a ↦ Mu (cubeSet Q) P0 a.toFun is LocalSigmaR (cubeSet Q)-measurable;
2. apply IsRestrictionLocalRandomVariable.of_measurable_localSigmaR (below) to conclude IsRestrictionLocalRandomVariable (cubeSet Q) hQ (fun a => Mu (cubeSet Q) P0 a.toFun).

Step 2 is provided here, law-independently. Step 1 (the carrier re-aim of the raw subtype/slice L² machinery) is the remaining P5 work; the honest, genuinely measurable slice sets it needs are now available (HCPolySupport.measurableSet_localSigmaR_aeeSlice).

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

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

The LocalSigmaR → restriction-local gate. A carrier observable measurable for the local entry-test σ-algebra LocalSigmaR U is a restriction-local random variable on the measurable observation set U.