QuasiMonotone #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Excess quasi-monotonicity (hmono) on the cube-sandwich family #
l.iteration.lemma never displays the inequality
E_k ≤ κ · E_{k+1}
but it uses it twice: once in Step 2, where the shifted excess sum is
reabsorbed across its h end terms (e.sum.excess.bound, whose graph edge
records "the reabsorption crosses the h end-terms of the shifted sum using
the per-scale quasi-monotonicity E_k ≤ κ E_{k+1}, which is a consequence of
the definition together with the window sandwich"), and once implicitly inside
the printed reabsorption factor 3^{(d+2)h}, which is κ^h. It is the
hmono hypothesis of the proved iteration engine
(IterationLemma.combinedBound, IterationLemma.iterationSlopeBound).
This module proves it, from geometry alone, on the family the lemma actually assumes.
The mechanism #
The competitor set is the same set of affine functions for both windows, so the domain comparison
is competitor-by-competitor: for W' ⊆ W and every affine ℓ,
‖u − ℓ‖_{L²(W')} ≤ (|W|/|W'|)^{1/2} ‖u − ℓ‖_{L²(W)} (Support.normalizedL2On_le_of_subset)
and the left-hand infimum is below every competitor
(Support.affineExcessRaw_le_affineDistOn), which gives
affineExcessRaw W' u ≤ (|W|/|W'|)^{1/2} affineExcessRaw W u. Restoring the |W|^{−1/d}
normalizer of Support.affineExcess turns the exponent 1/2 into 1/d + 1/2:
E(u, W') ≤ (|W|/|W'|)^{1/d + 1/2} E(u, W) .
The constant actually obtained #
On the sandwich x + □_{k−2} ⊆ U_k ⊆ y + □_k the one-scale ratio is
|U_{k+1}|/|U_k| ≤ 3^{(k+1)d}/3^{(k−2)d} = 3^{3d}, so the derived constant is
exactly the one already proved for slope stability,
κ = volumeRatioConstTriadic d = (3^{3d})^{1/d + 1/2} = 3^{3 + 3d/2} ,
with 1 ≤ κ available as one_le_volumeRatioConstTriadic — so the engine's hκ slot is
discharged by the same object. Nothing here is assumed: the ratio bound is
proved from the two inclusions.
The route above gives 3 + 3d/2 (the 3 is 3d · (1/d), the 3d/2 is 3d · (1/2); 1 + 3d/2 would need the ratio 3^d for the first summand and
3^{3d} for the second, so it cannot come from one ratio). Since 3 + 3d/2 ≤ d + 2 fails for every d ≥ 1, the printed 3^{(d+2)h} is too small at
the derived κ in every dimension, not only for d ≥ 3. This module does not
change any statement: κ is an explicit def here and the caveat is's to
adjust.
References #
- ABK26,
e.excess.def;e.sum.excess.bound.
MemLp transfer across the nesting #
The iteration engine reads u on every window of the family, while a caller typically knows
u ∈ L² on the largest one. Restriction is monotone in the set, so MemLp transfers downwards;
this is the whole content.
MemLp restricts to a subwindow. Measure.restrict_mono plus MemLp.mono_measure.
Domain comparison for the excess #
Domain comparison for the unnormalized excess. For W' ⊆ W of positive volume, with every
affine deviation of u square-integrable on W,
min_ℓ ‖u − ℓ‖_{L²(W')} ≤ (|W|/|W'|)^{1/2} · min_ℓ ‖u − ℓ‖_{L²(W)}.
Proved competitor-by-competitor: the seminorm comparison holds for each affine ℓ, and the
left-hand infimum is below every competitor.
Domain comparison for the excess E(u,W) = |W|^{−1/d} min_ℓ ‖u − ℓ‖_{L²(W)}.
For W' ⊆ W of positive volume,
E(u, W') ≤ (|W|/|W'|)^{1/d + 1/2} · E(u, W),
the exponent splitting as 1/d (restoring the two |·|^{−1/d} normalizers) plus 1/2 (the
seminorm volume ratio).
The hmono producer #
Excess quasi-monotonicity on an abstract nested family, in the exact shape
the proved iteration engine consumes as hmono
(IterationLemma.combinedBound, IterationLemma.iterationSlopeBound, at E:= fun k => affineExcess (U k) u):
hratio is the only quantitative input; the cube-sandwich instance below proves it.