TranslationCovariance

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

Deterministic translation covariance of the cutoff homogenization error

ABK26's induction state d.mathcalS.def controls the multiscale homogenization error mathcal E_{s,infinity,2}(square_m; a_m, sigma_m) at the centered cube square_m, while the local bad event e.Bloc.def lives at the off-centre cube z + square_j. The probabilistic half of the passage between them is the translation invariance of the cutoff sample law (Cutoff.map_translateCutoffSample_cutoffSampleLaw). This module supplies the missing deterministic half: the pathwise identity

mathcal E(z + square_j; a_j(omega))  =  mathcal E(square_j; a_j(tau_z omega)) ,

where tau_z is the translation action Cutoff.translateCutoffSample z on the sample space and z = triadicCubeShift Q is the base point of the cube.

Proof route

Nothing analytic is reproved. The chain is:

• CoarseGraining's Ch02.HomogenizationErrorOnCube_translateCube_of_normalizedBlockResponseMax reduces the whole descendant tree to the one-cube covariance of Ch02.normalizedBlockResponseMax;
• the proved Observable.normalizedBlockResponseMax_cutoff_eq_fromRawCoarseBlock rewrites that one-cube maximum as a finite-dimensional sphere maximum of the raw coarse block matrix coarseBlockMatrix (cubeSet Q) a;
• CoarseGraining's coarseBlockMatrix_translateSet_eq_translateCoeffField is the covariance of the raw coarse block matrix under a real translation of the domain, and Cutoff.coefficientCutoff_translateCutoffSample transports the translation from the coefficient field to the sample.

The only genuinely new ingredient is the elementary triadic geometry cubeSet_translateCube_descendantTranslationShift: a depth-l descendant of a scale-j cube is shifted by the real vector 3^j z when its index is shifted by descendantTranslationShift l z.

Main results

• cubeSet_translateCube_descendantTranslationShift
• normalizedBlockResponseMax_translateCutoffSample
• homogenizationErrorOnCube_translateCutoffSample

References

• ABK26, d.mathcalS.def and e.Bloc.def.

Triadic geometry of the descendant shift

theorem Algsuperdiff.Section3.Provider.BadEvents.cubeSet_translateCube_descendantTranslationShift {d : ℕ} (z : Fin d → ℤ) (l : ℕ) {R : HCPolySupport.TriadicCube d} {j : ℤ} (hR : R.scale = j - ↑l) : HCPolySupport.cubeSet (HCPolySupport.translateCube (HCPolySupport.descendantTranslationShift l z) R) = HCPolySupport.translateSet (fun (i : Fin d) => ↑(z i) * 3 ^ j) (HCPolySupport.cubeSet R)

The half-open realization of a scale-(j - l) cube whose index is shifted by descendantTranslationShift l z is the translate of the original by the scale-j real vector 3^j z. This is the geometry that makes a single real translation act simultaneously on all nine generations of descendants.

One-cube covariance of the normalized block-response maximum

theorem Algsuperdiff.Section3.Provider.BadEvents.normalizedBlockResponseMax_translateCutoffSample {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (v : HCPolySupport.Vec d) {R T : HCPolySupport.TriadicCube d} (hset : HCPolySupport.cubeSet T = HCPolySupport.translateSet v (HCPolySupport.cubeSet R)) (a0 : HCPolySupport.Mat d) (omega : Cutoff.CutoffSample d) : HCPolySupport.Book.Ch02.normalizedBlockResponseMax T (Cutoff.coefficientCutoffTriadicCoeffFamily M m omega) a0 = HCPolySupport.Book.Ch02.normalizedBlockResponseMax R (Cutoff.coefficientCutoffTriadicCoeffFamily M m (Cutoff.translateCutoffSample v omega)) a0

One-cube translation covariance for the actual coefficient cutoff: if the half-open realization of T is the translate by v of that of R, then the normalized block-response maximum of the cutoff at T equals the one at R for the translated sample.

Covariance of the multiscale homogenization error

theorem Algsuperdiff.Section3.Provider.BadEvents.homogenizationErrorOnCube_translateCutoffSample {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (Q : HCPolySupport.TriadicCube d) (s : ℝ) (p q : HCPolySupport.Book.Ch02.MultiscaleExponent) (a0 : HCPolySupport.Mat d) (omega : Cutoff.CutoffSample d) : HCPolySupport.Book.Ch02.HomogenizationErrorOnCube Q s p q (Cutoff.coefficientCutoffTriadicCoeffFamily M m omega) a0 = HCPolySupport.Book.Ch02.HomogenizationErrorOnCube (HCPolySupport.originCube d Q.scale) s p q (Cutoff.coefficientCutoffTriadicCoeffFamily M m (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift Q) omega)) a0

Deterministic translation covariance. For the actual coefficient cutoff, the multiscale homogenization error on an arbitrary triadic cube Q equals the one on the centered cube of the same scale, evaluated at the sample translated by the base point triadicCubeShift Q of Q.

This is the deterministic half of the passage between ABK26's induction state (stated at square_j) and the local bad event (stated at z + square_j).