OAI/Probability/GammaPassage/LocalIntegrability.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.FiniteLocal.finitePassageTime_le_sum line 11

   Source documentation

   Nonnegative candidate cost is bounded by the sum on its containing edge set. Nodup is essential: the finite coordinates are physical edges, not traversals.

   lemma finitePassageTime_le_sum (p q : Vertex) (R : ℕ)
       (hR : latticeDistance p q < R) (v : Coordinates p q R)
       (hv : ∀ e, 0 ≤ v e) : finitePassageTime p q R v ≤ ∑ e, v e := by
   …

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

2. lemma OAI.GammaFPP.FiniteLocal.finitePassageTime_nonneg line 31
3. theorem OAI.GammaFPP.FiniteLocal.integrable_finitePassageTime_exp line 37

   Source documentation

   All real t<=rate/2 are allowed, including arbitrarily negative t.

   theorem integrable_finitePassageTime_exp {shape rate : ℝ}
       (hs : 0 < shape) (hr : 0 < rate)
       (p q : Vertex) (R : ℕ) (hR : latticeDistance p q < R)
       (t : ℝ) (ht : t ≤ rate/2) :
       Integrable (fun v => Real.exp (t * finitePassageTime p q R v))
         (finiteGammaMeasure (ι := ↥(localEdges p q R)) shape rate) := by
   …

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