OneStepLaplace #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
One-step Laplace contraction on a good cube #
The Paley--Zygmund survival probability on the inner cube is converted into a strict contraction for the negative exponential of the exit time from the enlarged cube.
The one-step contraction obtained from survival at half the lower exit-time
scale and discount rate (Cup * T)⁻¹.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Algsuperdiff.Section5.Provider.lintegral_discountedExitTime_le_oneStepLaplaceContraction
{alpha : Type u_1}
[MetricSpace alpha]
[CompleteSpace alpha]
[MeasurableSpace alpha]
[BorelSpace alpha]
[SecondCountableTopology alpha]
[Nonempty alpha]
(P : MarkovProcess.SubMarkovKernelSemigroup alpha)
(hP : P.IsConservative)
{U : Set alpha}
(hU : IsOpen U)
(T Cup clow : NNReal)
(hT : 0 < T)
(hCup : 0 < Cup)
(x : alpha)
(hsurv :
↑(Trace.survivalProbabilityConstant Cup clow) ≤ ((MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x)
{eta : MarkovProcess.ContinuousPath alpha | ↑(clow * T / 2) ≤ MarkovProcess.ContinuousPath.exitTime U eta})
:
∫⁻ (eta : MarkovProcess.ContinuousPath alpha), Process.ContinuousPath.discountedStoppingWeight (↑Cup * ↑T)⁻¹ (MarkovProcess.ContinuousPath.exitTime U)
eta ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x ≤ oneStepLaplaceContraction Cup clow
A uniform lower survival probability gives the one-step Laplace
contraction at rate (Cup * T)⁻¹.