SmallScaleTail #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The small-scale tail of the Section 3.5 negative-norm lemma #
This module establishes the deterministic estimates behind the small-scale part
of the multiscale sum that occurs in the proof of l.Besov.norms. Nothing
about the left-hand side of e.Besov.norms.gradient, and nothing about the
status of the lemma, is asserted here.
Fix a cube Q = \cu_m and a scale n < L_0. At such a
scale the manuscript makes no use of the response defect: it bounds the
descendant averages (\nabla v)_{z+\cu_n} directly by the energy of the
maximizer, pays the multiscale ellipticity weight 3^{2s(m-n)}, and then sums
the resulting geometric series over the bi-infinite range n < L_0.
Formalization readings #
- The bi-infinite tail. ABK26 sums over
nfrom-\inftytoL_0-1. That range is enumerated here byn = L_0 - 1 - iwithi : \N, and the sum is the unconditionaltsumof the nonnegative summand. Summability is proved, not assumed; a finite-range corollary overFinset.range Nis also supplied, so a consumer that produces only finite partial sums can use the same right-hand side. - The energy carrier.
\| \s^{1/2} \nabla v \|^2_{\underline L^2(\cu_m)}is written as the cube average of the Chapter 2 quadratic energy integrand of the canonical maximizer, which is literally\fint_{\cu_m} \nabla v \cdot \s \nabla v. Its identification with2 J(\cu_m,p,q;\a)ise.Jenergyv.nosymmand is proved here. - The manuscript constant
C. ABK26 prints an unspecifiedC. The explicit values carried below are2\sqrt 2for both terms:\sqrt 2from the pointwise Euclidean inequality|x-y|^2 \le 2(|x|^2+|y|^2)used for the triangle step, and2from the geometric tail\rho/(1-\rho) \le 2, valid for both discounts\rho = 3^{-(1-s)}and\rho = 3^{-1}-- the first becauses \le 1/2, the second unconditionally. - The exponent carrier. As in
PerScaleDefect.lean, the manuscript'sr \in [1,\infty]isCh02.MultiscaleExponenttogether withIsAdmissible, and no exponent is pinned.
The energy carrier \| \s^{1/2}\nabla v \|_{\underline L^2(\cu_m)} #
The manuscript quantity \| \s^{1/2} \nabla v \|^2_{\underline L^2(\cu_m)},
written literally as the cube average of the Chapter 2 quadratic energy
integrand \nabla v \cdot \s \nabla v of the canonical maximizer on Q.
Equations
- One or more equations did not get rendered due to their size.
Instances For
e.Jenergyv.nosymm on this carrier. The squared energy norm of the
canonical maximizer gradient is twice the Chapter 4 response observable of the
cube. This is the cube instance of the identity for the Chapter 4 dependent
family; the node's quantifier over every admissible bounded Lipschitz U is
untouched, and the mathematics is upstream
(responseJOnCube_eq_cubeAverage_topHalfEnergy in CoarseGraining).
The manuscript quantity \| \s^{1/2} \nabla v \|_{\underline L^2(\cu_m)}.
Equations
Instances For
The one-scale energy bound #
The first inequality. The descendant average of the squared gradient
averages of the parent maximizer is at most the largest coarse |\s_*^{-1}|
over those descendants times the squared energy norm.
This is e.energymaps.nonsymm applied on each descendant cube to the
restriction of the parent maximizer, followed by the additivity of the energy
average over the partition.
The one-scale energy bound, at an arbitrary admissible exponent r \in [1,\infty].
The square-root form of the one-scale energy bound.
The triangle step #
The triangle step. For a fixed depth, the root of the descendant average of the deviation from the parent comparison vector is controlled by the one-scale energy bound plus the length of the comparison vector itself.
The geometric tail #
The bi-infinite tail #
Summability of the bi-infinite tail.
The small-scale tail. The bi-infinite multiscale sum over the scales n < L_0 is bounded by the low-scale tail term and the constant tail term of
e.Besov.norms.gradient, with the manuscript constant C given the explicit
value 2\sqrt 2 in both places.
The finite-range form of the small-scale tail. Every partial sum of the tail obeys the same bound, so a consumer that produces the multiscale sum only over a finite range of scales can use the identical right-hand side.