TailLocalization

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

Localization and local energy for the resolvent tail estimate

The tail estimate for mu z - div (a grad z) = g at a point x whose source vanishes on the ball of radius r about x uses one fixed localization: the smooth radial cutoff agmonTailCutoff x r, equal to one on the ball of radius 3 r / 4 and supported inside the ball of radius r. Its transition layer therefore sits entirely inside the region where the source vanishes, which is what makes the estimate decay away from the source.

Two quantitative facts about that localization are recorded, both with the scaling the tail function needs: the coordinate-gradient bound agmonTailCutoffGradientBound d r, which scales like r ^ (-2), and the volume bound agmonTailLayerVolume d r for the transition layer, which scales like r ^ d.

The local energy is then paid for entirely by that layer. Testing the equation with eta ^ 2 * z gives a Caccioppoli inequality in which the source term drops (the source vanishes where eta does not) and the mass term has a good sign, so the gradient energy on the ball of radius r / 2 is bounded by the layer term alone. With the maximum-principle bound |z| <= 1 / mu this produces agmonTailGradientSize d lam Lam mu r, the gradient size the interior Schauder estimate consumes.

The first two results convert an integral bound on the squared Euclidean magnitude of a vector field into a bound on the L^2 size the Schauder estimate is stated with.

Main results

• DivergenceFormProcess.Decay.vectorLpSizeOn_two_le
• DivergenceFormProcess.Decay.agmonTailCutoff
• DivergenceFormProcess.Decay.vecNormSq_fderiv_agmonTailCutoff_le
• DivergenceFormProcess.Decay.volume_layer_agmonTailCutoff_le

The Euclidean L² size of a vector field

theorem DivergenceFormProcess.Decay.memLp_euclideanNorm {d : ℕ} {W : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : HCPolySupport.MemVectorL2 W f) : MeasureTheory.MemLp (fun (y : HCPolySupport.Vec d) => HCPolySupport.euclideanNorm (f y)) 2 (HCPolySupport.volumeMeasureOn W)

The Euclidean magnitude of an L² vector field is a scalar L² function.

theorem DivergenceFormProcess.Decay.vectorLpSizeOn_two_le {d : ℕ} {W : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} {E : ℝ} (hf : HCPolySupport.MemVectorL2 W f) (hE : 0 ≤ E) (hint : ∫ (y : HCPolySupport.Vec d) in W, HCPolySupport.vecNormSq (f y) ≤ E ^ 2) : Algsuperdiff.StochasticProcess.Common.Regularity.Ported.vectorLpSizeOn W 2 f ≤ E

An integral bound on the squared Euclidean magnitude is a bound on the L² size the Schauder estimate consumes.

The localization

noncomputable def DivergenceFormProcess.Decay.agmonTailCutoff {d : ℕ} (x : HCPolySupport.Vec d) (r : ℝ) : HCPolySupport.Vec d → ℝ

The localization of the tail estimate: one on the ball of radius 3 r / 4 about x, supported inside the ball of radius r.

Equations

• DivergenceFormProcess.Decay.agmonTailCutoff x r = HCPolySupport.QuantitativeBallCutoff.canonicalFun x (3 * r / 4) (7 * r / 8)

theorem DivergenceFormProcess.Decay.contDiff_agmonTailCutoff {d : ℕ} (x : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) : ContDiff ℝ (↑⊤) (agmonTailCutoff x r)

theorem DivergenceFormProcess.Decay.hasCompactSupport_agmonTailCutoff {d : ℕ} (x : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) : HasCompactSupport (agmonTailCutoff x r)

theorem DivergenceFormProcess.Decay.tsupport_agmonTailCutoff_subset {d : ℕ} (x : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) : tsupport (agmonTailCutoff x r) ⊆ HCPolySupport.euclideanBall x r

theorem DivergenceFormProcess.Decay.agmonTailCutoff_eq_one {d : ℕ} (x : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) {y : HCPolySupport.Vec d} (hy : y ∈ HCPolySupport.euclideanBall x (3 * r / 4)) : agmonTailCutoff x r y = 1

noncomputable def DivergenceFormProcess.Decay.agmonTailCutoffGradientBound (d : ℕ) (r : ℝ) : ℝ

The coordinate-gradient bound of the tail localization: it scales like r⁻².

Equations

• DivergenceFormProcess.Decay.agmonTailCutoffGradientBound d r = ↑d * (HCPolySupport.smoothTransitionProfile.derivBound * (2 * ↑d / (r / 8))) ^ 2

theorem DivergenceFormProcess.Decay.agmonTailCutoffGradientBound_nonneg (d : ℕ) (r : ℝ) : 0 ≤ agmonTailCutoffGradientBound d r

theorem DivergenceFormProcess.Decay.vecNormSq_fderiv_agmonTailCutoff_le {d : ℕ} (x : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) (y : HCPolySupport.Vec d) : (HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ (agmonTailCutoff x r) y) (HCPolySupport.basisVec i)) ≤ agmonTailCutoffGradientBound d r

theorem DivergenceFormProcess.Decay.le_euclideanNorm_of_fderiv_agmonTailCutoff_ne_zero {d : ℕ} (x : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) {y : HCPolySupport.Vec d} (hy : fderiv ℝ (agmonTailCutoff x r) y ≠ 0) : 3 * r / 4 ≤ HCPolySupport.euclideanNorm (y - x)

The transition layer of the tail localization sits outside the ball of radius 3 r / 4.

noncomputable def DivergenceFormProcess.Decay.agmonTailLayerVolume (d : ℕ) (r : ℝ) : ℝ

The volume bound for the transition layer of the tail localization: it scales like r ^ d.

Equations

• DivergenceFormProcess.Decay.agmonTailLayerVolume d r = (MeasureTheory.volume (Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastUnitBall d)).toReal * r ^ d

theorem DivergenceFormProcess.Decay.agmonTailLayerVolume_nonneg (d : ℕ) {r : ℝ} (hr : 0 ≤ r) : 0 ≤ agmonTailLayerVolume d r

theorem DivergenceFormProcess.Decay.volume_layer_agmonTailCutoff_le {d : ℕ} [NeZero d] (x : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) (Om : Set (HCPolySupport.Vec d)) : (MeasureTheory.volume {y : HCPolySupport.Vec d | y ∈ Om ∧ fderiv ℝ (agmonTailCutoff x r) y ≠ 0}).toReal ≤ agmonTailLayerVolume d r

The local energy bound

noncomputable def DivergenceFormProcess.Decay.agmonTailGradientSize (d : ℕ) (lam Lam mu r : ℝ) : ℝ

The local gradient size supplied to the Schauder estimate: the Caccioppoli bound at the tail localization, read off on the ball of radius r / 2.

Equations

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

theorem DivergenceFormProcess.Decay.agmonTailGradientSize_nonneg (d : ℕ) {lam Lam mu r : ℝ} (hlam : 0 < lam) (hLam : 0 < Lam) (hmu : 0 < mu) : 0 ≤ agmonTailGradientSize d lam Lam mu r