OAI/Probability/GammaPassage/LocalCenteredCGF.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.FiniteLocal.finitePassageTime_hasDerivAt_cgf_zero line 11

   Source documentation

   Derivative at zero from the actual positive moment at rate/2.

   theorem finitePassageTime_hasDerivAt_cgf_zero {shape rate : ℝ}
       (hs : 0 < shape) (hr : 0 < rate) (p q : Vertex) (R : ℕ)
       (hR : latticeDistance p q < R) :
       HasDerivAt (cgf (finitePassageTime p q R) (finiteGammaMeasure shape rate))
         (∫ v, finitePassageTime p q R v ∂finiteGammaMeasure shape rate) 0 := by
   …

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

2. theorem OAI.GammaFPP.FiniteLocal.finitePassageTime_cgf_centered line 27

   Source documentation

   Signed centered cgf estimate, with all smallness conditions explicit.

   theorem finitePassageTime_cgf_centered {shape rate : ℝ}
       (hs : 0 < shape) (hr : 0 < rate) (p q : Vertex) (R : ℕ)
       (hR : latticeDistance p q < R) (a : ℝ) (ha : |a| ≤ rate/4)
       (hq : (16*(2 : ℝ)^shape/rate^2)*a^2*R ≤ 1/2) :
       cgf (finitePassageTime p q R) (finiteGammaMeasure shape rate) a ≤
         a*(∫ v, finitePassageTime p q R v ∂finiteGammaMeasure shape rate) +
         4*((16*(2 : ℝ)^shape/rate^2)*a^2*R) := by
   …

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