SandwichNondegeneracy #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The affine geometry of a sandwiched window #
l.iteration.lemma never assumes its windows are cubes. Its only stated
geometry is the sandwich x + □_{j-2} ⊆ U_j ⊆ y + □_j (hypothesis (iii),
scoped to j ≤ m per the binding). This module transports the exact cube
second moment of CubeMoments.lean to such a window, producing the two
window-geometry facts on which every §4.3 producer rests:
- the inverse (Bernstein) inequality
hndc₀ |W|^{1/d} |g| ≤ ‖c + g·x‖_{L²(W)}(normalizedL2On_affineEval_ge_of_sandwich), withc₀ = ndConst d θ = √(θ^d)·θ/(2√3)for a sandwich of aspect ratioθ = Lin/Lout; - the direct (diameter) inequality
haffosc‖ℓ − (ℓ)_W‖_{L²(W)} ≤ K |W|^{1/d} |∇ℓ|(normalizedL2On_affineEval_sub_average_le_of_sandwich), withK = oscConst d θ = 1/(√(θ^d)·θ·2√3).
They are the opposite halves of the same geometry, and they are exactly what
the two endpoint comparisons of Step 3 need. Note ndConst d θ · oscConst d θ = 1/12,
so on an exact cube (θ = 1) both constants are 1/(2√3) and both
inequalities are equalities.
For the paper's triadic sandwich the aspect ratio is θ = 3^{-2} = 1/9 at every scale, giving
the scale-free constants c₀ = 3^{-d-2}/(2√3) and K = 3^{d+2}/(2√3)
(ndConst_one_ninth, oscConst_one_ninth). Both are explicit definitions of d alone: no
existential constant appears anywhere in this module.
What is assumed and what is proved #
Nothing about W is assumed beyond the sandwich itself and 0 < Lin, 0 < Lout: positivity and
finiteness of |W|, square-integrability of the affine competitors, and the two inequalities are
all derived. In particular the nondegeneracy that AffineMinimizerExistence.lean had to
carry as a hypothesis (hlb/hub) becomes a theorem here --- see
SandwichNondegeneracyAttainment.lean.
References #
- ABK26,
e.grad.stability;l.iteration.lemma.
The two sandwich constants #
Volume bookkeeping for a sandwich #
Lin ≤ |W|^{1/d} ≤ Lout for a sandwiched window.
Square-integrability of the affine competitors #
The volume ratio of a sandwich #
The inner-cube volume ratio: (|W|/|□in|)^{1/2} ≤ (√(θ^d))⁻¹ for θ = Lin/Lout. Only the
outer inclusion is used: the inner cube enters through its volume Lin^d alone.
hnd: the inverse (Bernstein) inequality on a sandwiched window #
hnd at the sandwich's own aspect ratio. On a window sandwiched between two
axis-parallel cubes, c₀ |W|^{1/d} |g| ≤ ‖c + g·x‖_{L²(W)} with c₀ = ndConst d (Lin/Lout).
hnd at a uniform aspect ratio. If θ · Lout ≤ Lin then
ndConst d θ · |W|^{1/d} · |g| ≤ ‖c + g·x‖_{L²(W)}. This is the form the §4.3 producers need:
one constant for a whole family of windows.
The mean minimizes the L² deviation #
The volume average of a constant is that constant, on a window of positive finite volume.
Expansion of the average of (f − a)².
The mean minimizes the L² deviation: ‖f − (f)_W‖_{L²(W)} ≤ ‖f − a‖_{L²(W)} for every
constant a. This is what transfers the affine-oscillation bound from the outer cube to W.
haffosc: the direct (diameter) inequality on a sandwiched window #
haffosc at the sandwich's own aspect ratio. On a sandwiched window,
‖ℓ − (ℓ)_W‖_{L²(W)} ≤ K |W|^{1/d} |∇ℓ| with K = oscConst d (Lin/Lout).
On an exact cube (Lin = Lout) the constant is 1/(2√3) and the inequality is the equality
normalizedL2On_axisCube_affineEval_sub_average.
haffosc at a uniform aspect ratio. If θ · Lout ≤ Lin then
‖ℓ − (ℓ)_W‖_{L²(W)} ≤ oscConst d θ · |W|^{1/d} · |∇ℓ|.