OAI/Probability/GammaPassage/OriginEscapeLower.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.gammaMeanNorm_lower_euclidean line 11
2. theorem OAI.GammaFPP.gammaMeanNorm_exists_positive_lower line 17
3. theorem OAI.GammaFPP.GammaEnvironment.ae_eventually_origin_escape line 24

   Source documentation

   Origin escape with the positive coefficient proved from the actual Gamma mean lower bound, rather than supplied as an additional hypothesis.

   theorem GammaEnvironment.ae_eventually_origin_escape
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (δ : ℝ) (hδ : 0 < δ) :
       ∀ᵐ ω ∂P, ∀ᶠ s : ℝ in atTop, ∀ z : Vertex,
         δ*s/3 ≤ ‖RealDirectionBridge.latticeEmbed z‖ →
         cheapSlope shape rate*δ*s/6 ≤ passageTime (fun e => τ e ω) 0 z :=
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.RealDirectionBridge.latticeEmbed, OAI.GammaFPP.cheapSlope