Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch04.Theorems.Mu

Coarse-graining support: Support.Book.Ch04.Theorems.Mu #

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

Mu measurability (carrier re-aim, Packet P5 centrepiece) #

This file is the public Ch4 handoff for the coarse-grained energy Mu on the honest carrier. Following the carrier redesign, a law P : RestrictionCoeffLaw d is a measure on RegCoeffField d, and the observable is a ↦ Mu (cubeSet Q) P0 a.toFun.

The measurability is genuinely established, not merely null-covered. The carrier Mu-slice engine measurable_Mu_comp_aeeSlice_of_measurable_entryTest (Internal/AEESliceAssembly/CarrierMuFamily.lean) makes Mu ∘ toFun genuinely LocalSigmaR (cubeSet Q)-measurable on each AEE quantitative slice, using only the honest entry-test generators of the carrier (no fine pointwise data). The AEE slice events are genuinely LocalSigmaR-measurable (P4b), so the countable slice cover assembles by a genuine liftCover — no null bookkeeping — into a LocalSigmaR-measurable representative Y, which the gate IsRestrictionLocalRandomVariable.of_measurable_localSigmaR promotes to a genuine restriction-local random variable.

Note (statement check, Packet P5): Mu ∘ toFun is not LocalSigmaR-measurable on all of the carrier — off the a.e.-elliptic locus the carrier admits fields on which Mu is uninformative — so exists_isRestrictionLocalRandomVariable_ae_eq_Mu_cubeSet is not trivialised: the a.e.-representative Y (equal to Mu ∘ toFun on the a.s.-full elliptic locus) is genuinely needed. The honest endpoint therefore remains law-relative AEMeasurable, with the genuine local representative Y.

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

source
theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.exists_isRestrictionLocalRandomVariable_ae_eq_Mu_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (P0 : BlockVec d) :
∃ (Y : RegCoeffField d → ℝ), IsRestrictionLocalRandomVariable (cubeSet Q) ⋯ Y ∧ (fun (a : RegCoeffField d) => Mu (cubeSet Q) P0 a.toFun) =ᵐ[P] Y

Law-relative local representative of Mu on a fixed triadic cube. The carrier Mu-slice engine makes Mu ∘ toFun genuinely LocalSigmaR (cubeSet Q)- measurable on each AEE quantitative slice; the slices are genuinely LocalSigmaR-measurable and cover the law a.s., so a genuine liftCover produces a LocalSigmaR-measurable Y agreeing with Mu ∘ toFun almost surely, promoted to a restriction-local random variable by the gate.

source
theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.aemeasurable_Mu_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) (Q : TriadicCube d) (P0 : BlockVec d) :
AEMeasurable (fun (a : RegCoeffField d) => Mu (cubeSet Q) P0 a.toFun) P

The canonical Chapter 4 law-facing measurability theorem for Mu on a deterministic triadic cube. Downstream chapters should use this theorem directly; coarseBlockMatrix, ResponseJ, and BlockJ measurability should be derived from this finite-polarization root.