JBoundByBesov #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The J-bound composite of Section 3.5, on the multiscale right-hand side #
This module assembles the estimate of ABK26 l.J.bound.by.Besov for the
canonical maximizer on a centred cube, with the negative Sobolev factor of the
printed display replaced by the proved multiscale upper bound of this
directory. The two structural features of the printed right-hand side that the
consumer needs are retained verbatim: the literal factor 2 and the literal
depth-one sum \sum_{z \in 3^{m-1}\Zd \cap \cu_m} of the response defects.
Nothing about the status of the lemma l.J.bound.by.Besov is asserted here.
Route #
- The digging room. The response of the ordinary central child is the child
average of the child half-energy
(
JUpperBoundWeakNorms.responseJOnCube_eq_cubeAverage_topHalfEnergy); the pointwise polarization\tfrac12 \xi\cdot\s\xi \le \eta\cdot\s\eta + (\eta-\xi)\cdot\s(\eta-\xi)at an elliptic matrix replaces it by the parent energy plus the parent-minus-child difference energy; the difference energies of the other depth-one children are nonnegative and are added; and the summed difference energy is the summed response defect, by the upstream partition identity for the descendant average of the half-difference energy and the response partition defect. The last step is where the literal2and the literal depth-one sum are produced. - The Caccioppoli step.
CentralChildCaccioppoli.leanbounds the parent-coefficient energy on the ordinary central child by the upstream interior Caccioppoli right-hand side of the parent, andJBesovPrefactor.leanbounds the diagonal prefactor on0 < s \le 1/4by a dimension-only envelope times the three displayed factors\Theta^{s/(1-2s)},\Lambda_{s,1}and3^{-2m}. - The oscillation step, replacing.
OscillationPoincare.leanbounds the parent oscillationL^2square that the Caccioppoli right-hand side leaves by the square of the coordinate sum of the negative circ Besov norms of the gradient coordinates at(s,p,q) = (1,2,1). - The centring step. Each depth-
jcirc average of a gradient coordinate is bounded by twice the depth-jcirc average of the corresponding coordinate of the gradient defect plus twice the squared coordinate of the comparison vectorc = \s_*^{-1}(\cu_m)(q+\k(\cu_m)p) - p, because the descendant average of the gradient is the descendant average of the defect shifted byc. Summing the circ weights, whose total is at most\tfrac32 \cdot 3^m, and passing to the supremum withHomogenization.cubeBesovCircNorm_le_of_forall_entry_le, which is taken one coordinate at a time, by dominating a single coordinate entry with the full coordinate sum and re-summing over thedcoordinates, at the cost of a further factord, converts the coordinate sum of circ norms into the multiscale average sum of the centred gradient plus the length ofc. - The coordinate aggregation. The bound produced by step 3 aggregates the
coordinates in
\ell^1, while the printed multiscale sum aggregates them inside each depth term in the Euclidean norm. Cauchy's inequality in the coordinate index converts one into the other at the cost of\sqrt d, which the dimension-only constant absorbs. This is the conversion thatOscillationPoincare.leanrecords but does not formalize; it is formalized here, inweighted_sum_sqrt_le.
Correspondence with the printed display #
The printed right-hand side is
`C \Lambda_{s,1}(\cu_m) (\Lambda_{s,1}/\lambda_{s,1})^{s/(1-2s)} 3^{-2m} | \nabla v |_{\Hminusul(\cu_m)}^2
- \sum_{z\in 3^{m-1}\Zd\cap\cu_m} 2 (J(z+\cu_{m-1}) - J(\cu_m))`.
The composite below carries \Lambda_{s,1}(\cu_m;\a) as
Ch02.LambdaS (originCube d m) s, whose body is the q = 1 convention
Ch02.LambdaSq (originCube d m) s (.finite 1); the ellipticity ratio as
Ch02.ThetaRatio (originCube d m) s s, whose body is
Ch02.LambdaS (originCube d m) s / Ch02.lambdaS (originCube d m) s, raised to
s/(1-2s); and the depth-one sum
verbatim on descendantsAtDepth (originCube d m) 1, which is the set of the
3^d children z+\cu_{m-1} of \cu_m. Two features differ from the printed
display and are load bearing.
- The negative Sobolev factor is replaced by its multiscale upper bound.
3^{-2m}\|\nabla v\|_{\Hminusul}^2is replaced by the square ofcentredMultiscaleAverageSum, the manuscript sum\sum_{n\le m} 3^{-(m-n)}(\avsum_z|(\nabla v - c)_{z+\cu_n}|^2)^{1/2}. The scale weight3^{-m}of the printed display is carried inside that sum, by the reindexingn = m-j, exactly asCarriers.scaledNegHMinusOnecarries it at the use site. The replacement is in the direction of a weaker estimate: the proved bridgeMultiscalePoincareBridge.scaledNegHMinusOne_le_multiscaleAverageSumbounds the negative Sobolev object by the multiscale sum and no reverse comparison is available, so no statement here is equivalent to the printed one. The bridge's own right-hand side is the Euclidean coordinate aggregate of the same circ norms, which lies below the coordinate sum used here; the comparison is therefore in the stated direction only up to the√dcoordinate aggregation, and no declaration in this directory compares the negative Sobolev object to the multiscale average sum directly. - The centring term is explicit. Because the multiscale sum of item 1 is
the sum of the centred gradient, the centring of step 4 leaves the
summand
|c|, writtenReal.sqrt (vecNormSq (coarseScaleSeparation ...)). Squared, it is exactly the third summand of the consumer display at ,C \shom_L \E [ | \s_{L,*}^{-1}(\cu_m)(q+\k_L(\cu_m)p) - p |^2 ], so the consumer already carries it. The manuscript's own copy of that summand comes from squaring the fourth printed term ofe.Besov.norms.gradient, which carries the discount3^{-(m-L_0)}; the term produced here carries none, matching the undiscounted form. It is therefore a second, independent copy of the same summand, which the consumer's constant absorbs. It is kept explicit rather than absorbed.
Formalization readings #
The readings of Carriers.lean, PerScaleDefect.lean and BesovNorms.lean
(the pairing is volume normalized; a vector field's dual seminorm is the
Euclidean \ell^2 aggregate; the index set z \in 3^n\Zd \cap \cu_m is the set
of triadic descendants at depth m-n and \avsum is descendantsAverage; the
bi-infinite sum over n \le m is the supremum of its partial sums) are
inherited unchanged. One further reading is specific to this module.
The multiscale average sum is the supremum of its partial sums.
centredMultiscaleAverageSum is ⨆ N, \sum_{j < N} 3^{-j}(\ldots)^{1/2}. The
supremum is finite: partialMultiscaleSum_le_fourTerm bounds every partial sum
by the four printed terms of e.Besov.norms.gradient, at the admissible
parameters L_0 = m, s = 1/4 and r = \infty, so the defining family is
bounded above and centredMultiscaleAverageSum_le_fourTerm transfers the
four-term bound to the supremum itself at every admissible parameter choice.
Scalar helpers #
The circ entry at (s,p,q) = (1,2,1) #
The centred multiscale average sum #
The manuscript multiscale average sum
\sum_{n \le m} 3^{-(m-n)} ( \avsum_{z} | (\nabla v - c)_{z+\cu_n} |^2 )^{1/2}
, for the canonical maximizer gradient defect on \cu_m and
the comparison vector c = \s_*^{-1}(\cu_m)(q+\k(\cu_m)p) - p.
The reindexing n = m - j turns the printed discount 3^{-(m-n)} into 3^{-j}
and the printed index set z \in 3^n\Zd \cap \cu_m into the triadic descendants
at depth j; the bi-infinite sum over n \le m is the supremum of the partial
sums, exactly as in BesovNorms.lean.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Every partial multiscale sum is bounded by the four printed right-hand terms of
e.Besov.norms.gradient. This is the proved four-term display of
BesovNorms.lean, restated at an arbitrary truncation of the depth range.
Every partial multiscale sum is below the multiscale average sum.
The multiscale average sum obeys the four-term display of l.Besov.norms.
This is the form in which the composite below meets the proved
e.Besov.norms.gradient estimate.
The centring step #
The centring step. The scaled coordinate sum of the negative circ norms of the maximizer gradient is bounded by the multiscale average sum of the centred gradient plus the length of the comparison vector, with a dimension-only constant. The second summand is the term the manuscript already carries, squared.
The subadditivity digging room #
The subadditivity digging room. The response of the ordinary central child
\cu_{m-1} is bounded by the parent-coefficient energy of the parent maximizer
on that child, plus the literal depth-one sum of twice the response defects.
The composite #
The composite, with the negative Sobolev factor replaced by its proved
multiscale upper bound. For the canonical maximizer on \cu_m, the response
of the ordinary central child \cu_{m-1} is bounded by a dimension-only
constant times the coarse upper ellipticity \Lambda_{s,1}, times the coarse
ellipticity ratio raised to s/(1-2s), times the square of the multiscale
average sum of the centred gradient plus the length of the comparison vector,
plus the literal depth-one sum of twice the response defects.
The composite on the Chapter 4 restriction response observable. This is
the same estimate written on the carrier that the Section 3 response observable
J(\cu_m, p, q\;\a) uses, so that a Section 3 consumer meets it after
instantiating the loads.