CubeMoments #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The exact cube second moment #
ABK26, §4.3 rests four separate assertions on one unstated computation: the
second moment of an axis-parallel cube. For the open box
axisCube z L = ∏ᵢ (zᵢ, zᵢ + L) with centre x = axisCubeCenter z L = z + (L/2)·𝟙,
⨍_□ 1 = 1, ⨍_□ (xᵢ − xᵢ) = 0, ⨍_□ (xᵢ − xᵢ)(x_j − x_j) = δ_{ij} · L²/12 ,
and hence, for the affine function ℓ(x) = c + g·x,
⨍_□ ℓ = c + g·x ,
⨍_□ ℓ² = (c + g·x)² + (L²/12)|g|² (`volumeAverage_axisCube_affineEval_sq`).
On an exact cube both the inverse (Bernstein) inequality and the direct (diameter) inequality for affine functions become sharp:
(L/(2√3))·|g| ≤ ‖c + g·x‖_{L²(□)} , ‖ℓ − (ℓ)_□‖_{L²(□)} = (L/(2√3))·|g| .
The route is Fubini on a product measure: MeasureTheory.Measure.restrict_pi_pi identifies
volume.restrict (axisCube z L) with Measure.pi (fun i ↦ volume.restrict (zᵢ, zᵢ+L)), and
MeasureTheory.integral_fintype_prod_eq_prod factorizes the integral of a coordinate-wise
product (setIntegral_axisCube_prod). Every moment is then a one-dimensional
intervalIntegral.integral_pow computation: odd moments vanish because the interval is centred,
the diagonal second moment is L³/12, and off-diagonal moments vanish because one factor is an
odd moment.
Why this is not "the triangle inequality" #
This module supplies the true input; SandwichNondegeneracy.lean transports it
to the lemma's sandwiched windows. This is a change of proof attribution, not a
statement change: the sandwich is already a hypothesis of l.iteration.lemma.
References #
- ABK26,
e.grad.stability;l.iteration.lemma.
Measure-theoretic basics for axisCube #
The centre of axisCube z L (lower corner z, side L).
Equations
- Algsuperdiff.Section4.Provider.ExcessDecay.axisCubeCenter z L i = z i + L / 2
Instances For
|□(z,L)| = L^d.
A cube sits inside the corresponding closed box, which is compact; hence continuous functions are integrable on it.
The affine map x ↦ c + g·x is continuous.
The normalizer, applied once. If |U| = V ≠ 0 and ∫_U f = V · A, then ⨍_U f = A.
Every average in this module is computed through this lemma, so that no step depends on a
field_simp reading positivity facts out of the local context.
Fubini: the integral of a coordinate-wise product over a cube #
The product formula on a cube. ∫_□ ∏ᵢ hᵢ(xᵢ) = ∏ᵢ ∫_{(zᵢ,zᵢ+L)} hᵢ.
This is MeasureTheory.integral_fintype_prod_eq_prod transported along
MeasureTheory.Measure.restrict_pi_pi, which identifies volume.restrict (axisCube z L) with the
product of the one-dimensional restricted measures. No integrability hypotheses are needed (they
are absent from the mathlib statement as well).
The one-dimensional moments #
The cube moments #
First moment: the centre is the barycentre. ∫_□ (xᵢ − xᵢ) dx = 0.
Affine functions on an exact cube: the two sharp identities #
Recentring an affine function at an arbitrary point.
The linear part of an affine function integrates to zero over a cube.
The quadratic part: the cube second moment, summed against g ⊗ g.
The mean of an affine function over a cube is its value at the centre.
This is the single missing ingredient the whole §4.3 window geometry rests on: the inverse (Bernstein) inequality, the direct (diameter) inequality, attainment of the affine minimum on the consumption class, and both endpoint comparisons are corollaries.
The two sharp L² statements on an exact cube #
‖c + g·x‖_{L²(□)} = ((c + g·x)² + (L²/12)|g|²)^{1/2}.
The inverse (Bernstein) inequality on an exact cube, with the sharp
constant. (L/(2√3))·|g| ≤ ‖c + g·x‖_{L²(□)}.
|c + g·x| ≤ ‖c + g·x‖_{L²(□)} --- the intercept half of the two-sided cube bound.
The direct (diameter) identity on an exact cube. ‖ℓ − (ℓ)_□‖_{L²(□)} = (L/(2√3))·|∇ℓ| --- an equality, so the diameter constant's lower comparison
is sharp on cubes.