OneStepTriangle

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The excess algebra of the one-step contraction

The two purely definitional children of l.excess.decay.good.scales:

• The triangle assembly needs E(u,W) ≤ E(v,W) + |W|^{-1/d} ‖u-v‖_{L²(W)} and the passage of ‖u-v‖ between two windows of the family at the volume-ratio cost. Landed here as affineExcess_sub_le_truncatedWindow and normalizedL2On_truncatedWindow_le.
• The oscillation-to-excess comparison needs 3^{-n}‖u - (u)_{U_0}‖_{L²(U_0)} ≤ E(u,U_0) + C|∇ℓ_0|. Landed here as oscillationScaled_truncatedWindow_le, by composing the two proved sandwich comparisons of SlopeStabilityEndpoints / IterationLemmaProviderGeometry.

Two disclosed deviations from the printed displays

1. The subadditivity carrier. The tree's proved subadditivity (BoundaryLaneExcess.affineExcessRaw_add_le) is unusable from this module: BoundaryLaneExcess and SandwichNondegeneracyAttainment both declare normalizedL2On_le_of_abs_le in the same namespace, so they cannot be imported together, and the excess-geometry lane needs the latter. The subadditivity is therefore re-proved here from Minkowski (normalizedL2On_add_le) under the disclosing name affineExcessRaw_add_le_of_memLp, with the affine MemLp slot explicit.
2. The constant of the oscillation fold. ABK26 prints 3^{-n}‖u-(u)_{U_0}‖ ≤ E(u,U_0) + C|∇ℓ_0|, i.e. the constant on the slope only. The proved endpoint comparison charges one constant to both summands: osc ≤ endpointConst d (1/9) · (E + |∇ℓ|). That is weaker than print on the excess leg, and it is what is stated here. (The printed constant already hides a window-geometry fact, not "the triangle inequality" alone.)

1. Affine competitors are square-integrable on a truncated window

theorem Algsuperdiff.Section4.Provider.ExcessDecay.memLp_affineEval_truncatedWindow {d : ℕ} {m k : ℤ} (x : HCPolySupport.Vec d) (c : ℝ) (g : HCPolySupport.Vec d) : MeasureTheory.MemLp (Support.affineEval c g) 2 (MeasureTheory.volume.restrict (truncatedWindow x m k))

2. Subadditivity of the raw excess

theorem Algsuperdiff.Section4.Provider.ExcessDecay.affineExcessRaw_add_le_of_memLp {d : ℕ} {W : Set (HCPolySupport.Vec d)} {u w : HCPolySupport.Vec d → ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict W)) (hw : MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict W)) (haff : ∀ (c : ℝ) (g : HCPolySupport.Vec d), MeasureTheory.MemLp (Support.affineEval c g) 2 (MeasureTheory.volume.restrict W)) : (Support.affineExcessRaw W fun (y : HCPolySupport.Vec d) => u y + w y) ≤ Support.affineExcessRaw W u + Support.normalizedL2On W w

Subadditivity of the raw excess, re-proved from Minkowski with the affine MemLp slot explicit (see deviation 1 in the module docstring).

3. The triangle step at the |W|^{-1/d} normalizer

theorem Algsuperdiff.Section4.Provider.ExcessDecay.affineExcess_sub_le_truncatedWindow {d : ℕ} (hd : d ≠ 0) {m k : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k - 1 ≤ m) {u v : HCPolySupport.Vec d → ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (truncatedWindow x m k))) (hv : MeasureTheory.MemLp v 2 (MeasureTheory.volume.restrict (truncatedWindow x m k))) : Support.affineExcess (truncatedWindow x m k) u ≤ Support.affineExcess (truncatedWindow x m k) v + 9 * 3 ^ (-k) * Support.normalizedL2On (truncatedWindow x m k) fun (y : HCPolySupport.Vec d) => u y - v y

The triangle assembly, the comparison step.

E(u,W) ≤ E(v,W) + 9·3^{-k}·‖u-v‖_{L²(W)} on the truncated window W = (x+□_k) ∩ □_m; the factor 9 is the aspect-1/9 slack of the truncated normalizer against the cube normalizer 3^{-k}.

4. The window transfer of the L² remainder

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_truncatedWindow_le {d : ℕ} {m k l : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k - 1 ≤ m) (hlm : l - 1 ≤ m) (hkl : k ≤ l) {f : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (truncatedWindow x m l))) : Support.normalizedL2On (truncatedWindow x m k) f ≤ √((3 ^ (l - k + 2)) ^ d) * Support.normalizedL2On (truncatedWindow x m l) f

The volume-ratio transfer. Passing ‖f‖_{L²} from the outer window U_l down to the inner window U_k (k ≤ l) costs (3^{l-k+2})^{d/2}. This is the 3^{(d/2+1)k} bookkeeping, with the +2 coming from the truncated window's own aspect ratio.

5. The oscillation-to-excess fold

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_isAffineMinimizer_truncatedWindow {d : ℕ} {m k : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k - 1 ≤ m) {u : HCPolySupport.Vec d → ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (truncatedWindow x m k))) : ∃ (c : ℝ) (g : HCPolySupport.Vec d), Support.IsAffineMinimizer (truncatedWindow x m k) u c g

Existence of an affine minimizer on a truncated window (the source's ℓ(u,W)), from the proved sandwich attainment.