StepSevenEndEmbedding #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
t.regularity Step 7d, part two: the oscillation endpoint #
The target #
3^{-(m'-1)}‖u - (u)_{(z+□_{m'-1})∩□_m}‖_{L²((z+□_{m'-1})∩□_m)} 1_{𝒢(m',z;·,·)}
≤ C 3^{-(m'-1)}‖u - (u)_{z'+□_{m'-1}}‖_{L²(z'+□_{m'-1})} 1_{𝒢} (S44-G)
≤ C σ_m^{-1/2} 3^{(1/2)(d+γ)(m-m')}
( ν^{1/2}‖∇u‖_{L²(□_m)} + σ_m^{-1/2} 3^{sm}[𝐠]_{H^s(□_m)} ) .
Step one: the window replacement #
The manuscript replaces the truncated window (z+□_{m'-1}) ∩ □_m by the
off-grid cube z'+□_{m'-1} "at the cost of a constant C". The inclusion
is the Step-7a sandwich (StepSevenSelectionData.upper_sandwich_in); the
comparison of the two mean-subtracted L² norms is asserted. It is proved
here from two proved facts and one proved geometric input:
normalizedL2On_sub_volumeAverage_le— the mean minimizes theL²(S)deviation, so(u)_Smay be replaced by(u)_Tfor free;normalizedL2On_le_of_subset— nested windows compare at the square root of the volume ratio;image_add_wellPlacedCentre_subset_truncatedWindow— the inscribed cube□_{k-1}inside(z+□_k)∩□_m, which bounds the ratio by3^d.
The produced constant is therefore the explicit 3^{d/2}, a C(d) exactly as
printed. (The sharp constant is 2^{d/2}; the inscribed-cube route gives
3^{d/2}, and the difference is inside C.)
Step two: the embedding, and the summability bridge #
The manuscript's second inequality is e.fractional.Sobolev.embedding composed
with e.cg.Poincare.with.rhs.grad.applied. Two independent conditional
inputs, both named for what they are:
hembedstays a named input here, with its producer identified. The two sides sit at different summability indices:l.coarse.graining.RHSproduces theq = 2object. CoarseGraining's provedcoarsePoincareRHSTheory(Homogenization/Book/Ch03/Theorems/CoarsePoincare.lean) concludes withscaleNormalizedNegativeBesovVectorNorm Q s (.finite 2) …, i.e.B^{-s}_{2,2}, at ONE exponentswith0 < s < 1strictly.e.fractional.Sobolev.embeddingconsumes theq = 1object: the tex prints[∇u]_{B^{-s}_{p,1}}(macro\besov{-s}{p}{1}) and the proved local theorem above is atq = 1.- CoarseGraining has NO change-of-summability lemma on any negative Besov carrier in either direction (exhaustive sweep), and NO formalization of the embedding.
- The manuscript's own conversion is
[·]_{B^{-1}_{2,1}} ≤ C(t)[·]_{B^{-t}_{2,2}}with the geometric factor(Σ_{n≤0} 3^{2(1-t)n})^{1/2}, which needst < 1strictly and diverges ast ↑ 1. The hypothesis in hand is at index exactly-1, so the printed chain cannot be run as written. CoarseGraining's own proved constant(1 - 3^{-2(1/2-t)})^{-1/2}degenerating at the same endpoint is the independent Lean-side confirmation. Sohbridgeis a genuine external obligation, not a formalization artifact: as printed, the Step-7d chain is index-broken.
The scalar carriers #
oscTrunc—3^{-(m'-1)}‖u - (u)_{(z+□_{m'-1})∩□_m}‖_{L²((z+□_{m'-1})∩□_m)}·1_𝒢; this is theoscHileg, the quantitye.gradient.with.shomtransports.oscLoc— the same weight onz'+□_{m'-1}.besovP1/besov—3^{-m'}‖∇u‖inB^{-1}_{2,1}and inB^{-1}_{2,2}.shomMinv,gradM,dataM— as inStepSevenEndPoincare.
References #
- ABK26, Step 7d;
e.fractional.Sobolev.embedding; the summability conversion.
1. The mean comparison across nested windows #
The mean comparison on nested windows. For S ⊆ T,
‖u - (u)_S‖_{L²(S)} ≤ (|T|/|S|)^{1/2} ‖u - (u)_T‖_{L²(T)} .
The mean on S is replaced by the mean on T for free (the mean minimizes the
deviation), and the nested windows then compare at the square root of the
volume ratio. This is the inequality the manuscript asserts.
2. The volume ratio of the Step-7a sandwich pair #
The sandwich pair's volume ratio. For z ∈ □_m and k ≤ m, every
translate of □_k has volume at most 3^d times that of the truncated window
(z+□_k) ∩ □_m — the inscribed cube □_{k-1} of
image_add_wellPlacedCentre_subset_truncatedWindow supplies the lower bound.
3. The mean comparison at the Step-7a sandwich #
The Step-7d mean comparison, at the sandwich pair, with the constant made explicit:
‖u - (u)_{(z+□_k)∩□_m}‖_{L²((z+□_k)∩□_m)}
≤ 3^{d/2} ‖u - (u)_{z'+□_k}‖_{L²(z'+□_k)} .
hST is StepSevenSelectionData.upper_sandwich_in at k = m'-1. The
3^{d/2} is the inscribed-cube constant; the sharp value is 2^{d/2} and the
difference is inside C(d).
4. The oscillation endpoint on scalars #
The Step-7d oscillation endpoint, on abstract reals.
The four links of the manuscript's chain:
oscTrunc ≤ Cmean·oscLoc (proved above)
oscLoc ≤ Cemb ·besovP1 (hembed — e.fractional.Sobolev.embedding, mean-zero)
besovP1 ≤ Cbr ·besov (hbridge — the summability change)
besov ≤ Cout ·Ktr·(√σ_m^{-1}·gradM + σ_m^{-1}·dataM) (StepSevenEndPoincare)
composed, and the bracket rewritten into the printed
σ_m^{-1/2}(ν^{1/2}‖∇u‖_{L²(□_m)} + σ_m^{-1/2}3^{sm}[𝐠]_{H^s(□_m)}).