Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section4.Provider.ExcessDecay.OneStepSchauderWindow

OneStepSchauderWindow #

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

The interior gap: instantiating the Schauder atom at the §4 windows #

OneStepSchauderInterior.gradField_holderHalf_of_harmonic is stated for an abstract convex window W inside an enveloping window W₂. Here it is instantiated at the §4 pair

  W  = (x + □_{n-3}) ∩ □_m ,    W₂ = (x + □_{n-2}) ∩ □_m ,

on the interior branch, i.e. under the hypothesis x + □_{n-2} ⊆ □_m (the replacement cube is a full translated cube, so W₂ = x + □_{n-2}), which is the branch on which the boundary datum contributes nothing.

The interior gap, quantified #

For p ∈ W the sup-distance from p to ∂(x + □_{n-2}) is at least

  (3^{n-2} − 3^{n-3}) / 2  =  3^{n-3} ,

one full triadic scale. Taking R := 3^{n-3}/2 therefore gives euclideanBall p R ⊆ Metric.ball p R ⊆ x + □_{n-2} for every p ∈ W, with a factor-2 margin. This is the ball family the atom consumes; note that a single ball centred at x would not do (see OneStepSchauderInterior).

The volume ratio #

  |euclideanBall p (R/2)| ≥ ((R/2)/(d+1))^d = (3^{n-3}/(4(d+1)))^d ,

so the ratio is bounded by the scale-free constant (12(d+1))^d.

The resulting constant #

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

schauderConst d = d · C_native(d) being the constant of the transplanted native interior Hessian estimate. The bound produced is

  [∇v]_{C^{0,1/2}(W)} ≤ Csch(d) · (3^{-n})^{1/2} · E(v, W₂) ,

i.e. exactly the Schauder display with K_h = 0 — the interior branch carries no boundary-datum contribution.

1. The ball family inside the enveloping window #

source
theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.metricBall_subset_truncatedWindow_of_interior {d : ℕ} {x : HCPolySupport.Vec d} {m n : ℤ} (hcube : (fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2)) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) {p : HCPolySupport.Vec d} (hp : p ∈ truncatedWindow x m (n - 3)) :
Metric.ball p (3 ^ (n - 3) / 2) ⊆ truncatedWindow x m (n - 2)

The interior gap. On the interior branch every point of the window at scale n-3 carries a sup-ball of radius 3^{n-3}/2 inside the replacement cube at scale n-2.

source
theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.euclideanBall_subset_truncatedWindow_of_interior {d : ℕ} {x : HCPolySupport.Vec d} {m n : ℤ} (hcube : (fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2)) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) {p : HCPolySupport.Vec d} (hp : p ∈ truncatedWindow x m (n - 3)) {rho : ℝ} (hrho : 0 < rho) (hle : rho ≤ 3 ^ (n - 3) / 2) :
HCPolySupport.euclideanBall p rho ⊆ truncatedWindow x m (n - 2)
source
theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.metricBall_toEuc_subset_image_of_interior {d : ℕ} {x : HCPolySupport.Vec d} {m n : ℤ} (hcube : (fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2)) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) {p : HCPolySupport.Vec d} (hp : p ∈ truncatedWindow x m (n - 3)) :
Metric.ball (toEuc p) (3 ^ (n - 3) / 2) ⊆ ⇑toEuc '' truncatedWindow x m (n - 2)

The toEuc-image form of the ball family, as the atom consumes it.

2. The volume of the Euclidean ball, from below #

source
theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.volume_toReal_euclideanBall_ge {d : ℕ} (p : HCPolySupport.Vec d) {rho : ℝ} (hrho : 0 < rho) :
(rho / (↑d + 1)) ^ d ≤ (MeasureTheory.volume (HCPolySupport.euclideanBall p rho)).toReal

A scale-free lower bound for the Euclidean ball volume. CoarseGraining's conservative inclusion closedBall p (ρ/(2(d+1))) ⊆ euclideanBall p ρ and the product-measure formula give |euclideanBall p ρ| ≥ (ρ/(d+1))^d.

3. The scale-free volume ratio #

source
noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.schauderRatioConst (d : ℕ) :
ℝ

The ratio constant of the interior gap: √((12(d+1))^d).

Equations
Instances For
    source
    theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.schauderRatioConst_nonneg (d : ℕ) :
    0 ≤ schauderRatioConst d
    source
    theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.sqrt_volume_ratio_le {d : ℕ} {x : HCPolySupport.Vec d} {m n : ℤ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hnm : n - 3 ≤ m) (p : HCPolySupport.Vec d) :
    √((MeasureTheory.volume (truncatedWindow x m (n - 2))).toReal / (MeasureTheory.volume (HCPolySupport.euclideanBall p (3 ^ (n - 3) / 2 / 2))).toReal) ≤ schauderRatioConst d

    The volume ratio is scale free. On the interior branch the ratio of the enveloping window's volume to the volume of any of the atom's balls is at most (12(d+1))^d, independently of n.

    4. The window diameter #

    source
    theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.norm_sub_le_of_mem_truncatedWindow_pair {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {p q : HCPolySupport.Vec d} (hp : p ∈ truncatedWindow x m k) (hq : q ∈ truncatedWindow x m k) :
    ‖p - q‖ ≤ 3 ^ k