FiniteQTransfer #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: the finite-q multiscale transfer of the cube-maximum form #
The printed step
lambda^{-1}_{s,q}(square_m; a) <= max_{z in 3^n Z^d cap square_m}
lambda^{-1}_{s,q}(z + square_n; a)
(ABK26, reused in p.bfA.multiscalebound Step 1) is for finite q:
definition (2.23) puts a sum of per-depth maxima on the left and a maximum
of sums on the right.
Two routes are proved here, both with the exponent drop s -> t as their only
structural cost:
G(s,t,q) = [c_{sq} / c_{(s-t)q}]^{2/q} (gap route, headline)
K(s,t,q) = G(s,t,q) . c_{tq}^{-2/q} (endpoint route)
c_{aq} = 1 - 3^{-aq} = geometricDiscount a q .
The transfers #
lambdaSq_finite_inv_le_gapConst_mul_max_descendants (the sharp route): for 0 < t < s,
q >= 1 finite, n <= Q.scale,
lambda^{-1}_{s,q}(Q; a)
<= G(s,t,q) . max_{R in descendantsAtScale Q n} lambda^{-1}_{t,q}(R; a) .
Why the sharp route is sharper #
The endpoint detour prices the per-depth maxima of Q twice: once going into
lambda^{-1}_{t,infinity} and once coming out of it, and the second passage
costs c_{tq}^{-2/q} (= 7.79... at t = 1/16, q = 2). CoarseGraining's
e.bound.one.cube.by.lambdas (maxDescendant_lambdaSq_inv_le) supplies the
same geometric profile
M_i(Q) <= 3^{2ti} . max_{R in descendantsAtScale Q n} lambda^{-1}_{t,q}(R; a)
directly from the subcube gauges, with the descendant weight 3^{2t(R.scale - k)} for the deep scales and e.subadda.nosymm at the norm level for the
shallow ones, so the endpoint is never entered and only G survives.
The canonical instantiation s = 1/8, t = 1/16, q = 2 #
At q = 2 (so 2/q = 1), with u := 3^{-1/8} = 0.8716... (so
1 - u = 0.1283...):
G(1/8, 1/16, 2) = (1 - 3^{-1/4}) / (1 - 3^{-1/8}) = 1 + 3^{-1/8} = 1.871... <= 2 ,
K(1/8, 1/16, 2) = (1 - 3^{-1/4}) / (1 - 3^{-1/8})^2 = 14.58... <= 15 .
maxFormGapConst_eighth_sixteenth_two_le records the machine-checked bound on
G. K(s,t,2) is symmetric under t <-> s - t and therefore minimized at
the midpoint t = s/2, which is why t = 1/16 is canonical; G(s,t,2)
increases strictly in t (G → 1 as t → 0⁺, G → ∞ as t → s⁻, so the
sharp route gets cheaper at smaller t); t = 1/16 is therefore admissible but
not extremal for the sharp route. It is kept because the s-window and the
frozen hsWindow are checked at one fixed t.
Cube indices #
Every statement below quantifies over a cube Q with n <= Q.scale, i.e. the
subcube scale lies at or below the cube scale.
Main results #
maxFormGapConst: the explicitG.lambdaSq_finite_inv_le_gapConst_mul_of_maxDescendant_le: the summation core, from any geometric profileM_i(Q) <= 3^{2ti} D.maxDescendantSigmaStarInv_le_rpow_mul_max_descendants_lambdaSq_inv: the geometric profile supplied by the subcube gauges.lambdaSq_finite_inv_le_gapConst_mul_max_descendants: the sharp transfer.maxFormGapConst_eighth_sixteenth_two_le: the machine-checked boundG(1/8, 1/16, 2) <= 2.lambdaSq_eighth_inv_le_two_mul_max_descendants_sixteenth: the consumer-facing instancelambda^{-1}_{1/8,2}(Q) <= 2 max_R lambda^{-1}_{1/16,2}(R).
References #
- ABK26, (2.22)--(2.23),
l.bad.event.lemma, casen < m,p.bfA.multiscalebound.
The transfer constant #
The exponent-gap constant G(s,t,q) = [c_{sq} / c_{(s-t)q}]^{2/q}, the
first factor of K(s,t,q). It is the constant of the sharp route below, which
never leaves the finite-q gauge and therefore never pays the endpoint factor
c_{tq}^{-2/q}.
Equations
Instances For
Real-power and geometric-weight bookkeeping in CoarseGraining's spelling #
CoarseGraining states its multiscale definitions with explicit Real.rpow
applications, while Mathlib's rpow A is phrased with the ^ notation. The
restatements below keep every rewrite inside CoarseGraining's spelling; they
are the analogues, for the lemmas used here, of the mul_rpow' /
rpow_natCast' restatements already in InftyToQ.lean.
Real.rpow_nonneg, restated with an explicit Real.rpow application.
Real.rpow_one, restated with an explicit Real.rpow application.
The defining form of CoarseGraining's geometricWeight.
Leg one: the finite-q gauge at s against the endpoint gauge at t #
Leg one of the transfer. For 0 < t < s and 0 < q,
lambda^{-1}_{s,q}(Q; a) <= [c_{sq} / c_{(s-t)q}]^{2/q}. lambda^{-1}_{t,infinity}(Q; a).
This is (2.23) summed against the geometric density c_{(s-t)q} 3^{-(s-t)qj};
the gap s - t > 0 is exactly what makes that density summable.
The sharp route: the geometric profile from the subcube gauges #
The endpoint detour of the two legs above is not needed. CoarseGraining's
e.bound.one.cube.by.lambdas (maxDescendant_lambdaSq_inv_le) prices the
per-depth maxima of a subcube directly by that subcube's own finite-q gauge,
with the descendant weight 3^{2t . depth} — exactly the geometric profile
that the summation lemma consumes. The endpoint factor c_{tq}^{-2/q}
therefore never appears, and the constant drops from K to G.
The geometric profile of the subcube gauges. For n <= Q.scale,
t > 0 and admissible q, every per-depth maximum of Q is priced by the
scale-n subcube gauges at exponent t:
max_{depth-i descendants R' of Q} |sigma_*^{-1}(R'; a)| <= 3^{2ti}. max_{R in descendantsAtScale Q n} lambda^{-1}_{t,q}(R; a).
Deep scales (Q.scale - i <= n) are priced inside the relevant subcube by
e.bound.one.cube.by.lambdas; shallow scales by e.subadda.nosymm at the norm
level, which puts an ancestor's one-cube norm below the maximum over its
scale-n descendants.
For 0 < t < s, 1 <= q and n <= Q.scale,
lambda^{-1}_{s,q}(Q; a)
<= G(s,t,q) . max_{R in descendantsAtScale Q n} lambda^{-1}_{t,q}(R; a) ,
G(s,t,q) = [c_{sq} / c_{(s-t)q}]^{2/q} .
The only cost of the transfer is therefore the exponent drop s -> t; the
constant is G <= 2 at the canonical instantiation, so the threshold re-basing
it forces on C_{(e.cg.ellip.lower)} is a factor 2.
The canonical instantiation s = 1/8, t = 1/16, q = 2 #
3^{-1/8} is at most 7/8: equivalently (8/7)^8 = 2.91... <= 3.
The sharp constant at the canonical instantiation is at most 2. At
s = 1/8, t = 1/16, q = 2,
G = (1 - 3^{-1/4}) / (1 - 3^{-1/8}) = 1 + 3^{-1/8} = 1.871... <= 2,
and the inequality G <= 2 is in fact the identity (1 - u)^2 >= 0 at
u = 3^{-1/8}.
The transfer at the canonical instantiation s = 1/8, t = 1/16, q = 2,
with the machine-checked numerical constant of the sharp route:
lambda^{-1}_{1/8,2}(Q; a) <= 2. max_{R in descendantsAtScale Q n} lambda^{-1}_{1/16,2}(R; a).
This is the shape in which the ellipticity branch n < m of
l.bad.event.lemma (ABK26) and Step 1 of p.bfA.multiscalebound consume the
transfer. Both costs are visible: the right-hand gauge sits at t = 1/16 < 1/8, so p.cg.ellipticity.bounds must be read at 1/16, and the factor 2
re-bases the threshold constant C_{(e.cg.ellip.lower)} (module header,
disclosure). The factor is independent of d, of Q.scale - n and of the
number 3^{d(Q.scale-n)} of subcubes.