Carriers

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

Carriers for the Section 3.5 negative-norm estimates

This module fixes the deterministic comparison vector used by the negative-norm lemmas of Section 3.5 of ABK26.

• coarseScaleSeparation is the manuscript comparison vector \s_*^{-1}(\cu_m)(q + \k(\cu_m)p) - p, written literally from the Chapter 2 coarse matrices.

The single theorem of the file identifies coarseScaleSeparation with the Chapter 4 measurable representative of the whole-cube maximizer gradient average, which is the manuscript's e.v.spatial.averages on this carrier.

Formalization readings

Two readings are recorded so the correspondence with the manuscript is unambiguous.

1. Everything is volume normalized. ABK26 writes the Section 3.5 displays with normalized averages \fint_U, and that is the reading taken here: the Chapter 2 normalized average over the domain of a triadic cube is literally the cube average of the same cube, which is what ch02_average_cubeDomain_eq_cubeAverage records. No factor |U| separates the two sides of the identity below.
2. The comparison vector is written from the coarse matrices, not reformulated. coarseScaleSeparation applies Ch02.sigmaStarInvCoarse and Ch02.kappaCoarse, at the coefficient field restricted to Q, to the pair (p, q) exactly as printed. Its identification with the Chapter 4 maximizer-gradient average is then a theorem about that literal expression rather than a matter of definition.

The coarse scale-separation vector

noncomputable def Algsuperdiff.Section3.Provider.Besov.coarseScaleSeparation {d : ℕ} (a : HCPolySupport.RegCoeffField d) (ha : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField a) (Q : HCPolySupport.TriadicCube d) (p q : HCPolySupport.Vec d) : HCPolySupport.Vec d

The manuscript comparison vector \s_*^{-1}(\cu_m)( q + \k(\cu_m) p ) - p, written on the triadic cube Q from the Chapter 2 coarse matrices of the restricted coefficient field.

Equations

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

theorem Algsuperdiff.Section3.Provider.Besov.coarseScaleSeparation_eq_canonicalScalarResponseGradientAverageCubeSet {d : ℕ} [NeZero d] (a : HCPolySupport.RegCoeffField d) (ha : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField a) (Q : HCPolySupport.TriadicCube d) (p q : HCPolySupport.Vec d) : coarseScaleSeparation a ha Q p q = HCPolySupport.Book.Ch04.canonicalScalarResponseGradientAverageCubeSet Q Q p q a.toFun

The manuscript identity e.v.spatial.averages on this carrier. The Chapter 4 measurable representative of the whole-cube average of the canonical maximizer gradient is the coarse scale-separation vector of the same cube.