RealStationaryTransfer

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Real-translation stationary transfer of coarse block expectations

CoarseGraining's stationary-expectation layer (Homogenization.Book.Ch04.Theorems.StationaryExpectations) transfers coarse block expectations from a triadic cube to the origin cube at the same scale by writing the cube as a translate of the origin cube. Its transfer step is Ch04.integral_comp_toFun_translation_transfer, which consumes RestrictionStationaryLaw = IsStationaryR: invariance under integer translations only. The translation vector Q.index * 3 ^ Q.scale is an integer vector exactly when 0 ≤ Q.scale, which is why every CoarseGraining consequence of that route carries a nonnegative-scale hypothesis.

The genuine coefficient-cutoff law is invariant under every real translation (Algsuperdiff.Section3.Cutoff.coefficientCutoffLaw_stationary_real), so the scale restriction is an artifact of the interface, not of the mathematics. This module reroutes the transfer step through real translations: the scale-free geometric identity Homogenization.cubeSet_eq_translateSet_originCube_of_triadicCube writes an arbitrary triadic cube as the triadicCubeShift translate of the origin cube at the same scale, and Homogenization.coarseBlockMatrix_translateSet_eq_translateCoeffField is already stated for a real translation vector. The resulting expectation identities hold at every integer scale, positive or negative.

Main results

• integral_comp_toFun_translation_transfer_real
• integral_blockMatEntry_coarseBlockMatrix_cubeSet_eq_originCube_of_stationary_real
• integral_blockMatEntry_coarseBlockMatrix_cubeSet_eq_originCube_of_mem_descendantsAtScale

def Algsuperdiff.Section3.Provider.Annealed.IsStationaryRealR {d : ℕ} (P : HCPolySupport.RegCoeffLaw d) : Prop

Real-translation invariance of a carrier law, the hypothesis actually available for the coefficient-cutoff law. CoarseGraining's IsStationaryR is its restriction to integer translation vectors.

Equations

• Algsuperdiff.Section3.Provider.Annealed.IsStationaryRealR P = ∀ (z : HCPolySupport.Vec d), MeasureTheory.Measure.map (HCPolySupport.translateReg z) P = P

theorem Algsuperdiff.Section3.Provider.Annealed.translateReg_toFun_real {d : ℕ} (z : HCPolySupport.Vec d) (a : HCPolySupport.RegCoeffField d) : (HCPolySupport.translateReg z a).toFun = HCPolySupport.translateCoeffField z a.toFun

Carrier bridge for real translation: precomposition on the carrier projects to the raw real translation (rfl). The integer-vector specialization is CoarseGraining's Ch04.translateReg_toFun.

theorem Algsuperdiff.Section3.Provider.Annealed.integral_comp_toFun_translation_transfer_real {d : ℕ} {P : HCPolySupport.RegCoeffLaw d} {X : Set (HCPolySupport.Vec d) → HCPolySupport.CoeffField d → ℝ} (hstat : IsStationaryRealR P) {U : Set (HCPolySupport.Vec d)} (hmeas : MeasureTheory.AEStronglyMeasurable (fun (a : HCPolySupport.RegCoeffField d) => X U a.toFun) P) (hcov : ∀ (V : Set (HCPolySupport.Vec d)) (z : HCPolySupport.Vec d) (a : HCPolySupport.CoeffField d), X (HCPolySupport.translateSet z V) a = X V (HCPolySupport.translateCoeffField z a)) (z : HCPolySupport.Vec d) : ∫ (a : HCPolySupport.RegCoeffField d), X (HCPolySupport.translateSet z U) a.toFun ∂P = ∫ (a : HCPolySupport.RegCoeffField d), X U a.toFun ∂P

Real-translation carrier transfer. A real-translation-covariant raw observable composed with toFun integrates equally on real translates of a set under a real-translation-invariant carrier law. This is the exact analogue of Ch04.integral_comp_toFun_translation_transfer with the integer restriction removed.

theorem Algsuperdiff.Section3.Provider.Annealed.aestronglyMeasurable_blockMatEntry_coarseBlockMatrix_cubeSet {d : ℕ} {P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d} (hP : HCPolySupport.Book.Ch04.RestrictionLawCarrier P) (R : HCPolySupport.TriadicCube d) (alpha beta : HCPolySupport.BlockCoord d) : MeasureTheory.AEStronglyMeasurable (fun (a : HCPolySupport.RegCoeffField d) => HCPolySupport.blockMatEntry (HCPolySupport.coarseBlockMatrix (HCPolySupport.cubeSet R) a.toFun) alpha beta) P

A.e. strong measurability of a coarse block matrix entry on a triadic cube, assembled from the four RestrictionLawCarrier a.e.-measurability lemmas.

theorem Algsuperdiff.Section3.Provider.Annealed.integral_blockMatEntry_coarseBlockMatrix_cubeSet_eq_originCube_of_stationary_real {d : ℕ} {P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d} (hP : HCPolySupport.Book.Ch04.RestrictionLawCarrier P) (hstat : IsStationaryRealR P) (R : HCPolySupport.TriadicCube d) (alpha beta : HCPolySupport.BlockCoord d) : ∫ (a : HCPolySupport.RegCoeffField d), HCPolySupport.blockMatEntry (HCPolySupport.coarseBlockMatrix (HCPolySupport.cubeSet R) a.toFun) alpha beta ∂P = ∫ (a : HCPolySupport.RegCoeffField d), HCPolySupport.blockMatEntry (HCPolySupport.coarseBlockMatrix (HCPolySupport.cubeSet (HCPolySupport.originCube d R.scale)) a.toFun) alpha beta ∂P

Scale-free stationary transfer of coarse block expectations. Under real-translation invariance, every coarse block matrix entry on an arbitrary triadic cube has the same expectation as the corresponding origin-cube entry at the same scale. CoarseGraining's integral_coarseBlockMatrix_entry_cubeSet_eq_originCube_of_stationary is the 0 ≤ R.scale case of this statement.

theorem Algsuperdiff.Section3.Provider.Annealed.integral_blockMatEntry_coarseBlockMatrix_cubeSet_eq_originCube_of_mem_descendantsAtScale {d : ℕ} {P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d} (hP : HCPolySupport.Book.Ch04.RestrictionLawCarrier P) (hstat : IsStationaryRealR P) {n k : ℤ} (hnk : n ≤ k) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d k) n) (alpha beta : HCPolySupport.BlockCoord d) : ∫ (a : HCPolySupport.RegCoeffField d), HCPolySupport.blockMatEntry (HCPolySupport.coarseBlockMatrix (HCPolySupport.cubeSet R) a.toFun) alpha beta ∂P = ∫ (a : HCPolySupport.RegCoeffField d), HCPolySupport.blockMatEntry (HCPolySupport.coarseBlockMatrix (HCPolySupport.cubeSet (HCPolySupport.originCube d n)) a.toFun) alpha beta ∂P

Scale-free descendant transfer. Under real-translation invariance, every coarse block matrix entry on a descendant of an origin cube has the same expectation as the corresponding origin-cube entry at the descendant scale. No sign restriction on the scales is needed; CoarseGraining's integral_coarseBlockMatrix_entry_cubeSet_eq_originCube_of_mem_descendantsAtScale_originCube is the 0 ≤ n case.