PerScaleDefect #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The per-scale defect estimate of the Section 3.5 negative-norm lemma #
This module proves the per-scale estimate that feeds the large-scale half of
l.Besov.norms. Fix a cube Q = \cu_m, a depth j = m - n, and let
v = v(\cdot,\cu_m,p,q;\a) be the canonical maximizer on Q. For every
descendant R = z+\cu_n of Q at depth j, the manuscript compares the
average (\nabla v)_R with the local coarse projection
\s_*^{-1}(R)(q+\k(R)p) - p attached to R itself, and shows that the
descendant average of the squared deviation is controlled by the response
defect average, at the price of the multiscale ellipticity weight
3^{2s(m-n)} \lambda_{s,r}^{-1}(\cu_m;\a).
The estimate is proved here at an arbitrary admissible exponent
r \in [1,\infty], which is the range the manuscript states.
How the manuscript displays are distributed over the declarations #
The upstream Chapter 5 estimate used below already carries the one-cube step
composed with the first inequality: it is proved from
Ch02.vecNormSq_averageGradient_le_matrixNorm_sigmaStarInvCoarse_mul_variationEnergyValue,
which is the single inequality |(\nabla w)_R|^2 \le |\s_*^{-1}(R)| \fint_R \nabla w \cdot \s \nabla w. Consequently the square root \s_*^{1/2}(R)
never has to be constructed: the manuscript's two-step passage through
\s_*^{1/2} is realized upstream as one inequality with the same endpoints.
What remains is the second inequality, e.bound.one.cube.by.lambdas, and that
is maxDescendantSigmaStarInv_le_lambdaSqCoeffField_inv below.
Formalization readings #
- The descendant index set. The manuscript sums over
z \in 3^n\Zd \cap \cu_m; that index set is the set of triadic descendants of\cu_mat depthm-n, and\avsumisdescendantsAverage. The translation is the one already used throughout the Chapter 5 vocabulary. - The local coarse projection. The comparison vector at the descendant
RiscoarseScaleSeparation a ha R p qofCarriers.lean, evaluated atRand not at the parent cube. This is the vector printed the same descendant-evaluated coarse projection occurs inside a difference, with the two- psummands cancelled. By the identity ofCarriers.leanit is the Chapter 4 measurable representative of(\nabla v_{n,z})_R, which is how the manuscript'se.v.spatial.averagesenters. - The exponent carrier. The manuscript's
r \in [1,\infty]isCh02.MultiscaleExponenttogether withIsAdmissible, and\lambda_{s,r}(\cu_m;\a)isCh04.lambdaSqCoeffField. No exponent is pinned: the two Chapter 2 inputs used below are already stated for every admissible exponent.
The per-scale squared deviation #
The manuscript quantity | (\nabla v)_R - (\s_*^{-1}(R)(q + \k(R)p) - p) |^2, for the canonical maximizer v = v(\cdot,Q,p,q;\a) of the parent cube
Q and a descendant cube R.
The first summand is the Chapter 4 measurable representative of the average of
\nabla v over R, and the second is the local coarse projection of
Carriers.lean at R.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ellipticity weight conversion #
The ellipticity weight conversion, at an arbitrary admissible exponent.
The largest coarse |\s_*^{-1}| over the depth-j descendants of Q is at
most 3^{2sj} \lambda_{s,r}^{-1}(Q;\a).
Its first inequality, |P|^2 \le |\s_*^{-1}(R)| |\s_*^{1/2}(R)P|^2
(e.ellipticities.monotone.ordered), is already contained in the Chapter 5
estimate quoted in the next theorem.
The defect display #
The display chain on the Carriers.lean carrier. The descendant average of
the squared deviation of (\nabla v)_R from the local coarse projection at R
is at most twice the largest coarse |\s_*^{-1}| over those descendants times
the response partition defect.
The one-cube step (composed with the first inequality) is
e.v.spatial.averages together with e.energymaps.nonsymm, and the passage to
the average is e.quadresp.nosymm; both are supplied by the Chapter 5
energy-defect theory. The only work done here is the replacement of the
Chapter 4 average (\nabla v_{n,z})_R by the printed vector
\s_*^{-1}(R)(q+\k(R)p) - p, which is the identity of Carriers.lean.
The per-scale defect estimate #
The per-scale defect estimate, at an arbitrary admissible exponent r \in [1,\infty].
For a cube Q and a depth j, the descendant average of | (\nabla v)_R - (\s_*^{-1}(R)(q + \k(R)p) - p) |^2 is at most 2 \cdot 3^{2sj} \lambda_{s,r}^{-1}(Q;\a) times the response defect average. This is the
combination of the three displays, with the literal manuscript factor 2.
The per-scale defect estimate in the manuscript's scale indexing. For
n \le m the descendants of \cu_m at depth m-n are the cubes z+\cu_n
with z \in 3^n\Zd \cap \cu_m, and the right side is the manuscript's
2 \avsum_z ( J(z+\cu_n,p,q;\a) - J(\cu_m,p,q;\a) ) weighted by
3^{2s(m-n)} \lambda_{s,r}^{-1}(\cu_m;\a).
The square-root form of the per-scale defect estimate. This is the shape
in which sums the estimate over n: the factor 3^{s(m-n)} is the one that
turns the multiscale Poincaré weight 3^{-(m-n)} into the manuscript's
3^{-(1-s)(m-n)}.