Step5DefectGauge #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The Step-5 cross defect at the cube's own base point, and the re-sited gauge #
ABK26, e.nablaw.oscillations and e.lower.bound.oscillations, read inside
Step 5 of l.approximate.recurrence.formula.
Closure.StepProducers recorded an obstruction on the Step-5 binder hdefect:
the proved display sited the forcing gauge of e.nablaw.oscillations at
one window z0, whereas the per-cube geometric step needs the gauge on a
window containing the cube. This module carries out the re-siting.
What is proved #
step5CrossDefect_le_meshOscillationCell--- the manuscript's per-cube step, proved: for a cubeRof scale at mostn,
withstep5CrossDefect R omega n m e u <= (d^2 sqrt d / 2) * ( ||u - (u)_R||_{L2bar(R)} * 3^{R.scale} ||grad(k_m - k_n)||_{Linf(z_R + cu_n)} ) ,z_R = triadicCubeShift Rthe cube's own base point. The two steps are the manuscript's: the mean value inequality onR(through the provedProvider.Stream.abs_entry_sum_sub_origin_le, applied to the translated shell sequence) and Cauchy--Schwarz onR. The constantstep5CrossDefectConst d = d^2 sqrt d / 2is dimensional and absolute:d^2is the entrywise-l1comparison of the Euclidean operator norm,sqrt d / 2is the circumradius of the unit cube.meshOscillationCell_eq_sqrt_cubeAverage--- at its own scale the oscillation cell ofe.nablaw.oscillationsis the root cube average of the squared fluctuation, which is what Cauchy--Schwarz produces.gridFourthMomentRoot_shellDerivNormSum_le_of_base_point--- the grid is finite and the fourth-moment bound ofLocalizationOscillationTailis uniform in the base point, so the per-cube-sited grid gauge root is dominated by the single-window root at a maximizing cube.exists_gamma0_freshShellDirichlet_step5MeshOscillationResited_le_gamma_pow_fifteen--- consequentlye.lower.bound.oscillationsholds in the re-sited shape, i.e. literally thehoscbinder ofClosure.JunctionDischargeStepFiveDisplay.step5GaugeEndpoint_of_correctors_gaugeat the gauge familyfun R omega => 3^nmesh * shellDerivNormSum n (n+h) (triadicCubeShift R) omega. Nothing is weakened: the proved full-mesh producer is re-instantiated, not re-proved, and its own binders are carried verbatim.
References #
- ABK26,
e.nablaw.oscillations;e.lower.bound.oscillations; Step 5.
L^1 <= L^2 on the normalized cube #
Cauchy--Schwarz against the constant 1: on a probability space the mean of
a nonnegative L^2 function is at most the root of its second moment.
Transfer between the normalized cube measure and Lebesgue #
The oscillation cell as a root cube average #
The oscillation cell of e.nablaw.oscillations at the cube's own scale.
It is the root cube average of the squared fluctuation, which is exactly the
quantity Cauchy--Schwarz on the cube produces.
The mean value step, at the cube's own base point #
The entrywise mean value inequality. On its own cube the fresh shell deviates from its value at the cube's base point by at most the cube's circumradius times the shell-derivative gauge at that base point.
The operator-norm form of the mean value step.
The entries of a finite shell increment are continuous.
The per-cube cross defect #
The dimensional constant of the per-cube step: the entrywise-l1 comparison of
the Euclidean operator norm (d^2) times the circumradius of the unit cube
(sqrt d / 2).
Equations
Instances For
The per-cube step of e.nablaw.oscillations, proved.
The Step-5 cross defect on a cube R of scale at most n is at most the
absolute dimensional constant times the oscillation cell of grad w on R
times the cube's side length times the shell-derivative gauge on the window
triadicCubeShift R + cu_n --- the window based at R's own site.
The proof is the manuscript's: the defect equals
fint_R e . (h(x) - h(z_R)) (u(x) - (u)_R) (the two cross terms cancel against
the averages), the mean value inequality bounds ||h - h(z_R)||_{Linf(R)}, and
Cauchy--Schwarz on R turns fint_R |u - (u)_R| into the oscillation cell.
only on hsc (the cube is at most the gauge scale), on the direction bound
he and on the L^2 membership of u on the cube, which is the very object
the display is about.
The re-sited forcing gauge on the grid #
The bound of
LocalizationOscillationTail.integral_shellDerivNormSum_rpow_four_le is
uniform in the base point, and the grid is finite; so the average of the
per-cube fourth moments is at most the largest one, which is realized at a
maximizing cube. The proved full-mesh producer is quantified over the base
point, hence applies at that cube and delivers the re-sited display with no
loss.
The per-cube-sited grid gauge root is realized at one base point. The grid being finite, the grid fourth-moment root of the base-point-sited forcing gauge is at most its single-window root at a maximizing cube.
e.lower.bound.oscillations in the re-sited hosc shape.
This is literally the hosc binder of
Closure.JunctionDischargeStepFiveDisplay.step5GaugeEndpoint_of_correctors_gauge
at the gauge family
fun R omega => 3^nmesh * shellDerivNormSum n (n+h) (triadicCubeShift R) omega,
i.e. with the forcing gauge of e.nablaw.oscillations read at each cube's own
base point, which is what the per-cube step
step5CrossDefect_le_meshOscillationCell produces.
The proved full-mesh producer is re-instantiated, not re-proved: its base point is universally quantified and its bound is uniform in that point, so the maximizing cube of the finite grid supplies the transfer. Every binder is that producer's own.
Inherited unchanged from
ApproximateRecurrence.exists_gamma0_freshShellDirichlet_step5MeshOscillation_le_gamma_pow_fifteen.