HitExitTail

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

The early-exit tail from composite hit-then-exit chaining

Composing the Chernoff bound of Trajectory/ExitTimeLaplace.lean with the geometric estimate of Trajectory/HitExitChaining.lean turns the discounted chaining bound into a bound on the probability of leaving the open set U before a deterministic time, Q_x {τ_U ≤ t} ≤ e^{λ t} ρ ^ N

(IsConservative.measure_exitTime_le_le_rho_pow_hitExit). The hypotheses are those of the chaining estimate, together with openness of U, which the Chernoff bound needs; the deterministic horizon t is arbitrary, so the consumer chooses it after fixing the discount rate.

Nothing new is proved about the geometry of the hit family: the counting premise is exactly the one of the chaining estimate.

theorem Algsuperdiff.Process.SubMarkovKernelSemigroup.IsConservative.measure_exitTime_le_le_rho_pow_hitExit {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] [LocallyCompactSpace alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (hFeller : P.IsFellerKernelSemigroup) (hK : P.KolmogorovRegular hP) (V V' : ℕ → Set alpha) (hVmeasurable : ∀ (i : ℕ), MeasurableSet (V i)) (hDclosed : IsClosed (⋃ (i : ℕ), V i)) (hV'open : ∀ (i : ℕ), IsOpen (V' i)) (U : Set alpha) (hU : IsOpen U) (lam : ℝ) (hlam : 0 < lam) (rho : ENNReal) (hrho : rho ≠ ⊤) (hone : ∀ (i : ℕ), ∀ z ∈ V i, ∫⁻ (eta : MarkovProcess.ContinuousPath alpha), ContinuousPath.discountedStoppingWeight lam (MarkovProcess.ContinuousPath.exitTime (V' i)) eta ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) z ≤ rho) (K D N : ℕ) (x : alpha) (hoverlap : ∀ (i : ℕ), ∃ (s : Finset ℕ), s.card ≤ K ∧ ∀ (j : ℕ), (V j ∩ V' i).Nonempty → j ∈ s) (hvisits : ∀ᵐ (omega : MarkovProcess.ContinuousPath alpha) ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x, MarkovProcess.ContinuousPath.exitTime U omega < ⊤ → ∃ (s : Finset ℕ), D ≤ s.card ∧ ∀ i ∈ s, ∃ (t : NNReal), ↑t < MarkovProcess.ContinuousPath.exitTime U omega ∧ omega t ∈ V i) (hcount : N * K < D) (t : NNReal) : ((MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x) {omega : MarkovProcess.ContinuousPath alpha | MarkovProcess.ContinuousPath.exitTime U omega ≤ ↑t} ≤ ENNReal.ofReal (Real.exp (lam * ↑t)) * rho ^ N

The early-exit tail of composite hit-then-exit chaining. Under the hypotheses of the chaining estimate, the probability of leaving the open set U by the deterministic time t is at most e^{lam t} rho ^ N.