EventBudgets #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The two on-event budget slots of the clause-(i) assembly #
ABK26, Section 4.1, Step 2 of p.mathcalE.annular.decomp and Step 3's
gradient resummation.
ClauseOne.clauseOne_bound carries the gradient comparison as the named slot
hcsGn : forall j n, j <= m -> n <= j - 1 ->
gradNf j n <= Kgn * ((m - n) + 2)
* sum_{v < (m-n)+2} A (m - v) ^ 2 ,
where A is the shell block family A(k) = 3^{(2-gamma)k} max_{z in 3^k Z^d ∩ cu_m} ||j_k||_{W^{2,infinity}(z+cu_k)} -- pinned by the A5b interface to
DisplaySlots.shellBlockLatticeReal, which is literally the bracket of the
frozen clause-(i) fourth term and of Support.eventG1's second condition.
This module discharges that slot at the honest fourth-term content
gradNf j n = ( 3^{(2-gamma)n}
max_{z in 3^n Z^d ∩ (cu_j \ cu_{j-1})}
||grad (k_m - k_{n-2})||_{W^{1,infinity}(z+cu_n)} )^2 ,
i.e. annularGradBlock below, at the explicit constant Kgn = 81.
Part E does the same for the companion hcsL2 slot -- the L^2 term of
e.mathcalE.annular.decomp.pre.zero -- at the family
L2f j n = ( 3^{-gamma n}
max_{z in 3^n Z^d ∩ (cu_j \ cu_{j-1})}
||k_m - k_{n-2}||_{L^infinity(z+cu_n)} )^2 ,
i.e. annularL2Block, at the constant Kl2 = 1. The printed content is the
volume-normalized L^2 norm on the same cube; the L^infinity norm dominates
it there, so the family below is the conservative reading (a producer of the
per-cube ugly estimate at the honest L^2 norm feeds it unchanged).
The three moves #
- The layer sum.
k_m - k_{n-2} = sum_{l in (n-2, m]} j_l, andSupport.shellW1InfGradNorm_translate_shellIncrement_leis the triangle inequality at the translated Section 4 gauge. - The lattice-max enlargement. Each shell term is dominated by
9 A(l)--LatticeCover's tiling result, together with the weight arithmetic3^{(2-gamma)n} max(1, 3^{l-n}) <= 9 * 3^{(2-gamma)l}valid for everyl >= n - 1(the honest range: the layer sum starts atl = n - 1, one scale below the cube, which is exactly where the factor9 = 3^2 >= 3^{2-gamma}is spent). - Cauchy--Schwarz with the annulus count. The layer range
(n-2, m]has exactly(m-n)+2members, and reindexing it byl = m - vturns(sum_l A(l))^2 <= ((m-n)+2) sum_l A(l)^2into the printed shape.
Both slots are pointwise in the sample: no event membership and nothing
probabilistic enters. The good event Support.eventG1 is what later bounds
the sums of A(k)^2 these two displays produce; that is Step 3's business,
not this module's.
References #
- ABK26,
p.mathcalE.annular.decompStep 2. - ABK26,
p.mathcalE.annular.decompStep 3. - (the
(1-gamma)shell rate of the volume-normalized cube comparison), consistent with the weight arithmetic of move 2.
Part A -- the weight arithmetic, over abstract reals #
The Step-2 weight arithmetic. For a shell index ll at or above
nn - 1 -- the honest range of the layer sum (n-2, m] -- the cube-comparison
factor max(1, 3^{ll-nn}) is paid for by the constant 9:
3^{(2-gam) nn} max(1, 3^{ll-nn}) <= 9 * 3^{(2-gam) ll} .
Both branches are tight at ll = nn - 1, where the factor is 3^{2-gam}.
Part B -- the per-shell atom bound at the pinned lattice family #
The per-shell atom bound. On the annulus cube z + cu_n with z a
scale-n lattice point of cu_j, the weighted W^{1,infinity} gauge of the
shell j_l is at most 9 A(l), with A = shellBlockLatticeReal the pinned
lattice family of the frozen fourth term, for every layer index l with n - 1 <= l <= m.
Part C -- the layer sum and the reindexing #
Part D -- the honest fourth-term content, and the hcsGn slot #
The head-block gradient content of the clause-(i) fourth term.
The fourth term of e.mathcalE.annular.decomp.pre.zero after the m-vs-L
tail routing of ClauseOne.isUglyJEstimate_routeTail: the annulus maximum of
the volume-normalized W^{1,infinity} gauge of grad (k_m - k_{n-2}),
weighted by 3^{(2-gamma)n} and squared. This is the gradNf family
clauseOne_bound consumes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The layer bound. The weighted annulus maximum of the increment gauge is
at most 9 times the layer sum of the pinned lattice family.
The hcsGn slot of ClauseOne.clauseOne_bound, at Kgn = 81.
The gradient comparison of Step 3, discharged at the honest fourth-term content
annularGradBlock and at the A5b-pinned shell family shellBlockLatticeReal.
Every hypothesis is the enclosing display's own scale ordering; nothing
probabilistic and no event membership enters -- the estimate is pointwise in
the sample.
Part E -- the L^infinity value leg and the hcsL2 slot #
The Step-2 weight arithmetic at the value leg. For a shell index ll
at most mm, the value gauge's own factor 3^{2 ll} is converted into the
shell block weight at the cost of the single factor 3^{gam (mm - nn)}.
The per-shell atom bound at the value leg. On the annulus cube
z + cu_n, the weighted L^infinity norm of the shell j_l is at most
3^{gamma(m-n)} A(l), with A = shellBlockLatticeReal.
The L^2 content of the clause-(i) third term, in the conservative
L^infinity reading.
e.mathcalE.annular.decomp.pre.zero's third term carries the
volume-normalized L^2 norm of k_m - k_{n-2} on z + cu_n; the family
below uses the L^infinity norm of the same increment on the same cube, which
dominates it on a normalized cube. The reading is therefore conservative: any
producer of the per-cube ugly estimate at the honest L^2 norm feeds this
family unchanged. It is the L2f family clauseOne_bound consumes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The value-leg analogue of three_rpow_mul_fmax_le_sum.
The hcsL2 slot of ClauseOne.clauseOne_bound, at Kl2 = 1.
The L^2 comparison of Step 3, discharged at the conservative L^infinity
content annularL2Block and at the A5b-pinned shell family
shellBlockLatticeReal. No constant is lost: the 3^{2 gamma (m-n)} factor
of the printed shape is exactly the square of the per-shell weight 3^{gamma (m-n)}, and the annulus count (m-n)+2 is exactly the length of the layer
range (n-2, m].