ResolventTailMoments

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

Kolmogorov moments from resolvent tail decay

The displacement tail of Kernel/ResolventTail.lean is integrated here against the cubic weight of the layer-cake formula, which turns it into the intrinsic fourth-moment criterion SubMarkovKernelSemigroup.HasKolmogorovMoments 4 2 M and hence, through Main.lean, into the continuous-path process.

The layer cake is applied to the displacement rescaled by 4 sqrt t, so that the tail estimate enters in the scale-free variable and the time dependence t ^ 2 is produced by the Jacobian alone. Below the cutting radius the transition mass is bounded by one, which contributes (4 a) ^ 4 t ^ 2; above it the tail estimate contributes 8 e 4 ^ 4 times the cubic budget I of the profile. The resulting constant is explicit in the statement.

The budget is a hypothesis, as the tail decay is: nothing here asserts an analytic estimate for a particular generator.

On a state space of finite diameter only the shifts at least one are needed, because only the times at most one enter the local criterion. That is the form the one-point compactification of a live space uses: with an exhaustion function bounded by one, tail decay in the metric it determines produces the regularity data from which the continuous-path process of the compactified semigroup is formed.

theorem Algsuperdiff.Process.OnePoint.exhaustionDist_le_two {X : Type u_1} [MetricSpace X] {rho : X → ℝ} (hrho_le : ∀ (x : X), rho x ≤ 1) (z w : OnePoint X) : OnePoint.exhaustionDist rho z w ≤ 2

An exhaustion function bounded by one gives the compactification diameter at most two.

theorem Algsuperdiff.Process.OnePoint.exhaustionMetricSpace_edist_pow_le {X : Type u_1} [MetricSpace X] (rho : X → ℝ) (hrho_cont : Continuous rho) (hrho_pos : ∀ (x : X), 0 < rho x) (hrho_lipschitz : LipschitzWith 1 rho) (hrho_compact : ∀ epsilon > 0, IsCompact {x : X | epsilon ≤ rho x}) (hrho_le : ∀ (x : X), rho x ≤ 1) (z w : OnePoint X) : edist w z ^ 4 ≤ ↑16

The compactification displacement bound. In the metric determined by an exhaustion function bounded by one, the fourth power of the distance on the compactification is at most sixteen. This is the uniform displacement bound the local moment criterion consumes.

theorem Algsuperdiff.Process.lintegral_Ioc_ofReal_cube {a : ℝ} (ha : 0 ≤ a) : ∫⁻ (s : ℝ) in Set.Ioc 0 a, ENNReal.ofReal (s ^ 3) = ENNReal.ofReal (a ^ 4 / 4)

The weighted layer-cake budget of a cubic weight on a bounded interval.

theorem Algsuperdiff.Process.PositiveC0ContractiveResolvent.lintegral_edist_pow_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} (htmu : ↑mu * ↑t = 1) {a I : ℝ} (ha : 0 ≤ a) (hI : 0 ≤ I) (hint : ∫⁻ (s : ℝ) in Set.Ioi a, ENNReal.ofReal (phi s * s ^ 3) ≤ ENNReal.ofReal I) (x : X) : ∫⁻ (z : X), edist z x ^ 4 ∂(R.kernelSemigroup.kernel t) x ≤ ENNReal.ofReal (256 * (a ^ 4 + 8 * Real.exp 1 * I)) * ENNReal.ofReal (↑t ^ 2)

The fourth displacement moment at one time from resolvent tail decay. The layer-cake formula in the parabolic variable turns the displacement tail into a fourth moment of order t ^ 2, with the trivial bound below the cutting radius and the tail estimate above it.

theorem Algsuperdiff.Process.PositiveC0ContractiveResolvent.lintegral_edist_pow_zero {X : Type u_1} [MetricSpace X] [ProperSpace X] [MeasurableSpace X] [BorelSpace X] (R : MarkovProcess.PositiveC0ContractiveResolvent X) (y : X) : ∫⁻ (z : X), edist z y ^ 4 ∂(R.kernelSemigroup.kernel 0) y = 0

The fourth displacement moment of a transition law vanishes at the time zero.

def Algsuperdiff.Process.PositiveC0ContractiveResolvent.OnePointRegular.ofHasLocalKolmogorovMoments {X : Type u_1} [MetricSpace X] [ProperSpace X] [MeasurableSpace X] [BorelSpace X] (R : MarkovProcess.PositiveC0ContractiveResolvent X) (rho : X → ℝ) (hrho_cont : Continuous rho) (hrho_pos : ∀ (x : X), 0 < rho x) (hrho_lipschitz : LipschitzWith 1 rho) (hrho_compact : ∀ epsilon > 0, IsCompact {x : X | epsilon ≤ rho x}) {q : ℝ} {M B : NNReal} (hmom : R.onePointKernelSemigroup.HasLocalKolmogorovMoments 4 q M B) : R.OnePointRegular

Regularity data of a compactified process from a local moment estimate. An exhaustion function and a local fourth-moment estimate for the compactified semigroup in the metric that function determines give the data from which the continuous-path process of the compactified semigroup is formed. This is the common core of the tail criteria below: they differ only in how the local moment estimate is produced.

Equations

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