OneStepEvenBoundFinal

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

(★): the even part of the affine minimizer is priced by the excess

This module closes's residue. For V classically harmonic on the doubled window R = reflectedWindow x m (n-2) and odd about the met face {yᵢ = a}, a = (1/2)·3^m, and (c, A) an affine minimizer of V on U₂ = truncatedWindow x m (n-2),

  ‖even part of ℓ*‖_{L²(U₂)} ≤ C(d) · affineExcessRaw U₂ V .                (★)

Composed with's reduction oddClassDefect_oddPart_le_evenPart, (★) says that the boundary branch's odd-class defect is priced by the excess itself: the producer's second leg folds into its first, and no [∇h] leg enters through the odd class.

The two steps

1. The slab comparison (normalizedL2On_evenAffinePart_le_of_hessian_bound). Integrating the two-point Taylor estimate of OneStepEvenBound over the core slab of depth delta, and using that an affine function with vanishing i-slope keeps half of its L²(U₂) size on the transversally halved slab (OneStepEvenBoundBox.normalizedL2On_coordBox_affineEval_half_le — the reverse-Chebyshev step), gives

     (1/2) N ≤ 3 ((3^{n-2}/delta)^d)^{1/2} E + 3 M delta² ,
   

   with N = ‖e‖_{L²(U₂)}, E = ‖V - ℓ*‖_{L²(U₂)} and M any bound for the Hessian of V - ℓ* on the Taylor box. The two f-terms cost only the volume ratio because the deep comparison point is a translate of the slab, of the same volume, still inside U₂.

2. The choice of delta (exists_evenAffinePart_le_affineExcessRaw). The interior Hessian estimate at the doubled window (OneStepEvenBoundHessian.exists_hessian_normalizedL2On_bound) gives M ≤ C₁ 3^{-2(n-2)} ‖V - ℓ*‖_{L²(R)}, and the odd bridge of OneStepEvenBoundOdd gives ‖V - ℓ*‖_{L²(R)} ≤ (2^d + 1)(E + N) — note the even part's L²(R) and L²(U₂) sizes are equal, since it has vanishing i-slope and the two boxes differ only in the i-edge. Taking delta = t·3^{n-2} with

     t = min (1/16) (1 / (1 + 24 K)) ,   K = C₁ (2^d + 1) ,
   

   makes 3 M delta² ≤ (1/8)(E + N), and (★) closes at C(d) = 8 ((1/t)^d)^{1/2} + 1/3 with no case split.

The constant is coefficient-free but not explicit as a closed form: C₁ is the constant of the transplanted interior Hessian estimate, itself produced existentially. This is the same convention schauderConst/boundarySchauderConst already follow.

1. The core slab, the deep slab and the translation between them

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.smul_basisVec_apply {d : ℕ} (delta : ℝ) (i j : Fin d) : (delta • HCPolySupport.basisVec i) j = if j = i then delta else 0

The i-th coordinate of the normal displacement delta·eᵢ.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.image_sub_slab {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i : Fin d) (delta : ℝ) : (fun (z : HCPolySupport.Vec d) => z - delta • HCPolySupport.basisVec i) '' coordBox (slabLo x m k i delta) (slabHi x m k i) = coordBox (deepLo x m k i delta) (deepHi x m k i delta)

The deep slab is the translate of the core slab.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.volume_toReal_coordBox_deep_ge {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} {delta : ℝ} (hdelta : 0 < delta) (hdelta16 : 16 * delta ≤ 3 ^ k) : delta ^ d ≤ (MeasureTheory.volume (coordBox (deepLo x m k i delta) (deepHi x m k i delta))).toReal

The deep slab's volume from below. Every edge is at least delta.

2. The slab comparison

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.normalizedL2On_evenAffinePart_le_of_hessian_bound {d : ℕ} {m n : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hmn : n - 2 < m) {i : Fin d} (hup : MeetsUpperFace x m (n - 2) i) (hother : ∀ (j : Fin d), j ≠ i → ¬MeetsUpperFace x m (n - 2) j ∧ ¬MeetsLowerFace x m (n - 2) j) {V : HCPolySupport.Vec d → ℝ} (hVodd : ∀ (z : HCPolySupport.Vec d), V (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) i z) = -V z) (hVR : MeasureTheory.MemLp V 2 (MeasureTheory.volume.restrict (reflectedWindow x m (n - 2)))) {c : ℝ} {A : HCPolySupport.Vec d} {delta M : ℝ} (hdelta : 0 < delta) (hdelta16 : 16 * delta ≤ 3 ^ (n - 2)) (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) : 1 / 2 * Support.normalizedL2On (truncatedWindow x m (n - 2)) (evenAffinePart x m i c A) ≤ (3 * √((3 ^ (n - 2) / delta) ^ d) * Support.normalizedL2On (truncatedWindow x m (n - 2)) fun (y : HCPolySupport.Vec d) => V y - Support.affineEval (c - HCPolySupport.vecDot A x) A y) + 3 * (M * delta ^ 2)

The slab comparison. The even part of the affine minimizer is priced on the near-face slab by the affine residual and the Hessian remainder.

3. (★)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.exists_evenAffinePart_le_affineExcessRaw (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (m n : ℤ) (x : HCPolySupport.Vec d) (i : Fin d) (V : HCPolySupport.Vec d → ℝ) (c : ℝ) (A : HCPolySupport.Vec d), x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → n - 2 < m → MeetsUpperFace x m (n - 2) i → (∀ (j : Fin d), j ≠ i → ¬MeetsUpperFace x m (n - 2) j ∧ ¬MeetsLowerFace x m (n - 2) j) → (∀ (z : HCPolySupport.Vec d), V (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) i z) = -V z) → InnerProductSpace.HarmonicOnNhd (V ∘ ⇑toEuc.symm) (⇑toEuc '' reflectedWindow x m (n - 2)) → MeasureTheory.MemLp V 2 (MeasureTheory.volume.restrict (reflectedWindow x m (n - 2))) → Support.IsAffineMinimizer (truncatedWindow x m (n - 2)) V (c - HCPolySupport.vecDot A x) A → Support.normalizedL2On (truncatedWindow x m (n - 2)) (evenAffinePart x m i c A) ≤ C * Support.affineExcessRaw (truncatedWindow x m (n - 2)) V

(★), the even-part bound. For a competitor odd about the met face and harmonic on the doubled window, the even part of an affine minimizer on U₂ is bounded by a dimensional constant times the excess itself.

Composed with's oddClassDefect_oddPart_le_evenPart, this prices the boundary branch's odd-class defect by the excess: the producer's datum leg folds into its excess leg.

4. The odd-class defect, priced by the excess

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.exists_oddClassDefect_le_affineExcessRaw (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (m n : ℤ) (x : HCPolySupport.Vec d) (i : Fin d) (V : HCPolySupport.Vec d → ℝ) (c : ℝ) (A : HCPolySupport.Vec d), x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → n - 2 < m → MeetsUpperFace x m (n - 2) i → (∀ (j : Fin d), j ≠ i → ¬MeetsUpperFace x m (n - 2) j ∧ ¬MeetsLowerFace x m (n - 2) j) → (∀ (z : HCPolySupport.Vec d), V (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) i z) = -V z) → InnerProductSpace.HarmonicOnNhd (V ∘ ⇑toEuc.symm) (⇑toEuc '' reflectedWindow x m (n - 2)) → MeasureTheory.MemLp V 2 (MeasureTheory.volume.restrict (reflectedWindow x m (n - 2))) → Support.IsAffineMinimizer (truncatedWindow x m (n - 2)) V (c - HCPolySupport.vecDot A x) A → oddClassDefect x m n V (oddAffineIntercept x m i A) (oddAffineSlope i A) ≤ C * Support.affineExcessRaw (truncatedWindow x m (n - 2)) V

's residue, discharged. Composing (★) with's reduction oddClassDefect_oddPart_le_evenPart, the odd-class defect at the normal part of an affine minimizer is priced by the excess itself. No [∇h] leg enters here: under face-oddness the datum has already been subtracted.