Scaling

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

Section 3 cube normalization

This file supplies the literal triadic change of variables used to feed a coefficient restriction on the centered cube square_m into the already frozen unit-cube observables. The normalized coefficient is the pullback

x ↦ a (3^m x)

on square_0. It is constructed by CoarseGraining's public CoeffOn.dilate; hence its ellipticity constants are the same as those of the source restriction and its representative agrees almost everywhere with the displayed pullback.

References

• ABK26, the scale-invariant cube conventions preceding Section 2.5.
• ABK26, Section 3, where square_m denotes originCube d m.

theorem Algsuperdiff.Section3.Observable.dilateOriginCube_neg_scale (d : ℕ) (m : ℤ) : HCPolySupport.Book.Ch02.dilateCube (-m) (HCPolySupport.originCube d m) = HCPolySupport.originCube d 0

Dilation by 3^(-m) sends the centered cube square_m to the unit centered cube square_0.

noncomputable def Algsuperdiff.Section3.Observable.unitRescaledCoeffOn {d : ℕ} (m : ℤ) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d m))) : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))

The exact unit-cube pullback of a coefficient restriction on square_m.

The underlying representative is x ↦ a (3^m x) almost everywhere on square_0. There is no fallback branch and no finite-scale surrogate.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Observable.unitRescaledCoeffOn_toCoeffField_ae_eq {d : ℕ} (m : ℤ) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d m))) : (unitRescaledCoeffOn m a).toCoeffField =ᵐ[HCPolySupport.volumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d 0))] HCPolySupport.Book.Ch02.dilateCoeffField (-m) a.toCoeffField

The representative of unitRescaledCoeffOn is exactly the pullback x ↦ a(3^m x) almost everywhere on the unit cube.

theorem Algsuperdiff.Section3.Observable.dilatedFamily_root_aeeq_unitRescaledCoeffOn {d : ℕ} (m : ℤ) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d m))) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (hF : (F.coeffOn (HCPolySupport.originCube d m)).AEEq a) : ((HCPolySupport.Book.Ch02.TriadicCoeffFamily.dilate (-m) F).coeffOn (HCPolySupport.originCube d 0)).AEEq (unitRescaledCoeffOn m a)

A compatible coefficient family on square_m, dilated by 3^(-m), agrees on square_0 with unitRescaledCoeffOn. This is the bridge used to read every unit-cube observable as the corresponding literal cube-m quantity.