OneStepSchauderProducer

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

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

This module produces, for a competitor v harmonic on the replacement window (x + □_{n-2}) ∩ □_m of the interior branch, exactly the four-hypothesis package that OneStepConditional.excessDecay_oneStep_of_harmonicApprox consumes in its hint / hgrad / hhol / hschauder slots:

  Gv := gradField v ,
  ∀ i, IntegrableOn (fun p => Gv p i) ((x + □_{n-3}) ∩ □_m) ,
  HasGradientOn ((x + □_{n-3}) ∩ □_m) v Gv ,
  HolderSeminormBoundOn ((x + □_{n-3}) ∩ □_m) (1/2) K Gv ,
  K ≤ Csch(d) · (3^{-n})^{1/2} · E(v, (x + □_{n-2}) ∩ □_m)  +  0 ,

with

  Csch(d) = schauderWindowConst d
          = 48 · 3^{3/2} · schauderConst d · √((12(d+1))^d) ,
  schauderConst d = d · C_native(d) ,

C_native(d) the constant of the transplanted native interior Hessian estimate interiorSecondDerivEstimateL2_ball. The boundary-datum contribution is K_h = 0: on the interior branch the replacement window is a full translated cube and no face of ∂□_m is met.

What the harmonicity hypothesis is

hharm : HarmonicOnNhd (v ∘ toEuc.symm) (toEuc '' ((x + □_{n-2}) ∩ □_m)) — the classical predicate. For the competitor produced by ResidualCorrectorExistence.exists_weaklyHarmonicOn_of_datum (which satisfies the variational Support.IsWeaklyHarmonicOn), the Weyl bridge of OneStepSchauderWeyl supplies this for every CoarseGraining convex smoothing of the competitor, at the full radius.

1. The constant

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

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

Equations

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

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

2. The scale arithmetic

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sqrt_zpow_div_self (n : ℤ) : √(3 ^ (n - 3)) / 3 ^ (n - 3) = 3 ^ (3 / 2) * (3 ^ (-n)) ^ (1 / 2)

3. Differentiability and integrability of the gradient field

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.hasGradientOn_gradField {d : ℕ} {v : HCPolySupport.Vec d → ℝ} {S : Set (EuclideanSpace ℝ (Fin d))} {W : Set (HCPolySupport.Vec d)} (hharm : InnerProductSpace.HarmonicOnNhd (v ∘ ⇑toEuc.symm) S) (hWS : ∀ p ∈ W, toEuc p ∈ S) : Support.HasGradientOn W v (gradField v)

The gradient field realizes HasGradientOn.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.continuousOn_gradField_coord {d : ℕ} {v : HCPolySupport.Vec d → ℝ} {S : Set (EuclideanSpace ℝ (Fin d))} {W : Set (HCPolySupport.Vec d)} (hharm : InnerProductSpace.HarmonicOnNhd (v ∘ ⇑toEuc.symm) S) (hWS : ∀ p ∈ W, toEuc p ∈ S) (i : Fin d) : ContinuousOn (fun (p : HCPolySupport.Vec d) => gradField v p i) W

The coordinates of the gradient field are continuous on a window of harmonicity.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.integrableOn_gradField_coord {d : ℕ} {v : HCPolySupport.Vec d → ℝ} {W : Set (HCPolySupport.Vec d)} {K D : ℝ} (hWmeas : MeasurableSet W) (hWfin : MeasureTheory.volume W ≠ ⊤) (hK : 0 ≤ K) (hcont : ∀ (i : Fin d), ContinuousOn (fun (p : HCPolySupport.Vec d) => gradField v p i) W) (hhol : Support.HolderSeminormBoundOn W (1 / 2) K (gradField v)) (hdiam : ∀ p ∈ W, ∀ q ∈ W, ‖p - q‖ ≤ D) {p₀ : HCPolySupport.Vec d} (hp₀ : p₀ ∈ W) (i : Fin d) : MeasureTheory.IntegrableOn (fun (p : HCPolySupport.Vec d) => gradField v p i) W MeasureTheory.volume

The gradient field is integrable coordinatewise on a bounded window on which it satisfies a Hölder bound.

4. The producer

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.exists_gradientHolder_interior {d : ℕ} [NeZero d] (hd : d ≠ 0) {m n : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hnm : n - 3 ≤ m) (hcube : (fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2)) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) {v : HCPolySupport.Vec d → ℝ} (hharm : InnerProductSpace.HarmonicOnNhd (v ∘ ⇑toEuc.symm) (⇑toEuc '' truncatedWindow 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) (truncatedWindow 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 ≤ schauderWindowConst d * (3 ^ (-n)) ^ (1 / 2) * Support.affineExcess (truncatedWindow x m (n - 2)) v + 0

The Schauder gradient-Hölder estimate, interior branch — the producer.

For v harmonic on the replacement window (x + □_{n-2}) ∩ □_m of the interior branch (x + □_{n-2} ⊆ □_m), the gradient field gradField v realizes the four slots hint / hgrad / hhol / hschauder of OneStepConditional.excessDecay_oneStep_of_harmonicApprox, with

  Csch = schauderWindowConst d ,   K_h = 0 .