Geometry

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

Geometry for the exponentially weighted estimates

The weighted estimates need two explicit smooth objects: a localization with a quantitative coordinate-gradient bound, and a phase with unit coordinate gradient comparable to the distance from a point.

The localization is the smooth ball cutoff of the cutoff layer, whose operator-norm gradient bound is converted here into the coordinate form the weighted estimate consumes.

Two phases are supplied. The outward phase is the regularized radius radialPhase z delta x = sqrt (|x - z| ^ 2 + delta ^ 2) - delta, which is smooth everywhere, has coordinate gradient of length at most one, and differs from |x - z| by at most delta; it increases away from z, so it measures decay away from a ball or cube around z. The inward phase is its negative, inwardPhase z delta = -radialPhase z delta, which increases towards z, so it measures decay from the inscribed radius of a cube centred at z.

Each phase comes with the two comparisons the pointwise estimate consumes. For the outward phase, a transition layer inside {y : |y - z| <= s} admits tA := s, and a point x with a ball of radius rho around it admits tx := |x - z| - rho - delta, so tx - tA is the distance from x to the layer up to rho + delta. For the inward phase, a transition layer inside {y : R <= |y - z|} admits tA := -R + delta and the same point admits tx := -(|x - z| + rho), so tx - tA is R - |x - z| up to rho + delta.

Main results

• DivergenceFormProcess.Decay.vecNormSq_fderiv_le_of_norm_fderiv_le
• DivergenceFormProcess.Decay.vecNormSq_fderiv_ballCutoff_le
• DivergenceFormProcess.Decay.contDiff_radialPhase
• DivergenceFormProcess.Decay.vecNormSq_fderiv_radialPhase_le_one
• DivergenceFormProcess.Decay.radialPhase_bounds
• DivergenceFormProcess.Decay.le_euclideanNorm_sub_of_notMem_euclideanBall
• DivergenceFormProcess.Decay.contDiff_inwardPhase
• DivergenceFormProcess.Decay.vecNormSq_fderiv_inwardPhase_le_one
• DivergenceFormProcess.Decay.inwardPhase_le_of_le_euclideanNorm
• DivergenceFormProcess.Decay.le_inwardPhase_of_mem_euclideanBall

theorem DivergenceFormProcess.Decay.vecNormSq_fderiv_le_of_norm_fderiv_le {d : ℕ} {f : HCPolySupport.Vec d → ℝ} {C : ℝ} (hC : 0 ≤ C) {x : HCPolySupport.Vec d} (h : ‖fderiv ℝ f x‖ ≤ C) : (HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ f x) (HCPolySupport.basisVec i)) ≤ ↑d * C ^ 2

An operator-norm bound on the derivative gives the coordinate bound the weighted estimates consume.

theorem DivergenceFormProcess.Decay.vecNormSq_fderiv_ballCutoff_le {d : ℕ} (x₀ : HCPolySupport.Vec d) {r s : ℝ} (hr : 0 < r) (hrs : r < s) (x : HCPolySupport.Vec d) : (HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ (HCPolySupport.QuantitativeBallCutoff.canonicalFun x₀ r s) x) (HCPolySupport.basisVec i)) ≤ ↑d * (HCPolySupport.smoothTransitionProfile.derivBound * (2 * ↑d / (s - r))) ^ 2

Coordinate gradient bound for the smooth ball cutoff.

def DivergenceFormProcess.Decay.radialSq {d : ℕ} (z : HCPolySupport.Vec d) (delta : ℝ) (x : HCPolySupport.Vec d) : ℝ

The regularized radius about a point.

Equations

• DivergenceFormProcess.Decay.radialSq z delta x = HCPolySupport.vecNormSq (x - z) + delta ^ 2

noncomputable def DivergenceFormProcess.Decay.radialPhase {d : ℕ} (z : HCPolySupport.Vec d) (delta : ℝ) (x : HCPolySupport.Vec d) : ℝ

The smooth phase used by the exponential weight: the regularized radius, normalized to vanish at the centre.

Equations

• DivergenceFormProcess.Decay.radialPhase z delta x = √(DivergenceFormProcess.Decay.radialSq z delta x) - delta

theorem DivergenceFormProcess.Decay.radialSq_pos {d : ℕ} {z : HCPolySupport.Vec d} {delta : ℝ} (hdelta : 0 < delta) (x : HCPolySupport.Vec d) : 0 < radialSq z delta x

The regularized squared radius is bounded below by the regularization.

theorem DivergenceFormProcess.Decay.hasFDerivAt_radialSq {d : ℕ} {z : HCPolySupport.Vec d} {delta : ℝ} (x : HCPolySupport.Vec d) : HasFDerivAt (radialSq z delta) (∑ i : Fin d, (2 * (x i - z i)) • ContinuousLinearMap.proj i) x

The regularized squared radius has the expected derivative.

theorem DivergenceFormProcess.Decay.contDiff_radialPhase {d : ℕ} {z : HCPolySupport.Vec d} {delta : ℝ} (hdelta : 0 < delta) : ContDiff ℝ (↑⊤) (radialPhase z delta)

The regularized radius is smooth.

theorem DivergenceFormProcess.Decay.vecNormSq_fderiv_radialPhase_le_one {d : ℕ} {z : HCPolySupport.Vec d} {delta : ℝ} (hdelta : 0 < delta) (x : HCPolySupport.Vec d) : (HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ (radialPhase z delta) x) (HCPolySupport.basisVec i)) ≤ 1

The coordinate gradient of the regularized radius has length at most one.

theorem DivergenceFormProcess.Decay.radialPhase_bounds {d : ℕ} {z : HCPolySupport.Vec d} {delta : ℝ} (hdelta : 0 < delta) (x : HCPolySupport.Vec d) : 0 ≤ radialPhase z delta x ∧ HCPolySupport.euclideanNorm (x - z) - delta ≤ radialPhase z delta x ∧ radialPhase z delta x ≤ HCPolySupport.euclideanNorm (x - z)

The regularized radius is nonnegative and brackets the Euclidean distance.

theorem DivergenceFormProcess.Decay.euclideanNorm_sub_lt_of_mem_euclideanBall {d : ℕ} {x y : HCPolySupport.Vec d} {rho : ℝ} (hrho : 0 ≤ rho) (hy : y ∈ HCPolySupport.euclideanBall x rho) : HCPolySupport.euclideanNorm (y - x) < rho

A point of a Euclidean ball is within the radius of the centre.

theorem DivergenceFormProcess.Decay.le_euclideanNorm_sub_of_notMem_euclideanBall {d : ℕ} {x y : HCPolySupport.Vec d} {rho : ℝ} (hy : y ∉ HCPolySupport.euclideanBall x rho) : rho ≤ HCPolySupport.euclideanNorm (y - x)

A point outside a Euclidean ball is at least the radius from the centre. This is the form the transition-layer hypothesis consumes when the layer is read off as the complement of an inner ball.

noncomputable def DivergenceFormProcess.Decay.inwardPhase {d : ℕ} (z : HCPolySupport.Vec d) (delta : ℝ) (x : HCPolySupport.Vec d) : ℝ

The inward phase about a centre: the negative of the regularized radius. It increases towards the centre, so it measures decay from the inscribed radius of a region centred there.

Equations

• DivergenceFormProcess.Decay.inwardPhase z delta x = -DivergenceFormProcess.Decay.radialPhase z delta x

theorem DivergenceFormProcess.Decay.contDiff_inwardPhase {d : ℕ} {z : HCPolySupport.Vec d} {delta : ℝ} (hdelta : 0 < delta) : ContDiff ℝ (↑⊤) (inwardPhase z delta)

The inward phase is smooth.

theorem DivergenceFormProcess.Decay.vecNormSq_fderiv_inwardPhase_le_one {d : ℕ} {z : HCPolySupport.Vec d} {delta : ℝ} (hdelta : 0 < delta) (x : HCPolySupport.Vec d) : (HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ (inwardPhase z delta) x) (HCPolySupport.basisVec i)) ≤ 1

The coordinate gradient of the inward phase has length at most one.

theorem DivergenceFormProcess.Decay.inwardPhase_le_of_le_euclideanNorm {d : ℕ} {z : HCPolySupport.Vec d} {delta : ℝ} (hdelta : 0 < delta) {R : ℝ} {y : HCPolySupport.Vec d} (hy : R ≤ HCPolySupport.euclideanNorm (y - z)) : inwardPhase z delta y ≤ -R + delta

Beyond radius R the inward phase is at most -R + delta, which is the form the transition-layer hypothesis consumes.

theorem DivergenceFormProcess.Decay.le_inwardPhase_of_mem_euclideanBall {d : ℕ} {z : HCPolySupport.Vec d} {delta : ℝ} (hdelta : 0 < delta) {x y : HCPolySupport.Vec d} {rho : ℝ} (hrho : 0 ≤ rho) (hy : y ∈ HCPolySupport.euclideanBall x rho) : -(HCPolySupport.euclideanNorm (x - z) + rho) ≤ inwardPhase z delta y

On a ball of radius rho about x the inward phase is at least -(euclideanNorm (x - z) + rho), which is the form the near-point hypothesis consumes.