ResolventTailVariable

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

Kolmogorov moments from a shift-dependent resolvent tail

The moment criterion of Kernel/ResolventTailMoments.lean asks for one profile and one trivial cutting radius valid at every shift. An analytic estimate whose decay rate degrades with the shift satisfies no such uniform statement, and this file removes the requirement: the profile phi lam and the cutting radius cut lam may both depend on the shift, and only two things are asked uniformly, the cubic layer-cake budget I of the profile beyond its cutting radius and the growth cut lam ^ 4 ≤ A lam ^ (2 - q) of the cutting radius.

The price is the time exponent. At the time t the layer cake is applied at the shift 1 / t, where the trivial radius contributes 256 cut (1 / t) ^ 4 t ^ 2; the growth hypothesis converts that into 256 A t ^ q, and the budget term 256 · 8 e I · t ^ 2 is absorbed into t ^ q because t ≤ 1 and q ≤ 2. A cutting radius growing logarithmically in the shift is therefore free for every q < 2, and the library charges nothing for the smaller exponent: the local criterion, its passage to the global one, and the continuous-path construction are all stated for a general q > 1.

PositiveC0ContractiveResolvent.OnePointRegular.ofVariableResolventTail is the resulting regularity data of the compactified process, obtained from the local criterion through the shared core OnePointRegular.ofHasLocalKolmogorovMoments. Nothing here asserts an analytic estimate for a particular generator: the tail decay, the budget and the growth of the cutting radius are the consumer's hypotheses.

theorem Algsuperdiff.Process.PositiveC0ContractiveResolvent.hasLocalKolmogorovMoments_of_variableResolventTail {X : Type u_1} [MetricSpace X] [ProperSpace X] [MeasurableSpace X] [BorelSpace X] (R : MarkovProcess.PositiveC0ContractiveResolvent X) (hcons : R.kernelSemigroup.IsConservative) {phi : ℝ → ℝ → ℝ} (hphi : ∀ (lam s : ℝ), 0 ≤ phi lam s) (htail : ∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift), 1 ≤ ↑mu → SubMarkovKernelSemigroup.HasResolventTail R.kernelSemigroup (↑mu) (phi ↑mu)) {cut : ℝ → ℝ} (hcut : ∀ (lam : ℝ), 0 ≤ cut lam) {I : ℝ} (hI : 0 ≤ I) (hint : ∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift), 1 ≤ ↑mu → ∫⁻ (s : ℝ) in Set.Ioi (cut ↑mu), ENNReal.ofReal (phi (↑mu) s * s ^ 3) ≤ ENNReal.ofReal I) {q A : ℝ} (hq1 : 1 < q) (hq2 : q ≤ 2) (hA : 0 ≤ A) (hgrowth : ∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift), 1 ≤ ↑mu → cut ↑mu ^ 4 ≤ A * ↑mu ^ (2 - q)) {B : NNReal} (hB : ∀ (y z : X), edist z y ^ 4 ≤ ↑B) : R.kernelSemigroup.HasLocalKolmogorovMoments 4 q (256 * (A + 8 * Real.exp 1 * I)).toNNReal B

The local Kolmogorov criterion from a shift-dependent resolvent tail. The profile and the trivial cutting radius may depend on the shift; a cutting radius growing no faster than lam ^ ((2 - q) / 4) still gives the local moment criterion, with the time exponent q.

noncomputable def Algsuperdiff.Process.PositiveC0ContractiveResolvent.OnePointRegular.ofVariableResolventTail {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}) (hrho_le : ∀ (x : X), rho x ≤ 1) {phi : ℝ → ℝ → ℝ} (hphi : ∀ (lam s : ℝ), 0 ≤ phi lam s) (htail : ∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift), 1 ≤ ↑mu → SubMarkovKernelSemigroup.HasResolventTail R.onePointKernelSemigroup (↑mu) (phi ↑mu)) {cut : ℝ → ℝ} (hcut : ∀ (lam : ℝ), 0 ≤ cut lam) {I : ℝ} (hI : 0 ≤ I) (hint : ∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift), 1 ≤ ↑mu → ∫⁻ (s : ℝ) in Set.Ioi (cut ↑mu), ENNReal.ofReal (phi (↑mu) s * s ^ 3) ≤ ENNReal.ofReal I) {q A : ℝ} (hq1 : 1 < q) (hq2 : q ≤ 2) (hA : 0 ≤ A) (hgrowth : ∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift), 1 ≤ ↑mu → cut ↑mu ^ 4 ≤ A * ↑mu ^ (2 - q)) : R.OnePointRegular

Regularity data of a compactified process from shift-dependent tail decay. An exhaustion function bounded by one, tail decay of the compactified potential measures at every shift at least one with a profile and a trivial cutting radius that may both depend on the shift, a uniform cubic budget and a uniform growth bound for the cutting radius together give the data from which the continuous-path process of the compactified semigroup is formed.

Equations

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