GammaTenStripEnergy #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The energy leg of hstrip: the exact tiling fold of the cell second moments #
ABK26, Step 2 of l.approximate.recurrence.formula, e.nablaw.in.L.eight.
What this module is #
Closure.GammaTenStripBound.gammaTenStrip_cell_average_sq_le leaves exactly two
grid binders: the mesh averages of the sample second moments of the two cell
data D_R, F_R of the crude elliptic majorant. This module folds those two
averages onto the localization cube by the exact mesh tiling identity
LocalizationGrid.cubeAverage_originCube_eq_mesoGridAverage, whose constant is
1 and which loses nothing at boundary cells:
avsum_{R in 3^n Zd cap cu_K} ( fint_R |u|^2 )^2
<= avsum_R fint_R |u|^4 = fint_{cu_K} |u|^4 = originCubeFourthEnergy K u .
The first step is the per-cell Jensen inequality of CoarseGraining
(sq_cubeAverage_le_cubeAverage_sq_of_memLp); the second is the tiling
identity; the third is the definition of the annealed fourth energy of
LocalizationEnvelopeMesh. Its consumer Closure.GammaTenStripRemainder
composes the fold with
LocalizationFluctuationGridEighth.cubeFamilyAverage_integral_le_of_pointwise
in the sample, which reduces the two grid binders to one expectation per
leg,
E[ fint_{cu_K} | e' + grad w_D |^4 ] and E[ fint_{cu_K} | e + F |^4 ] ,
which is the shape e.nablaw.in.L.eight controls through
LocalizationEnvelopeSpatial.originCubeFourthEnergy_le_sq_of_cubeEuclideanLpNorm_sq_le
and LocalizationEnvelopeMoment's Gamma_1 second moment.
The load legs cost nothing #
Both cell data are energy + |load|^2 with the load the cell average of the
same field, so the vector Jensen inequality
(vecNormSq_const_add_cubeAverageVec_le, the constant-shifted form proved here)
gives |load|^2 <= energy at every cell and hence D_R <= 2 Epot_R,
F_R <= 2 Eflux_R. No separate load moment is needed: the P_z legs are
absorbed by a factor 4 in the constant.
What is proved #
cubeAverageVec_const,vecNormSq_const_add_cubeAverageVec_le--- the constant-shifted vector Jensen step at one cube.cubeFamilyAverage_sq_cubeAverage_vecNormSq_le_originCubeFourthEnergy--- the pathwise fold: Jensen and the exact tiling identity, constant1.stripCellPotentialDatum_le_two_mul_energy,stripCellFluxDatum_le_two_mul_energy--- the two cell data against twice their own cell energies.
A pair of grid statements assembling these into the two binders of
Closure.GammaTenStripBound.gammaTenStrip_cell_average_sq_le directly from an
annealed fourth energy per leg once stood here too. Their callers moved to the
pathwise-majorant form Closure.GammaTenStripRemainder states
(..._le_of_majorant), they lost every consumer, and they were removed; git
history keeps them.
Binders #
Beyond the typing binders: the mesh scale gate hn (which only names the mesh);
the per-sample spatial L^8 membership of the leg field on the localization
cube; and the per-cell L^2 membership used by the two cell-datum comparisons.
No smallness gate, no induction state, no measurable selection and no
interior-mesh restriction occurs.
Scope #
Internal Provider infrastructure for the Step-2 fluctuation estimate. There is
no sorry, no admit, no custom axiom and no set_option maxHeartbeats.
References #
- ABK26,
l.approximate.recurrence.formulaStep 2,e.Pz.def,e.Fz.def,e.nablaw.in.L.eight.
Membership bookkeeping #
|u|^2 is square-integrable on a cube whose L^8 membership is known.
The constant-shifted vector Jensen step #
The cube average of a constant vector field is that constant.
Jensen with a constant shift. |c + (g)_R|^2 <= fint_R |c + g|^2.
only on the L^2 membership of g on the cube.
The pathwise fold #
The exact mesh fold of the squared cell energies.
avsum_{R in 3^n Zd cap cu_K} ( fint_R |u|^2 )^2 <= fint_{cu_K} |u|^4 .
Per cell this is Jensen; over the mesh it is the tiling identity, whose constant
is 1. Boundary cells are included: nothing in the statement distinguishes
them.
on the scale gate hn, which only names the mesh, and on the spatial L^8
membership hu on the localization cube.
The two cell energies as cube averages #
The potential cell energy is shom^{-1} times the cube average of
|e' + grad w_D|^2. Unconditional.
The flux cell energy is shom times the cube average of |e + F|^2.
Unconditional.
The load legs are below their own cell energies #
The potential load leg is below the potential cell energy. This is the
constant-shifted Jensen inequality at the cell, read through the two closed
forms; the gauge shom^{-1} is common to both sides.
only on the cell L^2 membership of the corrector gradient.
The flux load leg is below the flux cell energy.
only on the cell L^2 membership of the flux leg field.
The potential cell datum is below twice the potential cell energy.
The flux cell datum is below twice the flux cell energy.