ExitTimeSurvival #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Survival of the exit time above a fraction of its mean #
A uniform bound E_y tau_U ≤ M on the expected exit time from an open set U, valid from every
starting point, controls every moment of the exit time. The multiplier K = 4 and the rate
lam = log (4 / 3) / (4 M) meet the rate condition of
IsConservative.lintegral_exponentialStoppingWeight_exitTime_le_two_of_lintegral_le with equality,
so E_x exp (lam * tau_U) ≤ 2, and the elementary bound t ^ p ≤ (p / (lam * e)) ^ p * exp (lam t)
turns that into E_x tau_U ^ p ≤ 2 * (p / (lam * e)) ^ p
(IsConservative.lintegral_exitTime_pow_le_of_lintegral_le). At p = 2 this is the explicit
second-moment bound E_x tau_U ^ 2 ≤ 288 * M ^ 2
(IsConservative.lintegral_exitTime_sq_le_of_lintegral_le).
Fed into the Paley--Zygmund inequality, the second moment turns a lower bound mLow ≤ E_x tau_U
into a lower bound on the probability of surviving a fraction of mLow,
(1 - rho) ^ 2 * mLow ^ 2 ≤ 288 * M ^ 2 * Q_x {rho * mLow ≤ tau_U}
(IsConservative.sq_le_mul_measure_le_exitTime_of_lintegral_le), which at rho = 1 / 2 reads
mLow ^ 2 ≤ 1152 * M ^ 2 * Q_x {mLow / 2 ≤ tau_U}
(IsConservative.sq_le_mul_measure_half_le_exitTime_of_lintegral_le). The upper bound M is
required from every starting point, as the exponential moment needs it; the lower bound mLow is
required only at the starting point whose survival probability is bounded, so the conclusion is
uniform over any set of starting points on which the lower bound holds.
The constant 288 is not optimal. It records the two crude estimates 1 / 4 ≤ log (4 / 3) and
8 / 3 ≤ e that keep the arithmetic elementary; the exponential-moment theorem itself is stated
with a free multiplier and a free rate, so a consumer wanting a smaller constant can supply its
own pair.
Every polynomial moment from an expected-exit bound. A uniform bound M on the expected
exit time from U, together with a multiplier K > 1 and a positive rate lam meeting the
normalization condition exp (lam * K * M) * (K + 2) ≤ 2 * K, bounds every polynomial moment of
the exit time by 2 * (p / (lam * e)) ^ p.
An explicit second moment from an expected-exit bound. A uniform bound M on the
expected exit time from U, valid from every starting point, gives the second-moment bound
E_x tau_U ^ 2 ≤ 288 * M ^ 2 from every starting point.
Paley--Zygmund for the exit time. A uniform bound M on the expected exit time from U,
valid from every starting point, together with a lower bound mLow on the expected exit time from
the single starting point x, bounds the probability of surviving the level rho * mLow:
(1 - rho) ^ 2 * mLow ^ 2 ≤ 288 * M ^ 2 * Q_x {rho * mLow ≤ tau_U}. The subtraction is the
truncated one of ℝ≥0∞, so a level rho ≥ 1 leaves the trivial bound.
Survival above half the guaranteed mean. The level rho = 1 / 2 of
IsConservative.sq_le_mul_measure_le_exitTime_of_lintegral_le:
mLow ^ 2 ≤ 1152 * M ^ 2 * Q_x {mLow / 2 ≤ tau_U}.