Translate

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

The translation calculus of the cutoff sample carrier

Support layer for the Section 4 good-event A. Every Section 4 event is built from the frozen Algsuperdiff.Frozen.Section4.goodEventAt, which is a Cutoff.translateCutoffSample y preimage (resolution A4: the sample is translated, never the cube). Reading such an event, comparing two of them, and transferring its probability from a lattice point z to the origin all reduce to three facts about Cutoff.translateCutoffSample:

• it is a group action of Vec d — translate 0 = id and translate z ∘ translate w = translate (z + w);
• each translate z is a measurable equivalence of the carrier; and
• each translate z preserves the cutoff-sample law.

The third is not re-derived here. It is the proved Algsuperdiff.Section3.Cutoff.map_translateCutoffSample_cutoffSampleLaw (Section3/Cutoff/Symmetry.lean), which holds for every real vector z: Vec d, not merely for lattice shifts: it descends J1 stationarity of the zero shell through the exact marginal scaling law and the independence of the shell coordinates. Section 4's lattice sums therefore need no additional stationarity input; see the module note below.

Stationarity strength available to Section 4

What the graph's stationarity gaps still require is not a stronger invariance of the law: it is the (separate) claim that the observable being maximized is the same function of the translated sample, i.e. the pointwise identities observable(z + □) (ω) = observable(□) (translate z ω). Those identities are per-observable statements and are proved in the individual Section 4 modules; this module supplies only the law-level half.

References

• ABK26, d.good.event.for.lambda, (the translate convention).

1. The additive action

theorem Algsuperdiff.Section4.Provider.GoodEvents.translateCutoffSample_zero {d : ℕ} (omega : Section3.Cutoff.CutoffSample d) : Section3.Cutoff.translateCutoffSample 0 omega = omega

The zero translation is the identity. Pointwise form.

theorem Algsuperdiff.Section4.Provider.GoodEvents.translateCutoffSample_zero_eq_id {d : ℕ} : Section3.Cutoff.translateCutoffSample 0 = id

The zero translation is the identity. Function form; this is the shape consumed when a preimage is rewritten.

2. Preimage calculus

theorem Algsuperdiff.Section4.Provider.GoodEvents.preimage_translateCutoffSample_zero {d : ℕ} (t : Set (Section3.Cutoff.CutoffSample d)) : Section3.Cutoff.translateCutoffSample 0 ⁻¹' t = t

The preimage form of translate 0 = id.

3. The law-level statements

theorem Algsuperdiff.Section4.Provider.GoodEvents.measurePreserving_translateCutoffSample {d : ℕ} (M : Section3.ABKModel d) (z : HCPolySupport.Vec d) : MeasureTheory.MeasurePreserving (Section3.Cutoff.translateCutoffSample z) ↑(Section3.Cutoff.cutoffSampleLaw M) ↑(Section3.Cutoff.cutoffSampleLaw M)

Every real translation preserves the cutoff-sample law.

The bundled MeasurePreserving form of the proved Cutoff.map_translateCutoffSample_cutoffSampleLaw; the translation vector is an arbitrary real vector, in particular any triadic lattice point.

theorem Algsuperdiff.Section4.Provider.GoodEvents.measure_preimage_translateCutoffSample {d : ℕ} (M : Section3.ABKModel d) (z : HCPolySupport.Vec d) {t : Set (Section3.Cutoff.CutoffSample d)} (ht : MeasurableSet t) : ↑(Section3.Cutoff.cutoffSampleLaw M) (Section3.Cutoff.translateCutoffSample z ⁻¹' t) = ↑(Section3.Cutoff.cutoffSampleLaw M) t

The per-z transfer of a probability. A measurable event and its z-translate carry the same mass, for every real z.