StepFourSeminormComparisons #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
t.regularity Step 4: the two seminorm comparisons #
The target #
[g]_{H^{1/4}(U_j)} ≤ C · 3^{j/4} · [g]_{W^{1/2,∞}(□_m)} (A1)
[∇h]_{W^{1/2,∞}(U_j)} ≤ [∇h]_{W^{1/2,∞}(□_m)} (A2)
on the Step-3 window family U_j = (z + □_j) ∩ □_m.
What is delivered #
(A1) normalizedGagliardoESeminormOn_stepThreeWindow_le, at a general index 0 < s < 1/2 with the honest closed-form constant and the honest scale weight,
[g]_{H^s(U_j)} ≤ K · C_{S4.4}(d,s) · 3^{j(1/2-s)} ,
C_{S4.4}(d,s) = ( 2^d 3^{d+2s-1} / (1 - 3^{-(1-2s)}) )^{1/2}
≤ 2^{(d+1)/2} 3^{d/2} (1-2s)^{-1/2} ,
Specialized at the §4.4/§4.5 pin s = 1/4 the exponents are the numerals 3^{j(1/2-1/4)} = 3^{j/4} and (1-2s)^{-1/2} = 2^{1/2}, giving exactly the printed C·3^{j/4} with C ≤ (2^{d+2} 3^d)^{1/2} (normalizedGagliardoESeminormOn_stepThreeWindow_quarter_le, the
constant read off the range guard at 1 - 2s = 1/2).
3^{sm} [g]_{H^s(□_m)} ≤ K · C_{S4.4}(d,s) · 3^{m/2}
(three_rpow_mul_normalizedGagliardoESeminormOn_cube_le). This is the missing line
between the Step-7d display's 3^{sm}[g]_{H^s(□_m)} and e.energy.density.estimate's
3^{m/2}[g]_{W^{1/2,∞}(□_m)}; note the free s cancels out of the scale weight, which
is why the theorem's conclusion can be s-free.
(A2) The p = ∞ comparison is the ⨍∫-normalized Gagliardo seminorm at
p = ∞. Its volume normalization is inert, an essential supremum not seeing a
positive scalar multiple of the measure, so no |U_j|/|□_m| ratio would enter (A2)
in either reading — unlike the p = 2 seminorm of (A1), where the ratio would enter
and is instead avoided by the uniform-in-first-slot argument of
HolderGagliardoEmbedding.
The range guard #
At the §4.4 pin s = 1/4 the guard is met with room.
References #
- ABK26,
t.regularityStep 4; Step 7d. - ABK26, (the seminorm conventions).
1. The window has sup-diameter at most 3^j #
Every point of U_j = (z + □_j) ∩ □_m sees the whole window inside the
sup-ball of radius 3^j: the window sits in a cube of side 3^j.
2. The scale weight 3^{j(1/2-s)} #
3. Atom (A1): the g-restriction comparison #
[g]_{H^s(U_j)} ≤ K · C_{S4.4}(d,s) · 3^{j(1/2-s)},
where K is any C^{0,1/2}(□_m) bound for g — the development's carrier of
the printed [g]_{W^{1/2,∞}(□_m)} slot. The scale weight is exactly the
window's diameter 3^j to the power 1/2 - s; no volume ratio appears.
The s = 1/4 pin: the printed C·3^{j/4}, with the constant carried
symbolically as stepFourGagliardoConst d (1/4), which stepFourGagliardoConst_le
bounds by (2^{d+2} 3^d)^{1/2}.
3b. The same atom on the full cube: the Step-7d passage #
The g-comparison on the full cube: [g]_{H^s(□_m)} ≤ K C(d,s) 3^{m(1/2-s)}.