CubeSchauderFold

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

Cube Schauder: the reflected-window excess fold

CubeSchauderBoundaryTwin.exists_gradientLipschitz_boundary prices the harmonic gradient's Lipschitz constant on the inner window by the excess of the competitor on the doubled window reflectedWindow x m (n-2). The Campanato recursion needs that excess folded back onto the truncated window, where the solution lives. This module performs the fold, at every met configuration and with no analytic input beyond the competitor's own binders:

  E(V, reflectedWindow x m (n-2)) ≤ C(d) · E(V, truncatedWindow x m (n-2)) .

The four items of the fold, and where each comes from

• the odd-affine projection — ExcessDecay.affineExcessRaw_reflectedWindow_le_odd_ae: for a competitor fixed by the partial odd extension and an affine datum of the odd class 𝕃_odd, the doubled excess costs at most 2^d times the affine distance on U₂;
• the even-function odd transfer — the same atom's 2^d, which is ExcessDecay.normalizedL2On_oddExtend_le ('s cellwise change of variables);
• the near-side pricing at one met face —'s (★) (exists_oddClassDefect_le_affineExcessRaw) and its lower twin;
• the corner degeneracy — 's (★★) (exists_oddClassDefect_le_affineExcessRaw_corner_any): at two met faces the odd class collapses to {0} and the collapse is priced, so no distance-to-boundary dichotomy is needed.

That is what lets a single boundary-route one step replace the interior chain at every base point of □_m.

1. The odd affine datum, priced at every met configuration

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

The odd-class datum selector.

For a competitor odd about every met face at every point of the doubled window, classically harmonic there, and an affine minimizer datum (c,A) on U₂, there is an affine datum of the odd class 𝕃_odd whose odd-class defect is priced by the excess minimum on U₂.

Three regimes, three suppliers: no met face (the odd class is everything, the minimizer itself works and the defect is 0); exactly one met face ('s (★) at either orientation); at least two met faces ('s (★★), orientation-free through 's transport).

2. The fold

theorem Algsuperdiff.Section4.Provider.Schauder.exists_affineExcess_reflectedWindow_le (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (m n : ℤ) (x : HCPolySupport.Vec d) (V : HCPolySupport.Vec d → ℝ), x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → n - 2 < m → (∀ (l : Fin d), ExcessDecay.MeetsUpperFace x m (n - 2) l → ∀ y ∈ ExcessDecay.reflectedWindow x m (n - 2), V (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) l y) = -V y) → (∀ (l : Fin d), ExcessDecay.MeetsLowerFace x m (n - 2) l → ∀ y ∈ ExcessDecay.reflectedWindow x m (n - 2), V (HCPolySupport.coordFaceReflection (-(1 / 2) * 3 ^ m) l y) = -V y) → InnerProductSpace.HarmonicOnNhd (V ∘ ⇑ExcessDecay.Schauder.toEuc.symm) (⇑ExcessDecay.Schauder.toEuc '' ExcessDecay.reflectedWindow x m (n - 2)) → MeasureTheory.MemLp V 2 (MeasureTheory.volume.restrict (ExcessDecay.reflectedWindow x m (n - 2))) → Support.affineExcess (ExcessDecay.reflectedWindow x m (n - 2)) V ≤ C * Support.affineExcess (ExcessDecay.truncatedWindow x m (n - 2)) V

The reflected-window excess fold.

For a competitor odd about every met face at every point of the doubled window, classically harmonic there and square integrable there,

  E(V, reflectedWindow x m (n-2)) ≤ C(d) · E(V, truncatedWindow x m (n-2)) .

No affine-minimizer hypothesis: the minimizer is produced internally by ExcessDecay.exists_isAffineMinimizer_shifted_truncatedWindow. The constant is 2^d · (1 + C_price(d)) with C_price(d) the odd-class pricing constant of exists_oddAffineDatum_priced; the normalizers cost nothing, because the doubled window contains the truncated one.