CubeSchauderSlope

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

Cube Schauder: the vector slope comparison of two nested windows

CubeSchauderCampanato.affineExcess_le_campanato controls the excess of the zero-datum solution on every truncated window. Converting that Campanato bound into a pointwise statement about the gradient needs the slopes of the affine minimizers to form a Cauchy family, and for that the vector difference g − g' must be controlled, not merely the difference of magnitudes |‖g‖ − ‖g'‖| that ExcessDecay.SlopeStability exports.

The proved proof of slopeStability_of_axisCubeSandwich produces the vector bound internally and then discards it in its very last step (the reverse triangle inequality). This module re-derives the strictly stronger statement, in a two-window form that additionally allows the two windows to have different centres — which is what the two-point Hölder estimate needs:

  |∇ℓ(u,W) − ∇ℓ(u,W')| ≤ c₀(θ)⁻¹ · (E(u,W') + κ · E(u,W))   for W' ⊆ W .

The two ingredients are exactly the two proved halves of e.grad.stability: normalizedL2On_affineEval_sub_le (Minkowski plus the volume ratio) and normalizedL2On_affineEval_ge_of_sandwich (the exact cube second moment). Nothing new is proved about either.

Main results

• slopeMagnitude_sub_le_of_sandwich — the abstract two-window vector bound.
• affineMinimizerPair / windowSlope — the canonical minimizer choice, indexed by the window set so that equal windows get equal slopes.
• slopeMagnitude_windowSlope_sub_le — the bound on truncated windows, at the scale-free constant slopeStabilityConst d (1/9) (volumeRatioConstTriadic d).

References

• ABK26, (e.grad.stability); Armstrong--Kuusi, Elliptic Regularity, Proposition p.Schauder.C1alpha.

1. The rpow bookkeeping

2. The abstract two-window vector bound

theorem Algsuperdiff.Section4.Provider.Schauder.slopeMagnitude_sub_le_of_sandwich {d : ℕ} (hd : 0 < d) {W W' : Set (HCPolySupport.Vec d)} {u : HCPolySupport.Vec d → ℝ} {c c' : ℝ} {g g' zin' zout' zout : HCPolySupport.Vec d} {Lin' Lout' Lout θ κ : ℝ} (hLin' : 0 < Lin') (hLout' : 0 < Lout') (hLout : 0 < Lout) (hθ0 : 0 < θ) (hθ : θ * Lout' ≤ Lin') (hin' : HCPolySupport.axisCube zin' Lin' ⊆ W') (hout' : W' ⊆ HCPolySupport.axisCube zout' Lout') (hout : W ⊆ HCPolySupport.axisCube zout Lout) (hsub : W' ⊆ W) (hWpos : 0 < (MeasureTheory.volume W).toReal) (hmeasW : MeasurableSet W) (hmeas' : MeasurableSet W') (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict W)) (hratio : ((MeasureTheory.volume W).toReal / (MeasureTheory.volume W').toReal) ^ ((↑d)⁻¹ + 1 / 2) ≤ κ) (hmin : Support.IsAffineMinimizer W u c g) (hmin' : Support.IsAffineMinimizer W' u c' g') : Support.slopeMagnitude (g - g') ≤ (ExcessDecay.ndConst d θ)⁻¹ * (Support.affineExcess W' u + κ * Support.affineExcess W u)

The vector slope comparison of two nested windows.

If (c,g) minimizes the affine deviation of u on W, (c',g') minimizes it on W' ⊆ W, W' carries an aspect-θ cube sandwich and W sits inside a cube, then

  |g − g'| ≤ c₀(θ)⁻¹ · (E(u,W') + κ · E(u,W)) ,

with κ any bound for the volume-ratio power (|W|/|W'|)^{1/d+1/2}.

This is slopeStability_of_axisCubeSandwich's chain stopped one step early: the proved statement applies the reverse triangle inequality | ‖g‖ − ‖g'‖ | ≤ ‖g − g'‖ at the end and so exports only the weaker scalar form. Neither window has to be centred at the same point.

3. The canonical minimizer of a window

noncomputable def Algsuperdiff.Section4.Provider.Schauder.affineMinimizerPair {d : ℕ} (W : Set (HCPolySupport.Vec d)) (u : HCPolySupport.Vec d → ℝ) : ℝ × HCPolySupport.Vec d

The canonical affine minimizer of u on W, indexed by the set W.

Indexing by the set (rather than by a centre/scale pair) is what makes affineMinimizerPair_congr available: two truncated windows that happen to be the same set get the same minimizer, which is exactly what the far-apart case of the two-point Hölder estimate uses.

Equations

• Algsuperdiff.Section4.Provider.Schauder.affineMinimizerPair W u = Classical.epsilon fun (p : ℝ × HCPolySupport.Vec d) => Algsuperdiff.Section4.Support.IsAffineMinimizer W u p.1 p.2

theorem Algsuperdiff.Section4.Provider.Schauder.isAffineMinimizer_affineMinimizerPair {d : ℕ} {W : Set (HCPolySupport.Vec d)} {u : HCPolySupport.Vec d → ℝ} (h : ∃ (p : ℝ × HCPolySupport.Vec d), Support.IsAffineMinimizer W u p.1 p.2) : Support.IsAffineMinimizer W u (affineMinimizerPair W u).1 (affineMinimizerPair W u).2

noncomputable def Algsuperdiff.Section4.Provider.Schauder.windowSlope {d : ℕ} (m : ℤ) (u : HCPolySupport.Vec d → ℝ) (x : HCPolySupport.Vec d) (k : ℤ) : HCPolySupport.Vec d

The slope of the canonical minimizer on the truncated window (x+□_k) ∩ □_m.

Equations

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

theorem Algsuperdiff.Section4.Provider.Schauder.isAffineMinimizer_windowSlope {d : ℕ} {m k : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k - 1 ≤ m) {u : HCPolySupport.Vec d → ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (ExcessDecay.truncatedWindow x m k))) : Support.IsAffineMinimizer (ExcessDecay.truncatedWindow x m k) u (affineMinimizerPair (ExcessDecay.truncatedWindow x m k) u).1 (windowSlope m u x k)

4. The bound on truncated windows

theorem Algsuperdiff.Section4.Provider.Schauder.volume_ratio_truncatedWindow_pair_le {d : ℕ} {m k l : ℤ} {x y : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hy : y ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k - 1 ≤ m) (hlm : l - 1 ≤ m) (hlk : l ≤ k + 1) : (MeasureTheory.volume (ExcessDecay.truncatedWindow x m l)).toReal / (MeasureTheory.volume (ExcessDecay.truncatedWindow y m k)).toReal ≤ 3 ^ (3 * d)

The volume ratio of two truncated windows whose scales differ by at most one is at most the triadic constant 3^{3d}.

theorem Algsuperdiff.Section4.Provider.Schauder.slopeMagnitude_windowSlope_sub_le {d : ℕ} (hd : 0 < d) {m k l : ℤ} {x y : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hy : y ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k - 1 ≤ m) (hlm : l - 1 ≤ m) (hlk : l ≤ k + 1) (hsub : ExcessDecay.truncatedWindow y m k ⊆ ExcessDecay.truncatedWindow x m l) {u : HCPolySupport.Vec d → ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (ExcessDecay.truncatedWindow x m l))) : Support.slopeMagnitude (windowSlope m u x l - windowSlope m u y k) ≤ ExcessDecay.slopeStabilityConst d (1 / 9) (ExcessDecay.volumeRatioConstTriadic d) * (Support.affineExcess (ExcessDecay.truncatedWindow y m k) u + Support.affineExcess (ExcessDecay.truncatedWindow x m l) u)

The vector slope comparison on truncated windows.

For base points x, y ∈ □_m and scales l ≤ k + 1 with (y+□_k) ∩ □_m ⊆ (x+□_l) ∩ □_m,

  |∇ℓ(u,W_k(y)) − ∇ℓ(u,W_l(x))|
      ≤ C_stab(d) · (E(u,W_k(y)) + E(u,W_l(x))) ,

with C_stab(d) = slopeStabilityConst d (1/9) (volumeRatioConstTriadic d), the proved scale-free constant of e.grad.stability.