CrudeResponseBound #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The crude response bounds and the J -> Lambda middle of Step 1 #
This module is the cube/descendant precursor for the middle of Step 1 of
p.bfA.multiscalebound (ABK26): the passage from the response J(., p, 0; a_L) and J(., 0, q; a_L) at a fine carrier to the multiscale gauges
Lambda_{1/4,2}(z + square_j; a_L) and lambda^{-1}_{1/4,2}(z + square_j; a_L) of the containing cube, and then to a_j through the proved
Lambda-half e.big.Lambda.sensitivity and the proved lambda-transfer of
entry.
The two crude bounds the manuscript uses with an unnamed C are
J(square, p, 0; a) <= C |p|^2 Lambda_{1/4,2}(square'; a) ,
J(square, 0, q; a) <= C |q|^2 lambda^{-1}_{1/4,2}(square'; a) ,
with square the fine carrier and square' a strictly larger cube.
Carrier scope: the cube precursor and its downstream simplex transfer #
The manuscript applies the two crude bounds at square = spx, a simplex of
SW(square_n) contained in the Whitney cube z + square_j. Every statement
below is at a triadic descendant cube R of the gauge cube Q; this file
itself supplies only that cube-carrier stage. The distinction is
mathematically substantive:
b(.; a)is not monotone under inclusion of carriers. Coarse-graining is subadditive downwards (l.subadd.betterer:bfA(V) <= sum_i (|U_i|/|V|) bfA(U_i)), so a single fine carrier'sbis not bounded by the coarse carrier'sb, and in particular|b(spx; a)|is not bounded by|b(supportCube(spx); a)|.Lambda_{s,q}(Q; a)is built from|b(z + square_k; a)|over triadic cubes only (definition (2.23)), so the only carriers it controls are triadic descendants.- The route from cubes to the source simplex is a triadic Whitney decomposition of the
open simplex into countably many disjoint triadic cubes
R_iof scalesk_ifilling it up to a null set, followed byl.subadd.bettererat that dissection and the summability ofsum_i (|R_i|/|spx|) 3^{2 s (j - k_i)}(convergent fors < 1/2, hence ats = 1/4). That decomposition and its counting estimate are now proved downstream inSimplexDissection.leanand consumed bySimplexResponseBound.lean; they are not part of the declarations in this cube-only file.
states that "the tex's step is recovered by supplying that depth bound". This
file proves the scale estimate for the local cube problem (the depth of spx
inside z + square_j is 1 + h_{k+1} - h_k, a b-only bound) but not the
shape half (a simplex is not a triadic descendant). The final section below
proves the scale half at the support cube of a cell of SW(square_m), which is
a triadic descendant of the Whitney cube at precisely the printed depth
(Whitney.mem_whitneySimplexCells_iff,
Whitney.toNat_scale_sub_simplexScale). The downstream simplex files provide
the shape transfer, without changing the local scope of the theorems here or
conferring graph-node status.
What the two assembled legs are #
- the
p̂leg: the crudeLambda-bound ata_L, thene.big.Lambda.sensitivityat the cube — the provedLambdaSq_quarter_le_of_notMem_bad_aeofBigLambdaSensitivity.lean, whose smallness gate is already discharged onnot B_osc and not B_loc; - Reading is the one used: the leg is produced at
a_Lby the polarization display and transferred toa_jhere, exactly as the entry's adopted correction prescribes.
The remaining two arrows of Step 1 — the not B_loc reduction of the two
gauges at a_j to 10 sigmabar_j^{\pm 1} and the running-diffusivity
comparison — are outside this module: the second is proved in
JResponseApplication.lean (sigmaBar_le_four_mul_rpow_mul_sigmaBar,
sigmaBar_le_four_mul_sigmaBar), and the lambda-half of the first is proved
in JSmallness.lean
(sigmaBar_le_ten_mul_cubeLowerEllipticity_of_notMem_badLoc).
Main results #
responseJ_zero_flux_le_coarseBMatrixNorm,responseJ_zero_slope_le_coarseSigmaStarInvMatrixNorm: the one-cube Rayleigh form of the two pure legs.responseJ_zero_flux_le_LambdaSq_of_mem_descendantsAtScale,responseJ_zero_slope_le_lambdaSq_inv_of_mem_descendantsAtScale: the crude response bounds, at a triadic descendant, with the explicit depth constant.
References #
- ABK26 (
p.bfA.multiscalebound, Step 1). - ABK26,
e.J.by.means.of.bfA, the definitions (2.22)--(2.23),e.ellipticities.monotone.ordered,e.bound.one.cube.by.lambdas. - ABK26,
e.big.Lambda.sensitivity(e.SW.def).
The one-cube Rayleigh form of the two pure legs #
The pure-potential leg at one cube. Combining the identity
2 J(U, p, 0; a) = p . b(U; a) p of e.J.by.means.of.bfA with the Euclidean
Rayleigh cap gives
J(z + square_k, p, 0; a) <= (1/2) |b(z + square_k; a)| |p|^2 .
No positivity of b is used: the Rayleigh cap is applied through the absolute
value.
The pure-flux leg at one cube. The mirror of
responseJ_zero_flux_le_coarseBMatrixNorm through
2 J(U, 0, q; a) = q . sigma_*^{-1}(U; a) q:
J(z + square_k, 0, q; a) <= (1/2) |sigma_*^{-1}(z + square_k; a)| |q|^2 .
The crude response bounds at a triadic descendant #
The scale weight 3^{2s(m-k)} of e.bound.one.cube.by.lambdas is
nonnegative.
For every triadic descendant R of Q at scale k, every s > 0 and every
admissible exponent,
J(R, p, 0; a) <= (1/2) . 3^{2 s (Q.scale - k)} . Lambda_{s,q}(Q; a) . |p|^2 .
The constant is explicit and grows by 3^{2s} per triadic generation of depth;
it is 1/2 at k = Q.scale. See the module header for the downstream
simplex-dissection route that transports this cube estimate to the manuscript's
carrier.
For every triadic descendant R of Q at scale k,
J(R, 0, q; a) <= (1/2) . 3^{2 s (Q.scale - k)} . lambda^{-1}_{s,q}(Q; a) . |q|^2 .