OAI/Probability/GammaPassage/GlobalConcentration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.localizationErrorBound line 9
2. def OAI.GammaFPP.meanLocalizationAllowance line 13
3. theorem OAI.GammaFPP.GammaEnvironment.passageTime_centered_exponential line 22

   Source documentation

   Unrestricted centered Gamma passage-time concentration with an explicit localization allowance and constants depending only on the shape and rate.

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

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.meanLocalizationAllowance, OAI.PlanarFPP.passageTime, OAI.GammaFPP.FiniteLocal.concentrationKappa, OAI.GammaFPP.localizationErrorBound

4. theorem OAI.GammaFPP.GammaEnvironment.passageTime_centered_exponential_at line 40

   Source documentation

   Equivalent arbitrary absolute-deviation threshold. sqrt R is positive because d<R, even at p=q. The explicit error need not be small for small R.

   theorem GammaEnvironment.passageTime_centered_exponential_at
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (p q : Vertex) (R : ℕ) (hR : latticeDistance p q < R) (u : ℝ) :
       P.real {ω | u ≤ |PlanarFPP.passageTime (fun e => τ e ω) p q -
         ∫ η, PlanarFPP.passageTime (fun e => τ e η) p q ∂P|} ≤
         2*exp (1-FiniteLocal.concentrationKappa shape rate *
           ((u-meanLocalizationAllowance shape rate (latticeDistance p q) R)/sqrt R)) +
           localizationErrorBound shape rate (latticeDistance p q) R := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.PlanarFPP.passageTime, OAI.GammaFPP.FiniteLocal.concentrationKappa, OAI.GammaFPP.meanLocalizationAllowance, OAI.GammaFPP.localizationErrorBound