OAI/Probability/GammaPassage/MeanPairSeminorm.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.gammaMeanPairSeminorm line 13
2. theorem OAI.GammaFPP.gammaMeanPairSeminorm_integerPair line 30

   Source documentation

   The extended mean seminorm agrees on lattice points with the normalized expectation limit of passage times.

   theorem gammaMeanPairSeminorm_integerPair
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (x : Vertex) : gammaMeanPairSeminorm h hs hr ((x.1 : ℝ), (x.2 : ℝ)) =
         directionalMeanConstant h hs hr x := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.gammaMeanPairSeminorm, OAI.GammaFPP.directionalMeanConstant