OneStepBoundarySchauder

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

The Schauder gradient-Hölder estimate, boundary branch: the producer

OneStepSchauderProducer.exists_gradientHolder_interior instantiates the Schauder atom at the interior ball family. This module does the same at the boundary family of OneStepBoundaryGeometry: the harmonicity domain is the partially reflected window reflectedWindow x m (n-2), on which the odd extension of the competitor is classically harmonic (OneStepSchauderComposeBoundary.exists_classicalCompetitor_reflectedWindow), and the Hölder window is the branch's own U_3 = (x + □_{n-3}) ∩ □_m.

The output is exactly the four-slot package hint / hgrad / hhol / hschauder that OneStepConditional.excessDecay_oneStep_of_harmonicApprox consumes:

  GV := gradField V ,
  ∀ i, IntegrableOn (fun p => GV p i) U_3 ,
  HasGradientOn U_3 V GV ,
  HolderSeminormBoundOn U_3 (1/2) K GV ,
  K ≤ Csch(d) · (3^{-n})^{1/2} · (3^{-(n-2)} · E_raw(V, reflectedWindow)) ,

with

  Csch(d) = boundarySchauderConst d
          = 48 · 3^{3/2} · schauderConst d · √((24(d+1))^d) ,

the interior constant with 12(d+1) replaced by 24(d+1) — the sole cost of the reflection is the 2^d volume spread of OddReflectionVolume.

The raw form above is stated at the unnormalized excess minimum E_raw together with the explicit scale factor 3^{-(n-2)}, because that is the shape in which the two downstream normalizers are read off:

• exists_gradientHolder_boundary divides by the reflected window's own normalizer |reflectedWindow|^{-1/d} ≥ (2·3^{n-2})^{-1}, giving the excess E(V, reflectedWindow) at the cost of a factor 2;
• the split bound splits E_raw over U_2 ⊔ (reflectedWindow \ U_2) and divides by U_2's normalizer, producing the manuscript's C 3^{-n/2} E(v, U_2) + K_h with K_h the far-side (datum) leg.

The raw display is tight: the inequality proved is the atom's own output with the powers of 3 regrouped, no slack.

References

• ABK26, l.excess.decay.good.scales, the Schauder gradient-Hölder estimate.

1. The constant

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

The Schauder constant of the boundary branch. C(d) explicit: 48 · 3^{3/2} · schauderConst d · √((24(d+1))^d).

Equations

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

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

2. The scale arithmetic

3. The producer, raw form

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.exists_gradientHolder_boundary_raw {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 → ℝ} (hharm : InnerProductSpace.HarmonicOnNhd (V ∘ ⇑toEuc.symm) (⇑toEuc '' reflectedWindow x m (n - 2))) (hintsq : ∀ (c : ℝ) (g : HCPolySupport.Vec d), MeasureTheory.IntegrableOn (fun (y : HCPolySupport.Vec d) => (V y - Support.affineEval c g y) ^ 2) (reflectedWindow x m (n - 2)) MeasureTheory.volume) : ∃ (K : ℝ), 0 ≤ K ∧ (∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (p : HCPolySupport.Vec d) => gradField V p i) (truncatedWindow x m (n - 3)) MeasureTheory.volume) ∧ Support.HasGradientOn (truncatedWindow x m (n - 3)) V (gradField V) ∧ Support.HolderSeminormBoundOn (truncatedWindow x m (n - 3)) (1 / 2) K (gradField V) ∧ K ≤ boundarySchauderConst d * (3 ^ (-n)) ^ (1 / 2) * (3 ^ (-(n - 2)) * Support.affineExcessRaw (reflectedWindow x m (n - 2)) V)

The Schauder gradient-Hölder estimate, boundary branch — the producer, raw form.

For V classically harmonic on the partially reflected window reflectedWindow x m (n-2), the gradient field gradField V realizes the four slots hint / hgrad / hhol / hschauder of OneStepConditional.excessDecay_oneStep_of_harmonicApprox, with

  Csch = boundarySchauderConst d

and the right-hand side read at the unnormalized excess minimum on the reflected window. No interior hypothesis, and no restriction on the met set.

4. The producer at the reflected window's own normalizer