OscillationAssemblyShell #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
e.nablaw.oscillations at the fresh-shell correctors #
ABK26 claims, for every mesh point z with z + cu_{m-h} ⊂ cu_K,
‖ ∇w_{D,e}^{(K)} - (∇w_{D,e}^{(K)})_{z+cu_n} ‖_{L2bar(z+cu_n)}
≤ C 3^{-(m-h-n)} ‖ ∇w_{D,e}^{(K)} ‖_{L2bar(z+cu_{m-h})}
+ C shom_{m-h}^{-1} (m-h-n) 3^n ‖ ∇(k_m - k_{m-h}) ‖_{L∞(z+cu_{m-h})} ,
and adds "the same results are valid for w_{N,e'}^{(K)}".
This module instantiates the abstract nested-recentring display of
OscillationNestedAssembly at exactly those carriers: w is the actual
finite-volume corrector of e.def.w on cu_K (Dirichlet or Neumann), the
forcing is the actual fresh-shell forcing streamForcing, and the concentric
family is the interior mesh cube z + cu_{n+N} with N = m - h - n.
The three ingredients #
- The abstract display,
exists_gradient_oscillation_nested_telescope_norm. - Coordinatewise differentiability and the differential bound of the forcing,
StreamForcingDeriv. - The passage of the weak equation from
cu_Kto the interior mesh cube,forall_h10Function_integral_vecDot_grad_eq_of_subset(OscillationNestedTransport), which is CoarseGraining's restriction of solenoidality along the extension by zero.
The Neumann leg #
The Neumann corrector's natural boundary condition enlarges its test class from
H^1_0(cu_K) to the mean-zero gauge of H^1(cu_K), and the mean-zero
representative of an H^1_0 competitor has the same gradient
(H1Function.toMeanZero_grad). So the Neumann weak equation implies the
H^1_0-tested equation on cu_K, and from there the interior transport and the
telescope are word for word the Dirichlet ones. Both legs are therefore
produced below, from one shared core.
Contents #
exists_freshShellDirichlet_gradient_oscillation_interior_meshandexists_freshShellNeumann_gradient_oscillation_interior_mesh-- the display at the two correctors, with the forcing amplitude quantified over majorants of the exact induced shell-derivative gauge.exists_freshShellDirichlet_gradient_oscillation_interior_mesh_localGaugeand its Neumann counterpart -- the same, with the amplitude written as the summed first-derivative gauges∑_{k ∈ (m-h,m]} ‖∇j_k‖_{L∞(z+cu_{m-h})}, which is the carrier ofe.nabla.km.kn.inftyat base pointz(Provider.Stream.isBigOWith_gammaSigma_shellDerivNormSum_Ioc_translate).
All four statements quantify over the corrector families rather than producing
them: wD and wN enter as arbitrary families of weak solutions of e.def.w,
and their existence is the business of FreshShellExistence.
Divergences from the printed statement #
- . The statement is the interior one: it is quantified over base points
zsubject toz + cu_{n+N} ⊆ cu_K, exactly the restriction printed. - The lattice hypothesis is dropped. The manuscript restricts to
z ∈ 3^n Z^d ∩ cu_K; the proof uses no lattice property, so the realization below quantifies over all base points with the containment, which is strictly stronger. - The gap restriction
d + 3. The telescope's coarse term uses the arbitrary-gap harmonic decay, available only for gaps≥ d + 3, so the number of scalesN = m - h - nmust satisfyd + 3 ≤ N. This is inherited fromOscillationNestedAssemblyand is carried as an explicit hypothesis. - The forcing amplitude is quantified over majorants. The printed
right-hand side contains
‖∇(k_m - k_{m-h})‖_{L∞(z+cu_{m-h})}. Here the statement is universally quantified over real numbersKgraddominating that exact induced gauge pointwise onz + cu_{m-h}; since the supremum is itself such a number, this form implies the printed one and is stronger. - The gauge reading of the forcing term is the lossless one. The summed
first-derivative gauges
∑_{k ∈ (n',m]} ‖∇j_k‖_{L∞(z+cu_ell)}dominate‖∇(k_m - k_{n'})‖_{L∞(z+cu_ell)}by the triangle inequality with no loss; that is the_localGaugeform, and it is the carrier ofe.nabla.km.kn.infty. Reading the amplitude off the summand ofe.W.1.inf.boundinstead would cost the factor3^{-(n'+1)}applied to the whole sum, because that summand carries the increasing weight3^k, hence a loss of at most3^{m-n'-1}in general and of3^{gamma(m-n')}once the shell gauges are inserted at their own amplitudes. In the parameter regime ofe.recurrence.paramsthat residue is3^{gamma h}withgamma h ≤ 6 cstar, i.e. bounded, but it is not dimension-only, so only the lossless reading is delivered here. - The visible
sqrt d. The ambient carrierVec dis sup-normed while the shell-derivative gauge is Euclidean, so the amplitude readssigmaInv * sqrt d * |e|_2 * Kgrad. The factor is written out, not absorbed; the manuscript'sCis dimension-only and absorbs it.
References #
- ABK26,
e.nablaw.oscillations. - ABK26,
e.def.w. - ABK26,
e.W.1.inf.bound.
One elementary fact #
The shared core #
The Dirichlet leg #
e.nablaw.oscillations for the Dirichlet corrector of e.def.w.
For the actual zero-trace solution w_{D,e}^{(K)} of e.def.w on cu_K, on
every interior mesh cube z + cu_{n+N} with z + cu_{n+N} ⊆ cu_K and
N ≥ d + 3,
‖ ∇w_D - (∇w_D)_{z+cu_n} ‖_{L2bar(z+cu_n)}
≤ C 3^{-N} ‖ ∇w_D ‖_{L2bar(z+cu_{n+N})}
+ C N 3^n (sigmaInv sqrt d |e|_2 Kgrad) ,
with N = m - h - n, sigmaInv = shom_{m-h}^{-1} and Kgrad any pointwise
majorant of ‖∇(k_m - k_{m-h})‖ on z + cu_{n+N} in the exact induced
shell-derivative gauge.
The Neumann leg #
e.nablaw.oscillations for the Neumann corrector of e.def.w.
The manuscript's "the same results are valid for w_{N,e'}^{(K)}". The natural
boundary condition of the Neumann problem enlarges the test class from
H^1_0(cu_K) to the mean-zero gauge of H^1(cu_K), and mean subtraction does
not change a gradient, so the Neumann weak equation implies the H^1_0-tested
equation, and the interior transport and telescope are unchanged.
The forcing term in the gauges of e.W.1.inf.bound #
The Dirichlet display with the forcing term in the summed first-derivative shell gauges.
Same statement as
exists_freshShellDirichlet_gradient_oscillation_interior_mesh, with the
majorant Kgrad taken to be ∑_{k ∈ (lowScale, highScale]} ‖∇j_k‖_{L∞(z+cu_ell)}
at ell = n + N. This is the sharp reading: the triangle inequality over the
shells loses nothing, and the random variable on the right is literally the one
bounded by Provider.Stream.isBigOWith_gammaSigma_shellDerivNormSum_Ioc_translate
(ABK26's e.nabla.km.kn.infty) when lowScale = n + N.
The Neumann display with the forcing term in the summed first-derivative shell gauges. The Neumann counterpart of the previous statement.