OneStepOddClassCornerApp

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

Corner pricing: the three slab applications

The packaged single-face and corner-slab applications of the two-point Taylor elimination, each combining: the window-hugging geometry, the Hessian value on the Taylor box, the box-generic slab estimate, the volume-ratio transfers, and the affine box-moment transfer back to the window.

• corner_faceApp_le — the single-face application at a met upper face: the even part of any affine competitor is priced by the residual on the window and the Hessian remainder on the doubled window.
• corner_pairApp_le — the corner application at the second face j against the competitor evenᵢ(ℓ*) (passed abstractly through its split identity): the doubly even part is priced by the residual, the normal-ramp size |Aᵢ|·delta, and the Hessian remainder of the shifted residual.

All constants are literal C(d) expressions; t is the free depth fraction (delta = t·3^{n−2}, t ≤ 1/16), chosen in the assembly.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.corner_faceApp_le {d : ℕ} {m n : ℤ} {x : HCPolySupport.Vec d} {face : Fin d} {V : HCPolySupport.Vec d → ℝ} {c : ℝ} {A : HCPolySupport.Vec d} {tt delta : ℝ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hmn : n - 2 < m) (hup : MeetsUpperFace x m (n - 2) face) (hVodd : ∀ (z : HCPolySupport.Vec d), V (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) face z) = -V z) (hharm : InnerProductSpace.HarmonicOnNhd (V ∘ ⇑toEuc.symm) (⇑toEuc '' reflectedWindow x m (n - 2))) (hVR : MeasureTheory.MemLp V 2 (MeasureTheory.volume.restrict (reflectedWindow x m (n - 2)))) (htt0 : 0 < tt) (htt16 : tt ≤ 1 / 16) (hdeltadef : delta = tt * 3 ^ (n - 2)) {CH : ℝ} (hCH0 : 0 ≤ CH) (hCH : ∀ (W : Set (HCPolySupport.Vec d)) (F : HCPolySupport.Vec d → ℝ) (p : HCPolySupport.Vec d) (r : ℝ), MeasureTheory.volume W ≠ ⊤ → 0 < (MeasureTheory.volume W).toReal → InnerProductSpace.HarmonicOnNhd (F ∘ ⇑toEuc.symm) (⇑toEuc '' W) → MeasureTheory.IntegrableOn (fun (y : HCPolySupport.Vec d) => F y ^ 2) W MeasureTheory.volume → 0 < r → Metric.ball p r ⊆ W → ‖fderiv ℝ (fderiv ℝ (F ∘ ⇑toEuc.symm)) (toEuc p)‖ ≤ CH * r⁻¹ * r⁻¹ * √((MeasureTheory.volume W).toReal / r ^ d) * Support.normalizedL2On W F) : Support.normalizedL2On (truncatedWindow x m (n - 2)) (evenAffinePart x m face c A) ≤ √((24 * ↑d + 1) * 4 ^ 2 + 2) * (3 * (√((1 / tt) ^ 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 * (CH * 256 * √(32 ^ d) * tt ^ 2 * Support.normalizedL2On (reflectedWindow x m (n - 2)) fun (y : HCPolySupport.Vec d) => V y - Support.affineEval (c - HCPolySupport.vecDot A x) A y))

The single-face application. For a competitor odd at the met upper face and an arbitrary affine (c, A), the even part at face is priced on the window by the residual and the doubled-window Hessian remainder.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.corner_pairApp_le {d : ℕ} {m n : ℤ} {x : HCPolySupport.Vec d} {i j : Fin d} {V : HCPolySupport.Vec d → ℝ} {c : ℝ} {A : HCPolySupport.Vec d} {c' : ℝ} {A' : HCPolySupport.Vec d} {tt delta : ℝ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hmn : n - 2 < m) (hij : i ≠ j) (hupi : MeetsUpperFace x m (n - 2) i) (hupj : MeetsUpperFace x m (n - 2) j) (hVoddj : ∀ (z : HCPolySupport.Vec d), V (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) j z) = -V z) (hharm : InnerProductSpace.HarmonicOnNhd (V ∘ ⇑toEuc.symm) (⇑toEuc '' reflectedWindow x m (n - 2))) (hVR : MeasureTheory.MemLp V 2 (MeasureTheory.volume.restrict (reflectedWindow x m (n - 2)))) (htt0 : 0 < tt) (htt16 : tt ≤ 1 / 16) (hdeltadef : delta = tt * 3 ^ (n - 2)) (hsplit3 : ∀ (y : HCPolySupport.Vec d), V y - Support.affineEval (c' - HCPolySupport.vecDot A' x) A' y = V y - Support.affineEval (c - HCPolySupport.vecDot A x) A y + oddAffinePart x m i A y) (hgi : evenAffineSlope j A' i = 0) {CH : ℝ} (hCH0 : 0 ≤ CH) (hCH : ∀ (W : Set (HCPolySupport.Vec d)) (F : HCPolySupport.Vec d → ℝ) (p : HCPolySupport.Vec d) (r : ℝ), MeasureTheory.volume W ≠ ⊤ → 0 < (MeasureTheory.volume W).toReal → InnerProductSpace.HarmonicOnNhd (F ∘ ⇑toEuc.symm) (⇑toEuc '' W) → MeasureTheory.IntegrableOn (fun (y : HCPolySupport.Vec d) => F y ^ 2) W MeasureTheory.volume → 0 < r → Metric.ball p r ⊆ W → ‖fderiv ℝ (fderiv ℝ (F ∘ ⇑toEuc.symm)) (toEuc p)‖ ≤ CH * r⁻¹ * r⁻¹ * √((MeasureTheory.volume W).toReal / r ^ d) * Support.normalizedL2On W F) : Support.normalizedL2On (truncatedWindow x m (n - 2)) (evenAffinePart x m j c' A') ≤ √((24 * ↑d + 1) * 4 ^ 2 + 2) * (3 * (√((1 / tt) ^ 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 * (|A i| * delta) + 3 * (CH * 256 * √(32 ^ d) * tt ^ 2 * Support.normalizedL2On (reflectedWindow x m (n - 2)) fun (y : HCPolySupport.Vec d) => V y - Support.affineEval (c' - HCPolySupport.vecDot A' x) A' y))

The corner application at the face j, against the shifted competitor (c', A') (in the assembly, the even part of the minimizer at i, so that its even part at j is the doubly even part). The residual of the shifted competitor is split through hsplit3 into the minimizer residual plus the normal ramp, which is pointwise at most |Aᵢ|·delta on the corner slab.