LambdaCovariance #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Translation and dilation covariance of the multiscale lower ellipticity #
The frozen Section 2.4 sensitivity gates are stated at the unit cube, against
Algsuperdiff.Frozen.Section24.unitCubeLambda s q a with
a : CoeffOn (cubeDomain (originCube d 0)); ABK26's good local event
e.good.local.events is stated at the off-centre cube
z + square_m, against lambda_{s,q}(z + square_m; a_n). This module supplies
the identification between the two,
lambda_{s,q}(z + square_m; a_n(omega))
= unitCubeLambda s q ( a_n(omega) rescaled by y |-> z + 3^m y ) ,
i.e. the scale-and-translation covariance of the multiscale lower ellipticity for the actual coefficient cutoff.
Proof route #
Nothing analytic is reproved; the identity is the composition of a translation and a dilation, each of which is an existing CoarseGraining interface.
- Translation. CoarseGraining's
Ch02.lambdaSq_translateCube_of_coarseSigmaStarInvMatrixNormreduces the whole descendant tree ofz + square_mto the one-cube covariance ofCh02.coarseSigmaStarInvMatrixNorm. That one-cube covariance is obtained exactly as inTranslationCovariance.lean: the proved CoarseGraining bridgecoarseBlockMatrix_cubeSet_eq_ch02_coarseBlockMatrix_of_aelocallyUniformlyEllipticFieldrewrites the Chapter 2 coarse block matrix as the rawcoarseBlockMatrix (cubeSet Q) a, CoarseGraining'scoarseBlockMatrix_translateSet_eq_translateCoeffFieldis its covariance under a real translation of the domain, andCutoff.coefficientCutoff_translateCutoffSamplemoves the translation from the coefficient field to the sample. The triadic geometry is the provedcubeSet_translateCube_descendantTranslationShift. - Dilation. CoarseGraining's
Ch02.TriadicCoeffFamily.dilateandCh02.TriadicCoeffFamily.isDilation_dilategive, throughCh02.lambdaSq_dilate, the scale normalizationlambda_{s,q}(square_0; dilate (-m) F) = lambda_{s,q}(square_m; F), sincedilateCube (-m) (originCube d m) = originCube d 0. - Unit cube. The frozen
unitCubeLambdais characterized byAlgsuperdiff.Section24.UnitCubeMultiscale.Lambda.characterization; the witness family is the dilated family itself, so the side condition is reflexivity.
The rescaled coefficient object #
unitRescaledCutoffCoeff M Q n omega is the coefficient object on the unit cube
obtained from a_n by the manuscript's rescaling y |-> z + 3^m y, represented by
dilate (-m) applied to the family of the sample translated by
z = triadicCubeShift Q. Its coefficient field is described almost everywhere
by unitRescaledCutoffCoeff_toCoeffField_ae_eq:
(unitRescaledCutoffCoeff M Q n omega).toCoeffField y = a_n(omega)(3^m y + z)
for almost every y in the open unit cube.
Main results #
coarseSigmaStarInvMatrixNorm_cutoff_translateCutoffSample: the one-cube covariance.lambdaSq_cutoff_translateCutoffSample: the multiscale translation covariance.lambdaSq_originCube_dilate: the scale normalization.unitCubeLambda_unitRescaledCutoffCoeff: the full identification.unitRescaledCutoffCoeff_toCoeffField_ae_eq: the pointwise a.e. description of the rescaled coefficient field.
References #
- ABK26 (the definitions (2.22)--(2.23) and the sentence extending them to
translates
y + square_m). - ABK26,
e.good.local.events.
One-cube translation covariance of |sigma_*^{-1}| #
One-cube translation covariance of the coarse block matrix for the actual
coefficient cutoff: if the half-open realization of T is the translate by v
of that of R, then the Chapter 2 coarse block matrix of the cutoff at T
equals the one at R for the translated sample.
Translation covariance of the actual cutoff family's full coarse matrix.
The upper-left block of the cutoff coarse matrix has the same translation covariance.
One-cube translation covariance of |sigma_*^{-1}(Q; a)| for the actual
coefficient cutoff.
Translation covariance of the multiscale lower ellipticity #
Deterministic translation covariance of lambda_{s,q}. For the actual
coefficient cutoff, the multiscale lower ellipticity 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.
Dilation to the unit cube #
dilateCube (-m) normalizes the centered scale-m cube to the unit cube.
Scale normalization of lambda_{s,q}. The multiscale lower ellipticity
of a family on the centered scale-m cube is that of its 3^{-m}-dilation on
the unit cube.
The rescaled unit-cube coefficient object #
The coefficient cutoff a_n, rescaled from the cube Q = z + square_m to
the unit cube by the manuscript's map y |-> z + 3^m y, as a Section 2.4
unit-cube coefficient object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The lambda-transfer identity. The multiscale lower ellipticity of the
cutoff a_n on the cube Q = z + square_m is the frozen unit-cube gauge
unitCubeLambda of the rescaled coefficient object.
The rescaled coefficient field #
The coefficient field of the rescaled unit-cube object is, almost everywhere
on the open unit cube, the manuscript's rescaling y |-> a_n(z + 3^m y) of the
literal cutoff field.