HomSpineDataBridge #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
StepTwoDataBridge PRODUCED: the correction discharged #
What this file discharges #
HomSpineTopScale.StepTwoDataBridge — the ONE data-leg input of
htop_of_stepTwoA_enlargedY — is the passage from the printed p = ∞
normalization of the manuscript,
[g]_{C^{0,1/2}(□_m)} ≤ K_g, [∇h]_{C^{0,1/2}(□_m)} ≤ K_h,
‖∇h‖_{L^∞(□_m)} ≤ K_h^∞,
to the q = 2-in-scale Besov data quantities that CoarseGraining's
coarse-graining right-hand side carries,
3^{sm}[g]_{B^s_{2,2}(□_m)} ≤ C_data · 3^{m/2} K_g,
3^{sm}‖∇h‖_{B^s_{2,2}(□_m)} ≤ C_data · (K_h^∞ + 3^{m/2} K_h).
The correction records this as a named input, together with the two findings it
verified: the passage is exponent-critical (s < 1/2 STRICTLY — at s = 1/2 the depth-j contribution 3^{m/2}3^{(s-1/2)j}[g] does not decay and the
ℓ²-in-scale sum diverges), and nothing in CoarseGraining or Mathlib proves
it.
It is proved here, from material already available in this repository. The route is the Gagliardo one, not the direct depth sum:
HomStepThreeData.memWsp_of_holderHalf— aC^{0,1/2}field on the cube lies inW^{s,2}(□_m)fors < 1/2(the radial kernel integrates near the diagonal exactly in that range);StepFourSeminormComparisons.three_rpow_mul_normalizedGagliardoESeminormOn_cube_le—3^{ms}[f]_{H^s(□_m)} ≤ K·C_{S4.4}(d,s)·3^{m/2}, whose constantC_{S4.4}(d,s) ≤ (2^{d+1}3^d/(1-2s))^{1/2}carries the correction's endpoint blow-up (here in the Gagliardo form(1-2s)^{-1/2}; the correction states it in the depth-sum form(1-3^{2s-1})^{-1/2}— the same divergence ats ↑ 1/2, from the same geometric series);ExcessDecay.scaleNormalizedPositiveBesovVectorSeminormTwo_le_gagliardo— theH^s → B^s_{2,2}bridge atbesovGagliardoConstant d;HomStepThreeData.sqrt_vecNormSq_cubeAverageVec_le— the MEAN term of the∇hNORM, priced by the root's ownK_h^∞binder at√d(a Hölder seminorm alone cannot price it; the root already carries the sup datum).
No hypothesis is added #
stepTwoDataBridge_of_holder takes exactly the frozen root's own data binders
(generator_renormalization, the Kg/Kh/KhInf block) plus the standing
0 < t, and the correction's own strict t < 1/2. There is no new
mathematical proposition in any binder.
The constant #
stepTwoDataConst d t = max ( √d, C_besov(d) · C_{S4.4}(d,t) )
— the √d prices the mean term (the ambient sup-versus-Euclidean conversion,
the standing convention) and the product prices both seminorm legs.
stepTwoDataConstPinned d is its t ≤ 1/4 specialization at the γ-free
homDataConst d.
1. The Gagliardo data embedding at the FULL corrected range s < 1/2 #
HomStepThreeData states the embedding at the gate s ≤ 1/4, where the
s-dependence of the constant is absorbed into the γ-free homDataConst d.
The correction asks for the whole open range, with the endpoint blow-up
displayed. These are the same proofs at stepFourGagliardoConst d s.
The data embedding in toReal form, at 0 < s < 1/2:
3^{ms}[f]_{H^s(□_m)} ≤ K · C_{S4.4}(d,s) · 3^{m/2}, with the correction's
endpoint factor kept visible inside C_{S4.4}(d,s).
B_g ≤ C 3^{m/2} K at 0 < s < 1/2. The q = 2-in-scale Besov data
leg of the coarse-graining right-hand side, priced by the printed Hölder normalization on the whole
range the correction names.
The ∇h NORM leg at 0 < s < 1/2. HomStepThreeData's M3 display
on the whole corrected range: the mean half priced by the root's sup binder at
√d, the seminorm half by the embedding.
2. The bridge constant #
The constant of the correction in this repository's carriers:
max(√d, C_besov(d)·C_{S4.4}(d,t)). The first entry prices the MEAN term of
the ∇h norm against the root's K_h^∞ binder, the second prices both
seminorm legs; the endpoint blow-up as t ↑ 1/2 sits in
stepFourGagliardoConst.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pinned form of the bridge constant (t ≤ 1/4, γ-free).
Equations
- One or more equations did not get rendered due to their size.
Instances For
3. The bridge is monotone in its constant #
Enlarging C_data weakens the bridge: the two right-hand sides are
nonnegative multiples of C_data.
4. The bridge, proved #
The Hölder-embedding correction, discharged.
HomSpineTopScale.StepTwoDataBridge at the constant stepTwoDataConst d t,
from exactly the frozen root's own data binders:
[g]_{C^{0,1/2}(□_m)} ≤ K_g, [∇h]_{C^{0,1/2}(□_m)} ≤ K_h,
‖∇h‖_{L^∞(□_m)} ≤ K_h^∞, 0 < t < 1/2.
The g leg is the embedding applied to -g (the forcing sign,
holderSeminormBoundOn_neg, at constant 1); the ∇h leg is the NORM, whose
mean half is the root's K_h^∞ binder at √d and whose seminorm half is the
embedding again. t < 1/2 is STRICT and load-bearing: it is what makes the
Gagliardo kernel of a C^{0,1/2} field integrable at the diagonal, i.e. the
correction's ℓ²-in-scale convergence.
The pinned corollary: at 0 < t ≤ 1/4 the bridge runs at the
γ-free constant stepTwoDataConstPinned d.