SlopeStability #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Gradient stability of consecutive best-affine approximations (e.grad.stability) #
|∇ℓ_k − ∇ℓ_{k−1}| ≤ C 3^{−k} ‖ℓ_k − ℓ_{k−1}‖_{L²(U_{k−1})} ≤ C (E_k + E_{k−1}) .
Both inequalities are proved here on the lemma's own window family.
- The second inequality is Minkowski for
‖·‖_{L²}plus the volume-ratio comparison on the nested windowsU_{k−1} ⊆ U_k, together with the two minimizing properties: this isnormalizedL2On_affineEval_sub_le. - The first inequality is the inverse (Bernstein) inequality for affine
functions, which the tex attributes to "the triangle inequality". It is
supplied here by
normalizedL2On_affineEval_ge_of_sandwich, i.e. by the exact cube second moment transported along the sandwichx + □_{k−3} ⊆ U_{k−1} ⊆ y + □_{k−1}thatl.iteration.lemmaalready assumes. This is a change of proof attribution, not of statement: nothing is added to the source hypotheses.
The constant chase #
Write A = |U_k|, B = |U_{k−1}|, e = 1/d, S = |∇ℓ_k − ∇ℓ_{k−1}|:
c₀ B^e S ≤ ‖ℓ_k − ℓ_{k−1}‖_{L²(U_{k−1})} (hnd)
≤ ‖u − ℓ_{k−1}‖_{L²(U_{k−1})} + ‖u − ℓ_k‖_{L²(U_{k−1})} (Minkowski)
≤ B^e E_{k−1} + (A/B)^{1/2} A^e E_k (minimality + ratio)
= B^e (E_{k−1} + (A/B)^{e+1/2} E_k) ,
so with κ the volume-ratio constant (A/B)^{1/d+1/2} ≤ κ (and 1 ≤ κ derived from
nestedness, one_le_volumeRatioConst_of_nested),
Cstab = slopeStabilityConst d θ κ = κ / ndConst d θ .
Under the paper's sandwich θ = 3^{−2}, so c₀ = 3^{−d−2}/(2√3) and Cstab = C(d), matching the tex's C in e.grad.stability; the tex's C 3^{−k} normalizer
is the Lean |U_{k−1}|^{−1/d} up to the same bounded volume ratio.
Scalar versus vector form #
The tex's Step 2 runs the Grönwall argument on the vector sequence ∇ℓ_{b−l} − ∇ℓ_b, while the proved §4.3 iteration engine (IterationLemma.lean,
hypothesis hstab) runs on the scalar sequence p_k = |∇ℓ_k|. records that
the two Grönwall arguments are therefore not literally the same argument. The
bridge is the reverse triangle inequality
abs_slopeMagnitude_sub_slopeMagnitude_le, proved below; the scalar statement
is weaker than the vector one, so nothing is smuggled by using it.
References #
- ABK26,
e.grad.stability.
The slope magnitude is a Euclidean norm #
Triangle inequality for the slope magnitude |g|₂ = (∑ᵢ gᵢ²)^{1/2}. The ambient norm on
Vec d = Fin d → ℝ is the sup norm, so this is not available from the Pi instance.
Reverse triangle inequality for the slope magnitude: the difference of the magnitudes is controlled by the magnitude of the difference.
Undoing the excess normalizer #
min_ℓ ‖u − ℓ‖_{L²(W)} = |W|^{1/d} · E(u,W) --- the |W|^{−1/d} normalizer of
affineExcess undone on a window of positive volume.
The second inequality of e.grad.stability #
The L² comparison of two affine minimizers on nested windows (the second inequality of
e.grad.stability). If (c,g) minimizes on W and (c',g') minimizes on W' ⊆ W, then
‖ℓ − ℓ'‖_{L²(W')} ≤ min_ℓ ‖u − ℓ‖_{L²(W')} + (|W|/|W'|)^{1/2} · min_ℓ ‖u − ℓ‖_{L²(W)}.
Minkowski on ℓ − ℓ' = (u − ℓ') + (ℓ − u), then the volume-ratio comparison on the second term.
The constant, and the arithmetic of the chase #
The slope-stability constant of a window family: Cstab = κ / c₀(θ), with κ the
volume-ratio constant of the nesting and c₀(θ) = ndConst d θ the nondegeneracy constant of the
sandwich. Explicitly a function of (d, θ, κ); no existential.
Equations
Instances For
1 ≤ κ is derived from nestedness, not assumed: a nested family has volume ratio at least
one, and the exponent 1/d + 1/2 is nonnegative.
The volume-ratio constant of the triadic sandwich family:
κ(d) = (3^{3d})^{1/d + 1/2}, i.e. 27 · 3^{3d/2}. On the family
x + □_{k−2} ⊆ U_k ⊆ y + □_k the ratio |U_{k+1}|/|U_k| is at most
3^{(k+1)d}/3^{(k−2)d} = 3^{3d}, so this value works at every scale. Explicitly a function of
d; no existential.
Equations
Instances For
The producer #
Gradient stability (e.grad.stability) on the sandwich class.
For a nested family U : ℤ → Set (Vec d) whose members are sandwiched between axis-parallel cubes
of aspect ratio at least θ, with u square-integrable on each window and (cc k, gg k) a chosen
affine minimizer on U k, the minimizer slopes on adjacent scales satisfy
| |∇ℓ_k| − |∇ℓ_{k−1}| | ≤ (κ / c₀(θ)) · (E_k + E_{k−1}) ,
exactly the shape IterationLemma.iterationSlopeBound consumes as hstab, with the explicit
Cstab = slopeStabilityConst d θ κ.
Neither is 1 ≤ κ, which one_le_volumeRatioConst_of_nested derives.