OneStepBoundaryOdd

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

The boundary datum leg through the odd class

The split Schauder bound prices the boundary branch against the far-side seminorm boundaryDatumLeg, an object with no direct manuscript counterpart. This module replaces it by the sharper and much more meaningful odd-class defect, using the repository's own odd-extension calculus (OddReflectionMap, OddReflectionSobolevL2).

The mechanism

Two proved facts do all the work.

• OddReflectionMap.oddExtend_affineLift — an affine function of the odd class 𝕃_odd(V) (IsOddAffineData: it vanishes on every hyperplane carrying a met face of ∂□_m) is its own partial odd extension. This is the paper's own free parameter ℓ in e.v0.hessian, i.e. the "affine shift freedom" of the excess, restricted to the class that survives the reflection.
• OddReflectionSobolevL2.eLpNorm_oddExtend_le — the partial odd extension costs at most 2^d in L², by the cellwise change of variables.

Together with oddExtend_sub: if the competitor V is odd about the met faces (oddExtend x m (n-2) V = V, which is exactly what the odd extension of a window competitor delivers) and ℓ ∈ 𝕃_odd, then V − ℓ is again odd, so

  E_raw(V, reflectedWindow) ≤ ‖V − ℓ‖_{L²(reflectedWindow)}
                            ≤ 2^d ‖V − ℓ‖_{L²(U_2)} = 2^d · affineDistOn U_2 V ℓ .

The residue, isolated to one scalar

  Csch = boundaryOddSchauderConst d = 2^d · boundarySchauderConst d ,
  K_h  = boundaryOddSchauderConst d · (3^{-n})^{1/2} · (3^{-(n-2)} · oddClassDefect) .

oddClassDefect x m n V c A is the amount by which restricting the affine competitor to the odd class 𝕃_odd(V) degrades the excess minimum on U_2. It is ≥ 0 always, and it is 0 on the interior branch, where isOddAffineData_of_no_met_face makes the odd class the full affine class (so a minimizer may be chosen inside it).

  oddClassDefect x m n V c A  ≤  C(d) · (3^{n-2})^{3/2} · [∇h]_{C^{0,1/2}(U_2)} ,

whose units are exactly right: multiplied by the display's prefactor boundaryOddSchauderConst d · (3^{-n})^{1/2} · 3^{-(n-2)} it yields C(d)·[∇h]_{C^{0,1/2}(U_2)}, the manuscript's second leg, including its indicator, which is carried here by the vanishing of the defect in the unmet case.

1. The two affine parametrizations

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

affineLift x c A is the affineEval competitor with intercept c − A·x.

2. Affine competitors are square integrable on both windows

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.memLp_affineEval_reflectedWindow {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (c : ℝ) (g : HCPolySupport.Vec d) : MeasureTheory.MemLp (Support.affineEval c g) 2 (MeasureTheory.volume.restrict (reflectedWindow x m k))

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.memLp_affineEval_truncatedWindow {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (c : ℝ) (g : HCPolySupport.Vec d) : MeasureTheory.MemLp (Support.affineEval c g) 2 (MeasureTheory.volume.restrict (truncatedWindow x m k))

3. The L² cost of the odd extension, normalized

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.normalizedL2On_oddExtend_le {d : ℕ} (x : HCPolySupport.Vec d) {m k : ℤ} (hkm : k < m) (f : HCPolySupport.Vec d → ℝ) (hRpos : 0 < (MeasureTheory.volume (reflectedWindow x m k)).toReal) (hUpos : 0 < (MeasureTheory.volume (truncatedWindow x m k)).toReal) (hfR : MeasureTheory.MemLp (oddExtend x m k f) 2 (MeasureTheory.volume.restrict (reflectedWindow x m k))) (hfU : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (truncatedWindow x m k))) : Support.normalizedL2On (reflectedWindow x m k) (oddExtend x m k f) ≤ 2 ^ d * Support.normalizedL2On (truncatedWindow x m k) f

The odd extension costs at most 2^d in the normalized seminorm. The unnormalized L² cost is OddReflectionSobolevL2.eLpNorm_oddExtend_le; the normalizers only help, because |U_2| ≤ |reflectedWindow|.

5. The odd-class defect

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.oddClassDefect {d : ℕ} (x : HCPolySupport.Vec d) (m n : ℤ) (V : HCPolySupport.Vec d → ℝ) (c : ℝ) (A : HCPolySupport.Vec d) : ℝ

The odd-class defect. The amount by which restricting the affine competitor to the odd class 𝕃_odd(V) degrades the excess minimum on U_2 = (x + □_{n-2}) ∩ □_m. It is the Lean surface's boundary datum leg.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.oddClassDefect_of_isAffineMinimizer {d : ℕ} {x : HCPolySupport.Vec d} {m n : ℤ} {V : HCPolySupport.Vec d → ℝ} {c : ℝ} {A : HCPolySupport.Vec d} (hmin : Support.IsAffineMinimizer (truncatedWindow x m (n - 2)) V (c - HCPolySupport.vecDot A x) A) : oddClassDefect x m n V c A = 0

The defect vanishes for a minimizer of the odd class when no face is met. In the interior regime the odd class is the whole affine class (isOddAffineData_of_no_met_face), so an unrestricted minimizer is admissible and the defect is 0.

6. The constant and the producer

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.boundaryOddSchauderConst (d : ℕ) [NeZero d] : ℝ

The Schauder constant of the boundary branch through the odd class: 2^d · boundarySchauderConst d.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.boundaryOddSchauderConst d = 2 ^ d * Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.boundarySchauderConst d

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.boundaryOddSchauderConst_nonneg (d : ℕ) [NeZero d] : 0 ≤ boundaryOddSchauderConst d