OscillationNestedAssembly #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The nested-recentring assembly #
This module runs the nested recentring end to end on the concentric triadic
family U_j = z + cu_{n+j}, 0 <= j <= N, and produces the abstract form of
the display e.nablaw.oscillations.
The mechanism #
At every scale j <= N the corrector w is replaced by a harmonic function
h_j = w - phi_j, where phi_j in H^1_0(U_j) is the potential of the forcing
recentred on U_j (OscillationNestedTransport). The defect obeys the
birth-scale bound || grad phi_j ||_{L2bar (U_j)} <= sqrt d * M * 3^{n+j}. On the
fine cube U_0 the gradient of w is then written as the finite sum
grad w = grad h_N + sum_{j < N} (grad h_j - grad h_{j+1}) + grad phi_0 ,
and each summand is estimated on U_0 directly from its own birth scale.
The two declared divergences #
- The gap restriction
d + 3. The arbitrary-gap harmonic decay (HarmonicReplaceGradient) is available only for gapsk >= d + 3. The coarse term therefore needsN >= d + 3, which is imposed as a hypothesis. - The small-gap branch. Increments born at a scale
j < d + 3cannot use the decay. They are dispatched instead by the volume-ratio comparison ofOscillationNestedFamily, at the cost of the dimensional constant(3 rho)^{d+2}withrho = sqrt (3^d). This branch is a single comparison between two cubes, not a recurrence, so it does not reintroduce the false step.
Both are visible in the constant, which is written as an explicit sum of the
decay contribution C(d) rho and the small-gap contribution (3 rho)^{d+2}.
Contents #
exists_replacement_family-- the per-scale harmonic replacements, chosen simultaneously at all scales.exists_h1Function_increment-- the harmonic incrementh_j - h_{j+1}as anH^1function on the finer cube, weakly harmonic there, with the explicit gradientgrad phi_{j+1} - grad phi_j.exists_gradient_oscillation_nested_telescope-- the abstract display.
Portability #
This file depends only on Mathlib, on CoarseGraining
(Homogenization.*) and on the harmonic/oscillation layer of this same
directory. It mentions no object of the manuscript: no model, no cutoff, no
shell, no corrector, no sigmaBar. The forcing G is an abstract Lipschitz
vector field; the manuscript's sigmaBar^{-1} grad (k_m - k_{m-h}) is one
instance of it, produced elsewhere. It is intended to be portable into
CoarseGraining by a single mechanical namespace rename.
References #
- ABK26,
e.nablaw.oscillations(the ball one-step estimate and the word "iterating").
The per-scale harmonic replacement family.
From the single weak equation on the coarse cube z + cu_{n+N} one obtains, at
every scale j <= N simultaneously, an H^1_0(z + cu_{n+j}) potential phi_j
whose subtraction makes w weakly harmonic on z + cu_{n+j} and whose gradient
has normalized L^2 size at most sqrt d * M * 3^{n+j} there.
The harmonic increment born at scale j.
For j < N the difference h_j - h_{j+1} of the two harmonic replacements built
at consecutive scales is an H^1 function on the finer cube z + cu_{n+j}, is
weakly harmonic there, and its weak gradient is
grad phi_{j+1} - grad phi_j: the corrector's own gradient cancels.
The nested-recentring display.
Let w be an H^1 function on the coarse concentric cube z + cu_{n+N} which
weakly solves - Delta w = div G there against H^1_0 competitors, and suppose
the differentials of the coordinates of the forcing G are bounded by M on
that cube. If the number of scales satisfies N >= d + 3, then
|| grad w - (grad w)_{z+cu_n} ||_{L2bar (z+cu_n)}
<= C(d) 3^{-N} || grad w - (grad w)_{z+cu_{n+N}} ||_{L2bar (z+cu_{n+N})}
+ C(d) N 3^n M ,
with a constant depending only on the dimension. This is the shape of the
manuscript's e.nablaw.oscillations with N = m - h - n and
M = sigmaBar^{-1} || grad (k_m - k_{m-h}) ||_{L^infty}: the full geometric gain
3^{-(m-h-n)} on the coarse term, and a forcing term linear in m - h - n
carrying the single factor 3^n. The coarse term appears here in the sharper
oscillation form; the printed norm form follows by mean recentring.
The proof never forms an adjacent-scale cube recurrence: increments born at
scale j >= d + 3 are hit once by the arbitrary-gap harmonic decay from their
birth scale directly to the fine cube, and the finitely many increments born at
j < d + 3 are dispatched by a single volume-ratio comparison. See.
The nested-recentring display in the printed norm form.
The same estimate with the coarse term written as the normalized L^2 norm of
grad w on the coarse cube, which is literally the right-hand side of
e.nablaw.oscillations:
|| grad w - (grad w)_{z+cu_n} ||_{L2bar (z+cu_n)}
<= C(d) 3^{-N} || grad w ||_{L2bar (z+cu_{n+N})} + C(d) N 3^n M .
It follows from the oscillation form by mean recentring, the oscillation being the deviation from the average and the norm the deviation from the origin.