SlopeStabilityEndpoints #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Small measure-theoretic helpers #
The volume average is additive on integrable differences.
‖a‖_{L²(W)} = |a| for a constant a, on a window of positive finite volume.
Jensen for the volume-normalized L² seminorm: |⨍_W f| ≤ ‖f‖_{L²(W)}.
Obtained from the completed-square expansion volumeAverage_sub_const_sq: the average of
(f − (f)_W)² is ⨍f² − ((f)_W)², and it is nonnegative.
Transfer the difference of nested-window means through normalized oscillation.
The oscillation #
The volume-normalized oscillation osc(u,W) = |W|^{−1/d} ‖u − (u)_W‖_{L²(W)}: the 3^{−j}‖u − (u)_{U_j}‖_{L²(U_j)} read at the
e.excess.def normalizer, so that it is directly comparable with
affineExcess.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The scale-normalized oscillation 3^{−j}‖u − (u)_W‖_{L²(W)}: the literal
normalizer and of e.excess.def.cubes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The un-normalized oscillation ‖u − (u)_W‖_{L²(W)} = |W|^{1/d} · osc(u,W).
The endpoint constant #
The endpoint constant of a sandwich of aspect ratio θ:
Ci(θ) = 2 + K(θ) + 2/c₀(θ), a single constant dominating both endpoint comparisons. Explicitly
a function of (d, θ); no existential.
Equations
Instances For
hhi: the excess and the slope are controlled by the oscillation #
hhi (the upper endpoint comparison), on a window carrying the inverse inequality.
E(u,W) + |∇ℓ| ≤ (1 + 2/c₀)·osc(u,W) for an affine minimizer (c,g).
E ≤ osc because the mean is one affine competitor; |∇ℓ| ≤ (2/c₀)osc because
hnd applied to ℓ − (u)_W plus Minkowski on ℓ − (u)_W = (ℓ − u) + (u − (u)_W) give c₀|W|^{1/d}|g| ≤ E_raw + osc_raw ≤ 2 osc_raw. hnd is the
inverse inequality, discharged from the sandwich in
endpoint_comparisons_of_axisCubeSandwich.
hlo: the oscillation is controlled by the excess and the slope #
hlo (the lower endpoint comparison), on a window carrying the diameter inequality.
osc(u,W) ≤ (2 + K)(E(u,W) + |∇ℓ|) for an affine minimizer (c,g).
Triangle inequality on u − (u)_W = (u − ℓ) + (ℓ − (ℓ)_W) + ((ℓ)_W − (u)_W);
the constant last term is |⨍(ℓ − u)| ≤ ‖ℓ − u‖_{L²(W)} = E_raw by Jensen.
haffosc is the direct (diameter) inequality, discharged from the sandwich in
endpoint_comparisons_of_axisCubeSandwich.
Both comparisons on a sandwiched window #
The two endpoint comparisons on the sandwich class.
On a window sandwiched between axis-parallel cubes of aspect ratio at least θ, with (c,g) a
chosen affine minimizer, both comparisons hold at the single explicit constant
Ci = endpointConst d θ = 2 + K(θ) + 2/c₀(θ):
osc(u,W) ≤ Ci · (E(u,W) + |∇ℓ|) and E(u,W) + |∇ℓ| ≤ Ci · osc(u,W) .
Both halves of the affine window geometry are discharged from the sandwich: the inverse inequality for the second, the direct/diameter inequality for the first.