AffineSplitLift

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

The affine lift ℓ_h of the boundary datum, and its residual

The boundary lane of §4.3 replaces the printed odd-reflection Schauder step by the affine split v = v₀ + w + ℓ_h of the replacement draft's item 2 (l.comparison.reduction). The affine lift is

  ∇ℓ_h := (∇h)_{W_0} ,     ℓ_h(x) = h(x) ,        W_0 := (x + □_n) ∩ □_m ,

and the whole point of the device is that the residual h - ℓ_h is controlled on W_0 by the C^{0,1/2} seminorm of ∇h — the leg the frozen theorem's general clause keeps (e.data.residual of the draft):

  ‖h - ℓ_h‖_{L^∞(W_0)} ≤ diam(W_0) · osc_{W_0} ∇h ≤ C(d) 3^{3n/2} [∇h]_{C^{0,1/2}(W_0)} .

This module proves that display, with C(d) = 2d at the sup-metric diameter, together with the H¹ realization of ℓ_h and the two elementary inputs (the slope functional and the deviation of a volume average from a pointwise value).

The dimensional constant, honestly

Vec d carries the supremum norm, so a slope A acts as a functional of operator norm ∑_i |A_i| ≤ d ‖A‖. That is the only source of the factor d in abs_sub_affineLift_le, and it is exactly the sup-vs-ℓ¹ conversion the manuscript hides in its C(d).

What is not done here

• No maximum principle: the passage from ‖h - ℓ_h‖_{L^∞(∂V ∩ ∂□_m)} to ‖w‖_{L^∞(V)} is a separate obligation (draft item 2(ii), first inequality).
• No harmonic function of any kind appears.
• HasGradientOn (now Algsuperdiff.Section4.Support.HasGradientOn, imported from Support/ClassicalGradient.lean) is the classical C^1 half of the source hypothesis h ∈ C^{1,1/2}(□_m); it is a genuine premise of the pinned statement, not a proof step promoted to a hypothesis.

References

• ABK26, l.excess.decay.good.scales, (datum).

1. The slope functional

slopeCLM and its @[simp] application lemma now live in Algsuperdiff/Section4/Support/ClassicalGradient.lean (the Support-layer home a frozen root anchor can bind); this module consumes them through open Algsuperdiff.Section4.Support. Only the norm estimates specific to the affine-split lane stay here.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.slopeCLM_sub {d : ℕ} (A B : HCPolySupport.Vec d) : Support.slopeCLM A - Support.slopeCLM B = Support.slopeCLM (A - B)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.norm_slopeCLM_le {d : ℕ} (A : HCPolySupport.Vec d) : ‖Support.slopeCLM A‖ ≤ ↑d * ‖A‖

The operator norm of the slope functional is at most d ‖A‖: the sup-norm of Vec d dualizes to ℓ¹.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.norm_slopeCLM_sub_le {d : ℕ} {G A : HCPolySupport.Vec d} {K : ℝ} (h : ‖G - A‖ ≤ K) : ‖Support.slopeCLM G - Support.slopeCLM A‖ ≤ ↑d * K

2. The affine lift

def Algsuperdiff.Section4.Provider.ExcessDecay.affineLift {d : ℕ} (x : HCPolySupport.Vec d) (c : ℝ) (A : HCPolySupport.Vec d) : HCPolySupport.Vec d → ℝ

The affine lift ℓ(y) = c + A · (y - x): the affine function with slope A taking the value c at x. With c = h(x) and A = (∇h)_{W_0} this is ℓ_h of the draft's e.data.affine.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.affineLift x c A y = c + HCPolySupport.vecDot A (y - x)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.vecDot_sub_right {d : ℕ} (A y x : HCPolySupport.Vec d) : HCPolySupport.vecDot A (y - x) = HCPolySupport.vecDot A y - HCPolySupport.vecDot A x

theorem Algsuperdiff.Section4.Provider.ExcessDecay.affineLift_eq_affineEval {d : ℕ} (x : HCPolySupport.Vec d) (c : ℝ) (A : HCPolySupport.Vec d) : affineLift x c A = Support.affineEval (c - HCPolySupport.vecDot A x) A

The affine lift is an affine function in the sense of Support.AffineExcess: it is affineEval at intercept c - A · x and slope A.

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.affineLift_self {d : ℕ} (x : HCPolySupport.Vec d) (c : ℝ) (A : HCPolySupport.Vec d) : affineLift x c A x = c

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.affineLiftH1 {d : ℕ} {U : Set (HCPolySupport.Vec d)} [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn U)] (hU : HCPolySupport.IsSobolevRegularDomain U) (x : HCPolySupport.Vec d) (c : ℝ) (A : HCPolySupport.Vec d) : HCPolySupport.H1Function U

The H¹ realization of the affine lift on a Sobolev-regular domain.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.affineLiftH1 hU x c A = (HCPolySupport.H1Function.affineOnIsSobolevRegularDomain hU A).addConst (c - HCPolySupport.vecDot A x)

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.affineLiftH1_toFun {d : ℕ} {U : Set (HCPolySupport.Vec d)} [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn U)] (hU : HCPolySupport.IsSobolevRegularDomain U) (x : HCPolySupport.Vec d) (c : ℝ) (A : HCPolySupport.Vec d) : (affineLiftH1 hU x c A).toFun = affineLift x c A

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.affineLiftH1_grad {d : ℕ} {U : Set (HCPolySupport.Vec d)} [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn U)] (hU : HCPolySupport.IsSobolevRegularDomain U) (x : HCPolySupport.Vec d) (c : ℝ) (A y : HCPolySupport.Vec d) : (affineLiftH1 hU x c A).grad y = A

3. The classical C¹ carrier

HasGradientOn — the classical C¹ half of the source hypothesis h ∈ C^{1,1/2}(□_m), written against Vec d's sup-norm through slopeCLM — now lives in Algsuperdiff/Section4/Support/ClassicalGradient.lean and is used here through open Algsuperdiff.Section4.Support.

4. The mean-value residual

theorem Algsuperdiff.Section4.Provider.ExcessDecay.abs_sub_affineLift_le {d : ℕ} {W : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → ℝ} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} {A : HCPolySupport.Vec d} {K r : ℝ} {x y : HCPolySupport.Vec d} (hW : Convex ℝ W) (hx : x ∈ W) (hy : y ∈ W) (hK : 0 ≤ K) (hf : Support.HasGradientOn W f G) (hG : ∀ p ∈ W, ‖G p - A‖ ≤ K) (hr : ‖y - x‖ ≤ r) : |f y - affineLift x (f x) A y| ≤ ↑d * K * r

The affine-lift residual, at an arbitrary slope.

If f is differentiable on the convex window W with gradient field G, and G stays within K of the slope A on W, then f differs from its affine lift at x by at most d·K·r on a window of sup-radius r around x. This is the mean-value inequality of the draft's e.data.residual computation.

5. The volume average as a slope

theorem Algsuperdiff.Section4.Provider.ExcessDecay.integrableOn_grad_coord {d : ℕ} {U : Set (HCPolySupport.Vec d)} [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn U)] (u : HCPolySupport.H1Function U) (i : Fin d) : MeasureTheory.IntegrableOn (fun (y : HCPolySupport.Vec d) => u.grad y i) U MeasureTheory.volume

Gradient coordinates of an H¹ function are integrable on the domain.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.norm_volumeAverageVec_sub_le {d : ℕ} {W : Set (HCPolySupport.Vec d)} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} {A : HCPolySupport.Vec d} {K : ℝ} (hvolpos : 0 < MeasureTheory.volume W) (hvoltop : MeasureTheory.volume W < ⊤) (hint : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (y : HCPolySupport.Vec d) => G y i) W MeasureTheory.volume) (hK : 0 ≤ K) (hG : ∀ y ∈ W, ‖G y - A‖ ≤ K) : ‖HCPolySupport.volumeAverageVec W G - A‖ ≤ K

The average slope is an admissible base point.

If G stays within K of a vector A on a window of positive finite volume, then so does its volume average. With A = G x this is the step |(∇h)_{W_0} - ∇h(x)| ≤ osc_{W_0} ∇h of the draft's residual computation.

6. The residual of the boundary datum's affine lift

theorem Algsuperdiff.Section4.Provider.ExcessDecay.abs_sub_affineLift_volumeAverage_le {d : ℕ} {W : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → ℝ} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} {K r : ℝ} {x y : HCPolySupport.Vec d} (hW : Convex ℝ W) (hx : x ∈ W) (hy : y ∈ W) (hK : 0 ≤ K) (hr0 : 0 ≤ r) (hvolpos : 0 < MeasureTheory.volume W) (hvoltop : MeasureTheory.volume W < ⊤) (hint : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (p : HCPolySupport.Vec d) => G p i) W MeasureTheory.volume) (hf : Support.HasGradientOn W f G) (hG : Support.HolderSeminormBoundOn W (1 / 2) K G) (hdiam : ∀ p ∈ W, ‖p - x‖ ≤ r) : |f y - affineLift x (f x) (HCPolySupport.volumeAverageVec W G) y| ≤ 2 * ↑d * K * r ^ (3 / 2)

The residual bound e.data.residual.

On a convex window W of sup-radius r around x, with f = h of class C^{1,1/2} (gradient field G, Hölder constant K), the affine lift at the average slope (∇h)_W satisfies

  |h(y) - ℓ_h(y)| ≤ 2 d K r^{3/2}      for every y ∈ W .

At W = (x+□_n) ∩ □_m and r = 3^n/2 this is the draft's ‖h - ℓ_h‖_{L^∞(W_0)} ≤ C(d) 3^{3n/2} [∇h]_{C^{0,1/2}(W_0)}, and it is the leg that the frozen theorem's general clause pays through its ‖(∇h)_W‖ slot.

7. The window instantiation

theorem Algsuperdiff.Section4.Provider.ExcessDecay.norm_sub_le_of_mem_truncatedWindow {d : ℕ} {x p : HCPolySupport.Vec d} {m k : ℤ} (hp : p ∈ truncatedWindow x m k) : ‖p - x‖ ≤ 3 ^ k / 2

Points of a truncated window are within sup-distance 3^k/2 of its centre.