ObservableTranslate #

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

The per-observable translation identities of the Section 4.2 lattice maxima #

Provider/GoodEvents/Translate.lean supplies the law-level half of the translation calculus and states explicitly that the remaining half — the per-observable pointwise identities observable(z+□)(ω) = observable(□)(translate z ω) — is supplied by the individual Section 4 modules. This module discharges that half for the three observables the §4.2 lattice maxima read, and packages the compositions with the proved measure preservation.

What the frozen displays actually contain #

Throughout, the sample is translated, never the cube: the manuscript's 𝓔(z+□_m), λ_{γ,2}^{-1}(z+□_{k−2}) and 𝒢(m, y; s, ε) are rendered as compositions with Cutoff.translateCutoffSample. Consequently

the public flux observables Support.fluxCorrectedErrorObservableSup / …SqSup are hard-wired to the origin cube (originCube d m throughout fluxCorrectedErrorRepresentative), and no public Section 4 observable exposes a cube parameter, so there is no second, cube-indexed observable that a translation identity could compare them to. (The atom layer beneath them is cube-indexed — Support.fluxCorrectedCoeffFamily M L m Q omega takes Q : TriadicCube d — so a literal 𝓔(z+□_m) could in principle be written at the triadic cube of scale m and index v; no frozen §4 statement does.) For these two observables the frozen composition is the rendering, so the identities below are the definitional ones a proof actually needs: the translation passes inside the L-supremum, the translations compose additively, and y = 0 is the identity;

Not required by any frozen statement. The lift of that coefficient covariance through the Ch02 error functional — i.e. a theorem "the (∞,2) error on y+□_m at a(ω) equals the error on □_m at a(translate y ω)" — is not proved and is not proved here. No frozen §4 statement needs it: every one of them composes with translateCutoffSample. Any future statement that wants to read the composition as a literal cube translation must prove that lemma first.

Consumers #

mul_sum_indicator_goodEventAt_comp_translate and measure_lt_mul_sum_indicator_goodEventAt are what the centre-union step reads: the two clauses of Frozen.Section4.minimal_scale_separation at the centre Support.triadicLatticePoint (n-1) z have the same law as at the origin.
measure_lt_comp_translateCutoffSample is the law-transport estimate used by the tail step.

References #

ABK26, d.good.event.for.lambda, (the translate convention).
ABK26, p.minimal.scale.separation.sec4.

1. The flux-corrected error observables at a translated sample #

The two public observables of p.mathcalE.annular.decomp are the ones the frozen minimal_scale_separation composes with Cutoff.translateCutoffSample. All four identities per observable are definitional (rfl, or congrArg over the proved group action).