OneStepEvenBound

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

The two-point Taylor estimate at the met face

This module carries the analytic step's residue (★): for a competitor V odd about the met face and harmonic on the doubled window, the even part of an affine competitor is controlled pointwise, on a near-face slab of depth delta, by the affine residual f = V - ℓ* at two nearby points plus a Hessian remainder.

The mechanism

Write ρ for the reflection through the met face {yᵢ = a}, a = (1/2)·3^m. The reflection identity f ∘ ρ + f = -2 e of OneStepEvenBoundOdd is exact but by itself carries no information: it is an identity. Harmonicity enters through a second-order Taylor comparison along the normal direction, applied twice:

• to the pair (y, ρ y), whose displacement is 2 s·eᵢ with s = a - yᵢ;
• to the pair (y, y - delta·eᵢ), whose displacement is -delta·eᵢ.

The first, combined with the reflection identity, gives |e y + f y + s β| ≤ 2 M delta² where β is the (unknown) normal derivative of f at y; the second gives |f(y - delta·eᵢ) - f y + delta β| ≤ M delta² and therefore determines β up to M delta. Eliminating β — legitimate because s/delta ∈ (0,1], which is exactly why the deep comparison point is taken at the fixed depth delta rather than at a depth proportional to s — leaves

  |e y| ≤ 2 |f y| + |f (y - delta·eᵢ)| + 3 M delta² .

This is the pointwise input the L² assembly of OneStepEvenBoundFinal consumes. Note that no continuity of V at the face is used, and no membership hypothesis beyond y in the core slab.

1. Displacements along the normal

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.normalizedL2On_abs {d : ℕ} (W : Set (HCPolySupport.Vec d)) (f : HCPolySupport.Vec d → ℝ) : (Support.normalizedL2On W fun (y : HCPolySupport.Vec d) => |f y|) = Support.normalizedL2On W f

The normalized seminorm does not see absolute values.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.normalizedL2On_le_of_abs_le_translate {d : ℕ} {W : Set (HCPolySupport.Vec d)} {u f : HCPolySupport.Vec d → ℝ} {v : HCPolySupport.Vec d} {a R : ℝ} (hW : MeasurableSet W) (hWpos : 0 < (MeasureTheory.volume W).toReal) (ha : 0 ≤ a) (hR : 0 ≤ R) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict W)) (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict W)) (hft : MeasureTheory.MemLp (fun (y : HCPolySupport.Vec d) => f (y - v)) 2 (MeasureTheory.volume.restrict W)) (hdom : ∀ y ∈ W, |u y| ≤ a * |f y| + |f (y - v)| + R) : Support.normalizedL2On W u ≤ a * Support.normalizedL2On W f + Support.normalizedL2On ((fun (z : HCPolySupport.Vec d) => z - v) '' W) f + R

Integrate a translated pointwise domination bound on an arbitrary window.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.coordFaceReflection_sub_self {d : ℕ} (a : ℝ) (i : Fin d) (y : HCPolySupport.Vec d) : HCPolySupport.coordFaceReflection a i y - y = (2 * (a - y i)) • HCPolySupport.basisVec i

The face reflection displaces a point by twice its distance to the face, along the normal.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sub_smul_basisVec_sub_self {d : ℕ} (t : ℝ) (i : Fin d) (y : HCPolySupport.Vec d) : y - t • HCPolySupport.basisVec i - y = -t • HCPolySupport.basisVec i

Translating by a multiple of a basis vector.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.toEuc_smul_basisVec {d : ℕ} (t : ℝ) (i : Fin d) : toEuc (t • HCPolySupport.basisVec i) = t • EuclideanSpace.single i 1

The toEuc image of a normal displacement.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.norm_toEuc_smul_basisVec {d : ℕ} (t : ℝ) (i : Fin d) : ‖toEuc (t • HCPolySupport.basisVec i)‖ = |t|

The length of a normal displacement.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.abs_evenAffinePart_le_pointwise_of_mem {d : ℕ} {m : ℤ} {x : HCPolySupport.Vec d} {i : Fin d} {V : HCPolySupport.Vec d → ℝ} (hVodd : ∀ (z : HCPolySupport.Vec d), V (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) i z) = -V z) {c : ℝ} {A : HCPolySupport.Vec d} {delta M : ℝ} (hdelta : 0 < delta) (hM : 0 ≤ M) {T : Set (HCPolySupport.Vec d)} (hT : Convex ℝ T) (hharm : ∀ z ∈ T, InnerProductSpace.HarmonicAt ((fun (y : HCPolySupport.Vec d) => V y - Support.affineEval (c - HCPolySupport.vecDot A x) A y) ∘ ⇑toEuc.symm) (toEuc z)) (hMbound : ∀ z ∈ T, ‖fderiv ℝ (fderiv ℝ ((fun (y : HCPolySupport.Vec d) => V y - Support.affineEval (c - HCPolySupport.vecDot A x) A y) ∘ ⇑toEuc.symm)) (toEuc z)‖ ≤ M) {y : HCPolySupport.Vec d} (hyT : y ∈ T) (hrT : HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) i y ∈ T) (hyD : y - delta • HCPolySupport.basisVec i ∈ T) (hylo : 1 / 2 * 3 ^ m - delta < y i) (hyhi : y i < 1 / 2 * 3 ^ m) : |evenAffinePart x m i c A y| ≤ 2 * |V y - Support.affineEval (c - HCPolySupport.vecDot A x) A y| + |V (y - delta • HCPolySupport.basisVec i) - Support.affineEval (c - HCPolySupport.vecDot A x) A (y - delta • HCPolySupport.basisVec i)| + 3 * M * delta ^ 2

Two-point Taylor elimination on a convex set containing both comparison points.

2. The pointwise estimate on the core slab

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.abs_evenAffinePart_le_pointwise {d : ℕ} {m n : ℤ} {x : HCPolySupport.Vec d} {i : Fin d} {V : HCPolySupport.Vec d → ℝ} (hVodd : ∀ (z : HCPolySupport.Vec d), V (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) i z) = -V z) {c : ℝ} {A : HCPolySupport.Vec d} {delta M : ℝ} (hdelta : 0 < delta) (hM : 0 ≤ M) (hharm : ∀ z ∈ coordBox (taylorLo x m (n - 2) i delta) (taylorHi x m (n - 2) i delta), InnerProductSpace.HarmonicAt ((fun (y : HCPolySupport.Vec d) => V y - Support.affineEval (c - HCPolySupport.vecDot A x) A y) ∘ ⇑toEuc.symm) (toEuc z)) (hMbound : ∀ z ∈ coordBox (taylorLo x m (n - 2) i delta) (taylorHi x m (n - 2) i delta), ‖fderiv ℝ (fderiv ℝ ((fun (y : HCPolySupport.Vec d) => V y - Support.affineEval (c - HCPolySupport.vecDot A x) A y) ∘ ⇑toEuc.symm)) (toEuc z)‖ ≤ M) {y : HCPolySupport.Vec d} (hy : y ∈ coordBox (slabLo x m (n - 2) i delta) (slabHi x m (n - 2) i)) (hyD : y - delta • HCPolySupport.basisVec i ∈ coordBox (taylorLo x m (n - 2) i delta) (taylorHi x m (n - 2) i delta)) : |evenAffinePart x m i c A y| ≤ 2 * |V y - Support.affineEval (c - HCPolySupport.vecDot A x) A y| + |V (y - delta • HCPolySupport.basisVec i) - Support.affineEval (c - HCPolySupport.vecDot A x) A (y - delta • HCPolySupport.basisVec i)| + 3 * M * delta ^ 2

The two-point Taylor estimate at a near-face point.

For f = V - ℓ* harmonic on the Taylor box with Hessian bounded by M, and y in the core slab of depth delta under the met face, comparing f at y with its values at the reflected point ρ y and at the pushed point y - delta·eᵢ eliminates the unknown normal derivative and prices the even part pointwise.