ResolventTail

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

Displacement tails from resolvent tail decay

For a divergence-form generator with rough coefficients the estimate an analysis produces is a decay of the RESOLVENT away from the region carrying the datum, not a bound on the transition law. This file turns the first into the second.

The hypothesis is SubMarkovKernelSemigroup.HasResolventTail: at a positive shift lam, the normalized lam-potential measure of the complement of the ball of radius rho about the starting point is at most phi (sqrt lam * rho), with sqrt lam * rho the parabolic scaling of the radius. The conclusion (PositiveC0ContractiveResolvent.measure_compl_ball_le_of_hasResolventTail) is that at the time t = 1 / lam the transition law leaves the ball of radius 4 r with probability at most 2 * exp 1 * phi (sqrt lam * r).

The proof is the excessive-function comparison of Blumenthal--Getoor. Let g be a radial cutoff vanishing on the ball of radius r and equal to one outside the ball of radius 2 r, transported to the one-point compactification by the value one at the added point, so that it becomes an observable vanishing at infinity there. Then v = 2 lam R_lam g is lam-excessive (PositiveC0ContractiveResolvent.mul_operator_smul_operator_le), so the exponential comparison of Semigroup/ExponentialComparison.lean bounds the transition average of any observable below v by exp 1 times v at the starting point. Tail decay at radius r about a point at distance at least 3 r makes v at least one there, and tail decay at radius r about the starting point, together with conservativity, makes v at the starting point at most 2 phi (sqrt lam * r).

The state space is a proper metric space, so that the radial cutoffs have compact support; both a compact state space and a Euclidean one are covered. No analytic estimate for a particular generator is asserted here: the tail decay is the consumer's hypothesis.

noncomputable def Algsuperdiff.Process.radialCutoff {X : Type u_1} [MetricSpace X] (x : X) (a b : ℝ) (z : X) : ℝ

The radial cutoff about x: one on the closed ball of radius a, zero outside the ball of radius b, and affine in the distance in between.

Equations

• Algsuperdiff.Process.radialCutoff x a b z = min 1 (max 0 ((b - dist z x) / (b - a)))

theorem Algsuperdiff.Process.radialCutoff_nonneg {X : Type u_1} [MetricSpace X] (x : X) (a b : ℝ) (z : X) : 0 ≤ radialCutoff x a b z

The radial cutoff is nonnegative.

theorem Algsuperdiff.Process.radialCutoff_le_one {X : Type u_1} [MetricSpace X] (x : X) (a b : ℝ) (z : X) : radialCutoff x a b z ≤ 1

The radial cutoff is at most one.

theorem Algsuperdiff.Process.radialCutoff_eq_one {X : Type u_1} [MetricSpace X] {x : X} {a b : ℝ} (hab : a < b) {z : X} (hz : dist z x ≤ a) : radialCutoff x a b z = 1

The radial cutoff is one on the inner ball.

theorem Algsuperdiff.Process.radialCutoff_eq_zero {X : Type u_1} [MetricSpace X] {x : X} {a b : ℝ} (hab : a < b) {z : X} (hz : b ≤ dist z x) : radialCutoff x a b z = 0

The radial cutoff vanishes outside the outer ball.

theorem Algsuperdiff.Process.continuous_radialCutoff {X : Type u_1} [MetricSpace X] (x : X) (a b : ℝ) : Continuous (radialCutoff x a b)

The radial cutoff is continuous.

noncomputable def Algsuperdiff.Process.radialCutoffC0 {X : Type u_1} [MetricSpace X] [ProperSpace X] (x : X) (a b : ℝ) (hab : a < b) : ZeroAtInftyContinuousMap X ℝ

The radial cutoff as a continuous function vanishing at infinity.

Equations

• Algsuperdiff.Process.radialCutoffC0 x a b hab = { toFun := Algsuperdiff.Process.radialCutoff x a b, continuous_toFun := ⋯, zero_at_infty' := ⋯ }

@[simp]

theorem Algsuperdiff.Process.radialCutoffC0_apply {X : Type u_1} [MetricSpace X] [ProperSpace X] (x : X) (a b : ℝ) (hab : a < b) (z : X) : (radialCutoffC0 x a b hab) z = radialCutoff x a b z

The bundled radial cutoff has the values of the radial cutoff.

def Algsuperdiff.Process.SubMarkovKernelSemigroup.HasResolventTail {X : Type u_1} [MetricSpace X] [MeasurableSpace X] (P : MarkovProcess.SubMarkovKernelSemigroup X) (lam : ℝ) (phi : ℝ → ℝ) : Prop

Resolvent tail decay at a positive shift lam, with profile phi: at every starting point the normalized lam-potential measure of the complement of a ball centred there is at most phi evaluated at the natural scaling sqrt lam * rho of the radius.

Equations

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

theorem Algsuperdiff.Process.PositiveC0ContractiveResolvent.mul_operator_smul_operator_le {Y : Type u_1} [TopologicalSpace Y] (R : MarkovProcess.PositiveC0ContractiveResolvent Y) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {g : ZeroAtInftyContinuousMap Y ℝ} (hg : ∀ (z : Y), 0 ≤ g z) {c : ℝ} (hc : 0 ≤ c) (nu : ↑MarkovProcess.Semigroup.PositiveShift) (hnu : ↑mu < ↑nu) (z : Y) : ↑nu * ((R.operator nu) (c • (R.operator mu) g)) z ≤ ↑nu / (↑nu - ↑mu) * (c • (R.operator mu) g) z

Resolvent values are excessive. A nonnegative multiple of the resolvent of a nonnegative observable satisfies, at every larger shift, the pointwise supersolution estimate consumed by generatedSemigroup_apply_le_exp_mul, with the smaller shift as the exponential rate.

theorem Algsuperdiff.Process.PositiveC0ContractiveResolvent.mul_operator_le_of_hasResolventTail {X : Type u_1} [MetricSpace X] [ProperSpace X] [MeasurableSpace X] [BorelSpace X] (R : MarkovProcess.PositiveC0ContractiveResolvent X) {phi : ℝ → ℝ} (hphi : ∀ (s : ℝ), 0 ≤ phi s) {mu : ↑MarkovProcess.Semigroup.PositiveShift} (htail : SubMarkovKernelSemigroup.HasResolventTail R.kernelSemigroup (↑mu) phi) {psi : ZeroAtInftyContinuousMap X ℝ} (hpsi0 : ∀ (z : X), 0 ≤ psi z) (hpsi1 : ∀ (z : X), psi z ≤ 1) (y : X) {rho : ℝ} (hrho : 0 < rho) (hvanish : ∀ (z : X), dist z y < rho → psi z = 0) : ↑mu * ((R.operator mu) psi) y ≤ phi (√↑mu * rho)

Tail decay of the potential measure bounds the normalized resolvent of any observable vanishing at infinity which is at most one and vanishes on the ball.

theorem Algsuperdiff.Process.PositiveC0ContractiveResolvent.measure_compl_ball_le_of_hasResolventTail {X : Type u_1} [MetricSpace X] [ProperSpace X] [MeasurableSpace X] [BorelSpace X] (R : MarkovProcess.PositiveC0ContractiveResolvent X) (hcons : R.kernelSemigroup.IsConservative) {phi : ℝ → ℝ} (hphi : ∀ (s : ℝ), 0 ≤ phi s) {mu : ↑MarkovProcess.Semigroup.PositiveShift} (htail : SubMarkovKernelSemigroup.HasResolventTail R.kernelSemigroup (↑mu) phi) {t : NNReal} (ht : ↑mu * ↑t = 1) (x : X) {r : ℝ} (hr : 0 < r) : ((R.kernelSemigroup.kernel t) x) (Metric.ball x (4 * r))ᶜ ≤ ENNReal.ofReal (2 * Real.exp 1 * phi (√↑mu * r))

Displacement tails from resolvent tail decay. Let the sub-Markov kernel semigroup represented by a positive C₀-contractive resolvent be conservative, and let its mu-potential measures have the tail decay phi in the sense of HasResolventTail. Then at the time t = 1 / mu the transition law started at x leaves the ball of radius 4 * r about x with probability at most 2 * exp 1 * phi (sqrt mu * r).

The proof compares the transition law with the excessive function 2 mu R_mu g, where g is a radial cutoff vanishing on the ball of radius r and equal to one outside the ball of radius 2 r, extended to the one-point compactification by the value one. Conservativity enters once, to turn the tail bound at the starting point into a lower bound for the resolvent of the complementary cutoff.