CubeSchauderBoundaryOneStep

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

Cube Schauder: the boundary one-step contraction at the Lipschitz rate

The boundary twin of CubeSchauderOneStep.excessDecay_oneStep_lipschitz. Three proved ingredients meet here:

1. the competitor — exists_harmonicCompetitor_reflected_odd, the chain of CubeSchauderBoundaryResidue re-run with the odd-reflection producer's met-face oddness kept (ExcessDecay.faceOdd_eqOn_reflectedWindow_of_ae's seam, run off continuousOn_of_harmonicOnNhd), so the fold can consume it;
2. the atom — CubeSchauderBoundaryTwin.exists_gradientLipschitz_boundary, the harmonic gradient-Lipschitz bound on the reflected window family;
3. the fold — CubeSchauderFold.exists_affineExcess_reflectedWindow_le, which converts the doubled-window excess of the atom's conclusion into the truncated-window excess the recursion iterates.

The result carries no interior geometry slot: it holds at every base point of □_m and every scale with n - 2 < m, so a single branch supplies the Campanato datum everywhere.

  E(u,U_k) ≤ C_contr(d) · 3^{-k} · E(u,U_0)
              + C_rem(d,k) · 3^{-n} · ‖u - V‖_{L²(U_2)} ,

U_j = (x + □_{n-j}) ∩ □_m, with the contraction at a full power of the step, exactly as in the interior branch — the reflected geometry costs only constants.

References

• Armstrong--Kuusi, Elliptic Regularity (ellipticregularity.tex), Proposition p.Schauder.C1alpha, display e.Sch1a.1.
• ABK26; Algsuperdiff/Frozen/External/CubeSchauder.lean.

1. The competitor, with its met-face oddness kept

theorem Algsuperdiff.Section4.Provider.Schauder.exists_harmonicCompetitor_reflected_odd {d : ℕ} [NeZero d] {m n : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hnm : n - 2 < m) (u : HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) {G : HCPolySupport.Vec d → HCPolySupport.Vec d} {KG : ℝ} (hKG : 0 ≤ KG) (hGL2 : HCPolySupport.MemVectorL2 (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) G) (hG : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) KG G) (hu : Support.IsDivFormWeakSolutionOn (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u.toH1Function G) : ∃ (V : HCPolySupport.Vec d → ℝ), InnerProductSpace.HarmonicOnNhd (V ∘ ⇑ExcessDecay.Schauder.toEuc.symm) (⇑ExcessDecay.Schauder.toEuc '' ExcessDecay.reflectedWindow x m (n - 2)) ∧ MeasureTheory.MemLp V 2 MeasureTheory.volume ∧ (∀ (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) ∧ (3 ^ (-n) * Support.normalizedL2On (ExcessDecay.truncatedWindow x m (n - 2)) fun (y : HCPolySupport.Vec d) => u.toFun y - V y) ≤ boundaryResidueConst d * KG * √(3 ^ n)

The harmonic competitor on the doubled window, odd about every met face.

CubeSchauderBoundaryResidue.exists_harmonicCompetitor_residue_reflected with the odd-reflection producer's oddness clause retained and transported to the Weyl representative: the representative is continuous on the doubled window (continuousOn_of_harmonicOnNhd) and almost everywhere equal there to the globally odd H¹ datum, so it is pointwise odd about every met face at every point of the doubled window — exactly the binder shape the fold consumes.

2. The fold constant

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

The fold constant C_fold(d) of CubeSchauderFold, named by choice.

Equations

• Algsuperdiff.Section4.Provider.Schauder.boundaryFoldConst d = ⋯.choose

theorem Algsuperdiff.Section4.Provider.Schauder.boundaryFoldConst_nonneg (d : ℕ) [NeZero d] : 0 ≤ boundaryFoldConst d

theorem Algsuperdiff.Section4.Provider.Schauder.affineExcess_reflectedWindow_le {d : ℕ} [NeZero d] {m n : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hmn : n - 2 < m) {V : HCPolySupport.Vec d → ℝ} (hupV : ∀ (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) (hlowV : ∀ (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) (hharm : InnerProductSpace.HarmonicOnNhd (V ∘ ⇑ExcessDecay.Schauder.toEuc.symm) (⇑ExcessDecay.Schauder.toEuc '' ExcessDecay.reflectedWindow x m (n - 2))) (hVR : MeasureTheory.MemLp V 2 (MeasureTheory.volume.restrict (ExcessDecay.reflectedWindow x m (n - 2)))) : Support.affineExcess (ExcessDecay.reflectedWindow x m (n - 2)) V ≤ boundaryFoldConst d * Support.affineExcess (ExcessDecay.truncatedWindow x m (n - 2)) V

The fold, at the named constant.

3. The one-step contraction

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

The contraction constant of the boundary Lipschitz one step.

Equations

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

theorem Algsuperdiff.Section4.Provider.Schauder.boundaryContractionConst_nonneg (d : ℕ) [NeZero d] : 0 ≤ boundaryContractionConst d

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

The remainder constant of the boundary Lipschitz one step.

Equations

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

theorem Algsuperdiff.Section4.Provider.Schauder.boundaryRemainderConst_nonneg (d : ℕ) [NeZero d] (k : ℕ) : 0 ≤ boundaryRemainderConst d k

theorem Algsuperdiff.Section4.Provider.Schauder.excessDecay_oneStep_boundary_lipschitz {d : ℕ} [NeZero d] (hd : d ≠ 0) {m n : ℤ} {k : ℕ} (hk : 3 ≤ k) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hnm : n - 1 ≤ m) (hmn : n - 2 < m) {u V : HCPolySupport.Vec d → ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (ExcessDecay.truncatedWindow x m n))) (hVR : MeasureTheory.MemLp V 2 (MeasureTheory.volume.restrict (ExcessDecay.reflectedWindow x m (n - 2)))) (hupV : ∀ (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) (hlowV : ∀ (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) (hharm : InnerProductSpace.HarmonicOnNhd (V ∘ ⇑ExcessDecay.Schauder.toEuc.symm) (⇑ExcessDecay.Schauder.toEuc '' ExcessDecay.reflectedWindow x m (n - 2))) : Support.affineExcess (ExcessDecay.truncatedWindow x m (n - ↑k)) u ≤ boundaryContractionConst d * 3 ^ (-↑k) * Support.affineExcess (ExcessDecay.truncatedWindow x m n) u + boundaryRemainderConst d k * (3 ^ (-n) * Support.normalizedL2On (ExcessDecay.truncatedWindow x m (n - 2)) fun (y : HCPolySupport.Vec d) => u y - V y)

The boundary one-step contraction at the Lipschitz rate.

For u on the window family U_j = (x + □_{n-j}) ∩ □_m at any base point of □_m, and V classically harmonic and met-face odd on the doubled window reflectedWindow x m (n-2),

  E(u,U_k) ≤ C_contr(d) · 3^{-k} · E(u,U_0)
              + C_rem(d,k) · 3^{-n} · ‖u - V‖_{L²(U_2)} .

The interior display, at the boundary, with no interior geometry slot: the reflected window replaces x + □_{n-2} ⊆ □_m.