OAI/Probability/GammaPassage/LocalCenteredConcentration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.FiniteLocal.finitePassageTime_centered_exponential line 15

   Source documentation

   For every real threshold t, finite local fluctuations have a centered sqrt(R)-scale exponential tail. The scale is positive for every rate>0.

   theorem finitePassageTime_centered_exponential {shape rate : ℝ}
       (hs : 0 < shape) (hr : 0 < rate) (p q : Vertex) (R : ℕ)
       (hR : latticeDistance p q < R) (t : ℝ) :
       (finiteGammaMeasure shape rate)
         {v | t*sqrt R ≤ |finitePassageTime p q R v -
           ∫ w, finitePassageTime p q R w ∂finiteGammaMeasure shape rate|} ≤
         2*ENNReal.ofReal (exp (1-concentrationKappa shape rate*t)) := by
   …

   Mentions: OAI.GammaFPP.finiteGammaMeasure, OAI.GammaFPP.FiniteLocal.finitePassageTime, OAI.GammaFPP.FiniteLocal.concentrationKappa