OAI/Probability/GammaPassage/GoodSiteProbability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.CrossingBridge.goodSiteEvent_failure_bound line 12
2. theorem OAI.GammaFPP.CrossingBridge.gamma_goodSiteEvent_failure line 43

   Source documentation

   Choosing the separation after the trial count gives an error uniform in both the site and the longitudinal scale.

   theorem gamma_goodSiteEvent_failure (h : GammaEnvironment shape rate P τ)
       (hshape : 0 < shape) (hrate : 0 < rate)
       (b A R ε : ℝ) (hb : |b| ≤ 1) (plus : Bool) (M : ℕ) (hM : 0 < M)
       (hR : 0 ≤ R) (hε : 0 < ε) :
       ∃ D0 : ℝ, 1 ≤ D0 ∧ ∀ κ > 0, ∀ᶠ s : ℝ in atTop,
         ∀ (n : ℤ) (v : Vertex) (p0 : ℝ),
         p0 ≤ P.real {ω | (fun e => τ e ω) ∈
           rareFastEvent b ((gammaMeanNorm h hshape hrate) (direction b)) (extremeSlope (gammaMeanNorm h hshape hrate) b plus) A R ε s n 0} →
         P.real {ω | (fun e => τ e ω) ∉ goodSiteEvent (gammaMeanNorm h hshape hrate) b A R ε s plus n ⌈D0*s⌉ M v} <
           (1-p0)^M+κ := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.CrossingBridge.rareFastEvent, OAI.GammaFPP.gammaMeanNorm, OAI.GammaFPP.CrossingBridge.goodSiteEvent