ResolventTail

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

Resolvent tails for the whole-space analytic exhaustion

The process construction below consumes the library predicate Algsuperdiff.Process.SubMarkovKernelSemigroup.HasResolventTail through an explicit profile package. This keeps the probabilistic theorem independent of the analytic route used to prove the tail.

The intended coefficient class is a = nu I + k, with nu > 0 and k continuous, skew, and of arbitrary size. The small-contrast construction is the first named input. The stream-field construction instead uses its split-skew localized bounds and a subexponential profile with finite cubic layer-cake budget, without changing any process declaration.

structure DivergenceFormProcess.Form.WholeSpaceVariableExhaustionResolventTailInput {d : ℕ} (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) : Type

A shift-dependent exhaustion-metric resolvent-tail input. The profile and the trivial cutting radius may depend on the shift; only the cubic layer-cake budget and the growth of the cutting radius are uniform.

• rho : HCPolySupport.Vec d → ℝ

  The positive exhaustion weight used for the one-point metric.

• continuous_rho : Continuous self.rho
• rho_pos (x : HCPolySupport.Vec d) : 0 < self.rho x
• lipschitz_rho : LipschitzWith 1 self.rho
• isCompact_superlevel (epsilon : ℝ) : epsilon > 0 → IsCompact {x : HCPolySupport.Vec d | epsilon ≤ self.rho x}
• rho_le_one (x : HCPolySupport.Vec d) : self.rho x ≤ 1
• phi : ℝ → ℝ → ℝ

  The nonnegative tail envelope indexed by the resolvent shift and distance.

• phi_nonneg (lam s : ℝ) : 0 ≤ self.phi lam s
• hasTail (mu : ↑MarkovProcess.Semigroup.PositiveShift) : 1 ≤ ↑mu → Algsuperdiff.Process.SubMarkovKernelSemigroup.HasResolventTail R.onePointKernelSemigroup (↑mu) (self.phi ↑mu)
• cutoff : ℝ → ℝ

  The lower integration cutoff for each resolvent shift's tail bound.

• cutoff_nonneg (lam : ℝ) : 0 ≤ self.cutoff lam
• budget : ℝ

  The common bound for the cubic-weighted resolvent-tail integrals.

• budget_nonneg : 0 ≤ self.budget
• integral_le (mu : ↑MarkovProcess.Semigroup.PositiveShift) : 1 ≤ ↑mu → ∫⁻ (s : ℝ) in Set.Ioi (self.cutoff ↑mu), ENNReal.ofReal (self.phi (↑mu) s * s ^ 3) ≤ ENNReal.ofReal self.budget
• timeExponent : ℝ

  The exponent controlling the time regularity obtained from the resolvent tails.

• one_lt_timeExponent : 1 < self.timeExponent
• timeExponent_le_two : self.timeExponent ≤ 2
• cutoffGrowth : ℝ

  The constant bounding the fourth power of the shift-dependent tail cutoff.

• cutoffGrowth_nonneg : 0 ≤ self.cutoffGrowth
• cutoff_pow_le (mu : ↑MarkovProcess.Semigroup.PositiveShift) : 1 ≤ ↑mu → self.cutoff ↑mu ^ 4 ≤ self.cutoffGrowth * ↑mu ^ (2 - self.timeExponent)

noncomputable def DivergenceFormProcess.Form.WholeSpaceVariableExhaustionResolventTailInput.toOnePointRegular {d : ℕ} {R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)} (H : WholeSpaceVariableExhaustionResolventTailInput R) : R.OnePointRegular

The shift-dependent exhaustion-tail package gives the one-point regularity data used by the canonical process construction.

Equations

• H.toOnePointRegular = Algsuperdiff.Process.PositiveC0ContractiveResolvent.OnePointRegular.ofVariableResolventTail R H.rho ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def DivergenceFormProcess.Form.WholeSpaceAnalyticData.KernelResolventIdentifiesAnalyticMinimal {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)) : Prop

Identification of a process kernel resolvent with the analytic cubic supremum on nonnegative observables bounded by one. The minimal-resolvent construction supplies this after identifying each transported cube resolvent.

Equations

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