CubeJensenVec #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Binder descriptions below are an informal inventory only, NOT a source certification; certification vocabulary is reserved for frozen source-facing declarations.
Portable: the vector cube-average Jensen inequality at the fourth power #
This file contains generic mathematics only. Apart from the sibling
portable module CubeJensen -- itself a Mathlib + Homogenization.* file, and
a candidate for relocation into CoarseGraining -- it imports nothing but
Mathlib and Homogenization.*, mentions no ABK26 object, no model, no cutoff
law, no scale and no anchor.
What is here #
Two facts are needed whenever a volume-normalized L^4 quantity built from the
averaged value of a vector field on a cube has to be compared with the
volume-normalized L^8 norm of the field itself:
sq_vecNormSq_cubeAverageVec_le_cubeAverage_sq_of_memLp-- the vector Jensen inequality at the fourth power,|u_Q|^4 <= avg |u|^4, where|.|is the Euclidean lengthvecNormSq^{1/2}onVec dandu_Q = cubeAverageVec Q u;cubeAverage_norm_pow_four_le_cubeLpNorm_eight_pow_four_of_memLp-- the volume-normalizedL^4 <= L^8bridge,avg ‖g‖^4 <= (‖g‖_{L^8(Q)})^4, for a field valued in an arbitrary normed group, and its Euclidean specializationcubeAverage_vecNormSq_sq_le_cubeLpNorm_eight_vecNorm_pow_four_of_memLp.
Why the vector Jensen is not the coordinate one #
CoarseGraining proves the p = 2 vector statement in sum form,
vecNormSq_cubeAverageVec_le_sum_cubeAverage_sq_of_memLp:
|u_Q|^2 <= sum_i avg (u_i)^2 .
Consumers that then need a fourth power must either pay a dimensional factor
d (Cauchy-Schwarz on the d-term sum, the route the proved
ellipticityBudget_le takes) or collapse the sum back into a single cube
average. The second route is taken here, because the display it feeds --
ABK26's fourth-moment display -- is a numerical bound by a dimension-only
constant, and paying an avoidable factor d inside a bound whose right-hand
side is a fourth root would make the resulting constant d^{1/4}-inflected
for no reason. The collapse is exact, not an estimate: it is the finite
additivity of the cube average, cubeAverage_finset_sum_of_integrable, which
CoarseGraining has only in the two-term form cubeAverage_add_of_integrableOn
and which is supplied here by rewriting both sides as integrals against the
normalized cube measure.
With the sum collapsed, |u_Q|^2 <= avg |u|^2 is a genuine scalar cube average
on the right, and the scalar p = 2 Jensen inequality of CoarseGraining
applies to it a second time, giving |u_Q|^4 <= (avg |u|^2)^2 <= avg |u|^4.
Main results #
Finite additivity of the normalized cube average #
Finite additivity of the cube average. CoarseGraining supplies the
two-term form cubeAverage_add_of_integrableOn; this is the Finset form,
obtained by reading both sides as integrals against the (finite) normalized
cube measure.
Membership bookkeeping #
The cube average of the Euclidean squared length #
The sum of CoarseGraining's coordinate averages is a single cube average. This is the exact collapse that lets the vector Jensen inequality be iterated without paying a dimensional factor.
The vector Jensen inequality at the fourth power #
Vector cube-average Jensen at the fourth power. For a vector field in
L^4 of the normalized cube measure,
|u_Q|^4 <= avg_Q |u|^4 ,
with |.| the Euclidean length and u_Q = cubeAverageVec Q u. Written with
vecNormSq on both sides, this is
vecNormSq (cubeAverageVec Q u)^2 <= cubeAverage Q (vecNormSq o u)^2.
The volume-normalized L^4 <= L^8 bridge #
The L^4 <= L^8 bridge on a cube. For a field valued in any normed
group and lying in L^8 of the normalized cube measure,
avg_Q ‖g‖^4 <= (‖g‖_{L^8(Q)})^4 ,
with ‖g‖_{L^8(Q)} = cubeLpNorm Q 8 g the volume-normalized L^8 norm. This
is the scalar L^4 <= L^8 comparison of CubeJensen applied to the pointwise
norm, read back through
cubeLpNorm_rpow_eq_cubeAverage_norm_rpow.
The Euclidean form of the L^4 <= L^8 bridge. With
‖u‖_{L^8(Q)} = cubeLpNorm Q 8 (vecNorm o u) the volume-normalized L^8 norm
read with the Euclidean pointwise length,
avg_Q |u|^4 <= (‖u‖_{L^8(Q)})^4 .