OAI/Probability/GammaPassage/LocalLawTransfer.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.GammaEnvironment.local_restriction_law line 13
2. theorem OAI.GammaFPP.GammaEnvironment.localPassageTime_law line 20

   Source documentation

   The local passage-time law is the pushforward of the finite Gamma product law.

   theorem GammaEnvironment.localPassageTime_law
       (h : GammaEnvironment shape rate P τ) (p q : Vertex) (R : ℕ)
       (hR : latticeDistance p q < R) :
       P.map (fun ω => FiniteLocal.passageTime (fun e => τ e ω) p q R) =
         (finiteGammaMeasure shape rate).map (FiniteLocal.finitePassageTime p q R) := by
   …

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

3. theorem OAI.GammaFPP.GammaEnvironment.integral_localPassageTime line 34

   Source documentation

   The finite-coordinate passage time has the same expectation as its realization in a Gamma environment.

   theorem GammaEnvironment.integral_localPassageTime
       (h : GammaEnvironment shape rate P τ) (p q : Vertex) (R : ℕ)
       (hR : latticeDistance p q < R) :
       (∫ ω, FiniteLocal.passageTime (fun e => τ e ω) p q R ∂P) =
         ∫ v, FiniteLocal.finitePassageTime p q R v ∂finiteGammaMeasure shape rate := by
   …

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

4. theorem OAI.GammaFPP.GammaEnvironment.integrable_localPassageTime line 53

   Source documentation

   Local passage times in a Gamma environment are integrable.

   theorem GammaEnvironment.integrable_localPassageTime
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (p q : Vertex) (R : ℕ) (hR : latticeDistance p q < R) :
       Integrable (fun ω => FiniteLocal.passageTime (fun e => τ e ω) p q R) P := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.FiniteLocal.passageTime

5. theorem OAI.GammaFPP.GammaEnvironment.localPassageTime_centered_exponential line 79

   Source documentation

   Centered local passage times have exponential tails at scale sqrt R, for every real threshold.

   theorem GammaEnvironment.localPassageTime_centered_exponential
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (p q : Vertex) (R : ℕ) (hR : latticeDistance p q < R) (t : ℝ) :
       P {ω | t*sqrt R ≤ |FiniteLocal.passageTime (fun e => τ e ω) p q R -
         ∫ η, FiniteLocal.passageTime (fun e => τ e η) p q R ∂P|} ≤
         2*ENNReal.ofReal (exp (1-FiniteLocal.concentrationKappa shape rate*t)) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.FiniteLocal.passageTime, OAI.GammaFPP.FiniteLocal.concentrationKappa