ErrorTransport #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The (2,2) error transport #
ABK26, Section 4.1 reads the homogenization-error functional π_{s,p,q} on
the translated cube z + β‘_n, and then feeds it to the Section 2.4
sensitivity machinery, which is stated only on the unit cube. The bridge
between the two is the manuscript's unremarked change of variables y β¦ z + 3^n y.
Section3.Provider.BadEvents.unitRescaledCutoffCoeff performs exactly that
change of variables on the coefficient cutoff: the sample is translated by the
base point z = triadicCubeShift Q of the cube, and the resulting triadic
family is dilated by 3^{-Q.scale} onto the unit cube. It is the object at
which the frozen Section 2.4 lower-ellipticity gate is already read
(unitCubeLambda_unitRescaledCutoffCoeff). This module supplies the same
identification for the error functional.
What is proved #
unitCubeHomogenizationError_dilatedFamilyβ the reusable core: for any triadic coefficient familyF, any exponent pair and any comparator matrix, the frozen unit-cube error of the root ofdilate (-m) Fis the literal manuscript error onβ‘_mofFitself. This is the statement a flux-corrected rescaling layer will consume verbatim once a flux-corrected triadic family exists; nothing in it mentions the cutoff.unitCubeHomogenizationError_unitRescaledCutoffCoeffβ its instance at the proved rescaling layer, i.e. the transport at the plain cutoff familyCutoff.coefficientCutoffTriadicCoeffFamily.unitCubeHomogenizationError_unitRescaledCutoffCoeff_eq_cutoffRaw22β the literal-observable leg at(2,2).unitCubeHomogenizationError22_unitRescaledCutoffCoeff_eq_annularErrorAtomβ theπ’βnormalization (cutoff leveln β 2, comparatorΟ_{nβ2} Id) at a lattice cubeβ¨n, vβ©: the unit-cube error at the rescaled coefficient object is literallySupport.annularErrorAtom M n tevaluated at the sample translated bySupport.triadicLatticePoint n v. This is the translated-sample rendering used throughout.
Exact, not almost-everywhere #
Every identity above is an exact pointwise equality of reals: no null set,
no representative choice, no normalization constant. The reason is structural.
The frozen characterization
Algsuperdiff.Frozen.Section24.unitCubeHomogenizationError_characterization is
quantified over every compatible family; at the root of a dilated family the
compatible family is that dilated family itself, so its a.e. side condition is
discharged by CoeffOn.A.refl. CoarseGraining's
Book.Ch02.HomogenizationErrorOnCube_dilate is an equality with factor 1,
and the (2,2) characterization of Support.cutoffHomogenizationErrorRaw22
proves on the very same HomogenizationErrorOnCube expression, so the two ends
meet with no residual scaling.
The single a.e. statement in this file is
unitCubeHomogenizationError22_unitRescaledCutoffCoeff_ae_eq_annularErrorObservable,
and its null set comes from elsewhere: it is the composition of the exact
identity with Support.annularErrorAtom_ae_eq_annularErrorObservable, where a
measurable modification is selected, as everywhere in the π’β lane.
Transporting that a.e. identity along the translation is legitimate because
every real translation preserves the cutoff-sample law
(GoodEvents.measurePreserving_translateCutoffSample).
Route #
unitCubeHomogenizationError t p q (unitRescaledCutoffCoeff M Q L Ο) aβ
= π(β‘β; dilate (βQ.scale) (a_L at Ο translated by z), aβ) [frozen char.]
= π(β‘_{Q.scale}; a_L at Ο translated by z, aβ) [CoarseGraining ..._dilate]
= annularErrorAtom M Q.scale t (translate z Ο) [(2,2) char., backwards]
What the manuscript says, and does not say #
d.mathcal.E extends the error functional to translated cubes in exactly one
sentence -- "We extend these definitions to translations y + β‘_m of β‘_m in
the obvious way" -- and says nothing at all about the behaviour of π under a
dilation. The only explicit rescale-and-translate passage in the manuscript (
inside the proof of l.lambda.sensitivity) is written for Ξ»_{s,q}, not for
π.
The rescaling this module supplies is therefore the step ABK26 performs silently. What is proved here is the error half of that step, and it is proved as an exact equality, so no constant and no inequality direction is introduced.
- -- the "obvious way" extension is a theorem, and is a.e.-tolerant. The rendering used here is the proved Support convention (translate the sample, never the cube), so no off-grid cube object is introduced and the a.e. tolerance is not consumed.
- -- the
q = βbranches should sum tol β€ n, notl β€ m. Invisible here: every statement in this module is atn = m(HomogenizationErrorOnCubefixesn := Q.scale). - Every comparator below is
isotropicComparatorMatrix ΟwithΟaPositiveScalar, which is that locus (and isscalarMatrix (Ο : β)on the nose). - -- all concern constants, exponents, annulus multiplicity or the truncation level inside the estimates, not the definition of the functional or its behaviour under the change of variables. None bears on an equality of two readings of the same functional.
References #
The base point of a triadic cube, at a lattice index #
The translation vector carrying β‘_k onto the cube β¨k, vβ© is the
Section 4 lattice point 3^k v. This is the index-level spelling of
Homogenization.triadicCubeShift, and it is what lets the transport below be
read at the lattice enumerations of Support.latticeAnnulusSet.
The reusable dilation glue #
The scale normalization of the homogenization error. For an arbitrary
triadic coefficient family F, the frozen unit-cube error functional read at
the root restriction of the 3^{-m}-dilated family is exactly the literal
manuscript error π_{s,p,q}(β‘_m; F, aβ).
Nothing here is specific to the coefficient cutoff, to the exponents, or to an isotropic comparator; this is the statement any other rescaling layer (for instance a flux-corrected one) consumes unchanged, once it exhibits its coefficient object as the root of a dilated triadic family.
The transport at the proved rescaling layer #
The error transport. The frozen unit-cube homogenization error, read
at the rescaled coefficient object unitRescaledCutoffCoeff M Q L Ο, is the
literal manuscript error functional on the centered cube of the same scale as
Q, evaluated at the sample translated by the base point of Q.
This holds at every exponent pair, every comparator matrix, every cube and
every cutoff level; the π’β atom below is one instance.
The (2,2) leg, proved at the Section 4 literal observable
Support.cutoffHomogenizationErrorRaw22.
The π’β annular atom #
The (2,2) error transport at the π’β normalization, cube form. The
frozen unit-cube error, read at the coefficient cutoff of level Q.scale β 2
rescaled from Q onto the unit cube and compared against Ο_{Q.scaleβ2} Id,
is exactly the π’β atom of Support.ErrorAtoms at the sample translated by
the base point of Q.
Both sides are the literal manuscript quantity, and the equality is exact.
The (2,2) error transport at the π’β normalization, lattice form.
The same identity at the cube β¨n, vβ© = 3^n v + β‘_n of the Section 4 lattice
enumerations, so that the translation is the lattice point
Support.triadicLatticePoint n v in the exact spelling of the good events and
of the frozen annular decomposition.
The measurable-observable corollary (the only a.e. statement here) #
This is the exact identity above composed with
Support.annularErrorAtom_ae_eq_annularErrorObservable, whose null set is the
representative-choice set of the π’β lane; the composition is legitimate
because every real translation preserves the cutoff-sample law. Consumers that
need measurability use this form; consumers that stay at the literal manuscript
quantity use the exact form above.