DilationResponse

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Response observables under dilation

This file exposes the arbitrary-cube response observable transport used by the Section 5.6 wrap-around branch. DilationLaw already contained the origin-cube specialization needed for scale-normalized laws; descendant averages need the same statement before specializing to origin descendants.

theorem HCPolySupport.Book.Ch04.restrictionResponseJObservableCubeSet_rescaleCoeffField_of_aelocallyUniformlyElliptic {d : ℕ} [NeZero d] {a : RegCoeffField d} (ha : AELocallyUniformlyEllipticField a) (k : ℕ) (Q : TriadicCube d) (p q : Vec d) : restrictionResponseJObservableCubeSet Q p q (rescaleReg k a) = restrictionResponseJObservableCubeSet (Ch02.dilateCube (↑k) Q) p q a

theorem HCPolySupport.Book.Ch04.restrictionResponse_dilateCoeffField_neg_nat {d : ℕ} [NeZero d] {a : RegCoeffField d} (ha : AELocallyUniformlyEllipticField a) (k : ℕ) (Q : TriadicCube d) (p q : Vec d) : restrictionResponseJObservableCubeSet Q p q (dilateReg (-↑k) a) = restrictionResponseJObservableCubeSet (Ch02.dilateCube (↑k) Q) p q a

Scalar response observables under the dilation defining restrictionScaleNormalizedLaw, for arbitrary triadic cubes.