OneStepCompetitor

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

The affine (Taylor) competitor: the affine contraction, first inequality

e.phi.approx.by.affine opens with the definition-level step

  E(v, U_k)  ≤  C 3^{(n-k)/2} [∇v]_{C^{0,1/2}(U_3)} ,

This module proves it, on an arbitrary truncated window and at the development's declared Hölder carrier Support.HolderSeminormBoundOn W (1/2) K G:

• affineExcessRaw_le_taylor — the raw excess is at most the sup-norm residual of the first-order Taylor competitor built at the window centre x with the average slope (∇v)_W, i.e. 2 d K (3^k/2)^{3/2};
• affineExcess_le_taylor — dividing by the |W|^{-1/d} normalizer (which the truncated-window sandwich of OneStepWindows bounds by 9·3^{-k}) turns this into

    E(v, (x+□_k) ∩ □_m)  ≤  taylorContractionConst d · K · (3^k)^{1/2} ,
  

  which at k = n-k' is the printed C 3^{(n-k')/2} [∇v]_{C^{0,1/2}} exactly.

The two proved atoms consumed are AffineSplitLift.abs_sub_affineLift_volumeAverage_le (the mean-value/Hölder residual) and SandwichNondegeneracyAttainment.normalizedL2On_le_of_abs_le (the L^∞ → L² conversion); the composition into affineExcess had no consumer before this module (affineResidualLevel has none in the tree).

What is NOT here (the residue this module makes precise)

The second inequality of e.phi.approx.by.affine substitutes the Schauder bound on K = [∇v]_{C^{0,1/2}(U_3)}; that bound is a harmonic-regularity estimate (a gradient-Hölder Schauder estimate up to a face of ∂□_m) and is not proved anywhere in this repository, in CoarseGraining, or in Mathlib.

1. The raw Taylor bound

theorem Algsuperdiff.Section4.Provider.ExcessDecay.affineExcessRaw_le_taylor {d : ℕ} {m k : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k - 1 ≤ m) {f : HCPolySupport.Vec d → ℝ} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} {K : ℝ} (hK : 0 ≤ K) (hmem : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (truncatedWindow x m k))) (hint : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (p : HCPolySupport.Vec d) => G p i) (truncatedWindow x m k) MeasureTheory.volume) (hf : Support.HasGradientOn (truncatedWindow x m k) f G) (hG : Support.HolderSeminormBoundOn (truncatedWindow x m k) (1 / 2) K G) : Support.affineExcessRaw (truncatedWindow x m k) f ≤ 2 * ↑d * K * (3 ^ k / 2) ^ (3 / 2)

The affine competitor on a truncated window.

The first-order Taylor polynomial of f at the window centre, built with the average gradient, is an admissible affine competitor; its L^∞ residual is the Hölder/mean-value bound 2 d K r^{3/2} at r = 3^k/2.

2. The excess form

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.taylorContractionConst (d : ℕ) : ℝ

The constant of the affine-competitor contraction: 18 d (1/2)^{3/2}, the product of the normalizer slack 9 of the truncated-window sandwich and the mean-value factor 2 d (1/2)^{3/2}.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.taylorContractionConst d = 18 * ↑d * (1 / 2) ^ (3 / 2)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.taylorContractionConst_nonneg (d : ℕ) : 0 ≤ taylorContractionConst d

theorem Algsuperdiff.Section4.Provider.ExcessDecay.affineExcess_le_taylor {d : ℕ} (hd : d ≠ 0) {m k : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k - 1 ≤ m) {f : HCPolySupport.Vec d → ℝ} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} {K : ℝ} (hK : 0 ≤ K) (hmem : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (truncatedWindow x m k))) (hint : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (p : HCPolySupport.Vec d) => G p i) (truncatedWindow x m k) MeasureTheory.volume) (hf : Support.HasGradientOn (truncatedWindow x m k) f G) (hG : Support.HolderSeminormBoundOn (truncatedWindow x m k) (1 / 2) K G) : Support.affineExcess (truncatedWindow x m k) f ≤ taylorContractionConst d * K * (3 ^ k) ^ (1 / 2)

The affine contraction, first inequality.

E(v, (x+□_k) ∩ □_m) ≤ C(d) · [∇v]_{C^{0,1/2}} · (3^k)^{1/2}. At k = n - j this is the printed C 3^{(n-j)/2} [∇v]_{C^{0,1/2}(U_3)}.