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

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

Law-relative measurability promotion (carrier re-type, Packet P3)

This is the canonical Ch4 bridge:

IsRestrictionLocalRandomVariable U hU X → AEMeasurable X P → AEStronglyMeasurable X P.

On the honest-fields carrier the promotion is genuine: the restriction σ-algebra RestrictionSigmaR U hU is contained in the canonical carrier σ-algebra (restrictionSigmaR_le), so a restriction-local random variable is honestly measurable, hence null- and a.e.-strongly measurable. This is unconditional in the law: the former LocalObservableLawCarrier hypothesis was always derivable (a vestigial hypothesis, Packet P4 R3-family strengthening) and has been dropped from these bridges — they now hold for every carrier law.

Later chapters should not introduce section-local copies of this bridge.

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

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

A restriction-local random variable is null-measurable under any carrier law.

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

A local random variable with countably generated target sigma algebra is a.e. measurable under any carrier law.

theorem HCPolySupport.Book.Ch04.IsRestrictionLocalRandomVariable.aestronglyMeasurable {β : Type u_1} [TopologicalSpace β] [MeasurableSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [OpensMeasurableSpace β] [SecondCountableTopology β] [MeasurableSpace.CountablyGenerated β] {d : ℕ} {P : RestrictionCoeffLaw d} {U : Set (Vec d)} {hU : MeasurableSet U} {X : RegCoeffField d → β} (hX : IsRestrictionLocalRandomVariable U hU X) : MeasureTheory.AEStronglyMeasurable X P

A local random variable into a second-countable pseudometrizable measurable space is a.e. strongly measurable under any carrier law.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.nullMeasurable_of_isLocalRandomVariable {β : Type u_1} [MeasurableSpace β] {d : ℕ} {P : RestrictionCoeffLaw d} (_hP : RestrictionLawCarrier P) {U : Set (Vec d)} {hU : MeasurableSet U} {X : RegCoeffField d → β} (hX : IsRestrictionLocalRandomVariable U hU X) : MeasureTheory.NullMeasurable X P

Dot-notation promotion from local-test measurability to null measurability.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_of_isLocalRandomVariable {β : Type u_1} [MeasurableSpace β] [MeasurableSpace.CountablyGenerated β] {d : ℕ} {P : RestrictionCoeffLaw d} (_hP : RestrictionLawCarrier P) {U : Set (Vec d)} {hU : MeasurableSet U} {X : RegCoeffField d → β} (hX : IsRestrictionLocalRandomVariable U hU X) : AEMeasurable X P

Dot-notation promotion from local-test measurability to a.e. measurability.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aestronglyMeasurable_of_isLocalRandomVariable {β : Type u_1} [TopologicalSpace β] [MeasurableSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [OpensMeasurableSpace β] [SecondCountableTopology β] [MeasurableSpace.CountablyGenerated β] {d : ℕ} {P : RestrictionCoeffLaw d} (_hP : RestrictionLawCarrier P) {U : Set (Vec d)} {hU : MeasurableSet U} {X : RegCoeffField d → β} (hX : IsRestrictionLocalRandomVariable U hU X) : MeasureTheory.AEStronglyMeasurable X P

Dot-notation promotion from local-test measurability to a.e. strong measurability.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.nullMeasurable_observable {β : Type u_1} [MeasurableSpace β] {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) {U : Set (Vec d)} (X : RestrictionObservable d U β) : MeasureTheory.NullMeasurable X.toFun P

Bundled-observable promotion to null measurability.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_observable {β : Type u_1} [MeasurableSpace β] [MeasurableSpace.CountablyGenerated β] {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) {U : Set (Vec d)} (X : RestrictionObservable d U β) : AEMeasurable X.toFun P

Bundled-observable promotion to a.e. measurability.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aestronglyMeasurable_observable {β : Type u_1} [TopologicalSpace β] [MeasurableSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [OpensMeasurableSpace β] [SecondCountableTopology β] [MeasurableSpace.CountablyGenerated β] {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) {U : Set (Vec d)} (X : RestrictionObservable d U β) : MeasureTheory.AEStronglyMeasurable X.toFun P

Bundled-observable promotion to a.e. strong measurability.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.measurableSet_aeeQuantitativeEllipticSlice_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (_hP : RestrictionLawCarrier P) (Q : TriadicCube d) (k : ℕ) : MeasurableSet {a : RegCoeffField d | AEEQuantitativeEllipticSlice (cubeSet Q) k a.toFun}

Canonical access to AEE quantitative slice local measurability, now the law-independent honest form (Packet P4b): genuine LocalSigmaR (cubeSet Q) measurability. The RestrictionLawCarrier argument is retained only for the dot-notation call site; the content no longer depends on the law.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.ae_exists_aeeQuantitativeEllipticSlice_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) : ∀ᵐ (a : RegCoeffField d) ∂P, ∃ (k : ℕ), AEEQuantitativeEllipticSlice (cubeSet Q) k a.toFun

A Chapter 4 law carrier gives the a.s. countable AEE quantitative-slice cover on each deterministic triadic cube.