ValueBridge #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The valueL2 slot: the frozen unit-cube L² gauge read on z + cu_n #
ABK26, Section 4.1. The second term of e.ugly.estimate.for.J.pre carries
sigmabar_{n-2}^{-2} || k_L - (k_L - k_m)_{cu_m} - k_{n-2} ||^2_{L^2(z + cu_n)} ,
while the cited unit-cube lemma l.J.sensitivity.no.conditions carries the
frozen UnitCubeSkewW2Infinity.valueL2 of the perturbation on cu_0. As with
the error, the response and the gradient slots, the change of variables is
performed silently; this module proves the value half.
The split #
k_L - (k_L - k_m)_{cu_m} - k_{n-2} = (k_m - k_{n-2}) + (k_L - k_m - (k_L - k_m)_{cu_m}), and the manuscript bounds the second bracket "by the Poincare
inequality". Its own display makes the reading unambiguous: the right-hand
side is 3^{2m} || grad (k_L - k_m) ||^2_{L^infinity(cu_m)}, i.e. the
mean-value bound on the big cube cu_m, not an L^2 Poincare inequality
on z + cu_n (an L^2 Poincare on cu_m cannot be restricted to z + cu_n
without a volume factor 3^{d(m-n)/2}, which the display does not carry).
What is proved here is that mean-value bound, at the explicit constant d^3.
What is re-derived, and why #
ApproximateRecurrence.PrincipalResponseCentre proves the same mean-value
estimate, but (i) file-privately and (ii) only at the same cube for the
average, the supremum and the gauge. Here the average is over cu_m, the
supremum over z + cu_n, and the gauge over cu_m, so the statement is a
different estimate. The entrywise/Euclidean norm comparisons use the common
Section 3 producers; the cube diameter and average estimates are proved below.
The public constant centeringConst is reused unchanged.
Part A -- the frozen L² carrier is a probability space #
The frozen valueL2 carrier is a probability space. Hence the frozen
valueL2 is the manuscript's volume-normalized L^2 norm on cu_0.
The frozen L² value norm is nonnegative: it is an ENNReal.toReal.
A uniform bound on the value field bounds the frozen L² gauge. On a
probability space the L² norm is below the L^infinity norm; the hypothesis
is the almost-everywhere form, which is what the frozen carrier supports.
Part C -- the mean-value (centering) estimate on the origin cube #
The mean-value estimate at the origin cube.
For a frozen shell field g and any point x of the open cube cu_m,
| g(x) - (g)_{cu_m} | <= d^3 . 3^{2m} || grad g ||_{W^{1,infinity}(cu_m)} .
This is the manuscript's "Poincare inequality" step, in the L^infinity
reading its own right-hand side forces. The supremum point x and the
averaging cube are decoupled, which is what the annular chain needs: there the
point runs over the small cube z + cu_n while the average is over cu_m.
Part D -- the manuscript's constant is the cube average #
(k_L − k_m)_Q is the cube average of the shell increment k_L − k_m.
Translation by the zero vector is the identity on shell fields.
The frozen L² value gauge of the centered shell, bounded on z + cu_n.
The shell is h = k_L - C - k_{n-2} at the lattice cube ⟨n, v⟩, and the bound
is the manuscript's own split: the L^infinity norm of k_m - k_{n-2} on
z + cu_n plus the mean-value bound for k_L - k_m - C on cu_m.
C is free here; the instance at the manuscript's (k_L - k_m)_{cu_m} is
valueL2_centeredShellUnitCube_fluxConst_le.
Part F -- the instance at the manuscript's own constant #
The manuscript's centering constant (k_L − k_m)_{cu_m} is antisymmetric, in
the cube-average spelling this module uses.
The hH slot of the ugly chain, at the lattice cube.
Ugly.poincareSplit applied to the two legs of
valueL2_centeredShellUnitCube_le: the frozen L² gauge squared is at most
twice the squared L^infinity content of k_m - k_{n-2} on z + cu_n plus
twice the squared mean-value bound, at Cp = d^3.