OAI/Probability/GammaPassage/CrossingEvents.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.CrossingBridge.crossingEvent line 8
2. theorem OAI.GammaFPP.CrossingBridge.measurableSet_crossingEvent line 13
3. theorem OAI.GammaFPP.CrossingBridge.crossingEvent_depends line 16
4. lemma OAI.GammaFPP.CrossingBridge.crossingEvent_eq_rareFastEvent line 20
5. lemma OAI.GammaFPP.CrossingBridge.crossingEvent_translate line 32
6. def OAI.GammaFPP.CrossingBridge.gridTrialTranslate line 38
7. lemma OAI.GammaFPP.CrossingBridge.gridTrialTranslate_center line 41
8. lemma OAI.GammaFPP.CrossingBridge.gridTrialTranslate_separation line 47
9. lemma OAI.GammaFPP.CrossingBridge.gridTrials_disjoint line 63
10. lemma OAI.GammaFPP.CrossingBridge.crossingEvent_probability_translate line 88
11. theorem OAI.GammaFPP.CrossingBridge.gridTrials_failure_bound line 96

    Source documentation

    Failure bound for all j² translated crossing trials.

    theorem gridTrials_failure_bound (henv : GammaEnvironment shape rate P τ)
        (b m K q₀ : ℝ) (X h w l : ℤ) (hw : 1 ≤ w) (j : ℕ)
        (hq : q₀ ≤ P.real {ω | (fun e => τ e ω) ∈ crossingEvent b m K w l 0}) :
        P.real {ω | ∀ t : Fin (j^2), (fun e => τ e ω) ∉
          crossingEvent b m K w l (gridTrialTranslate b X h w t)} ≤ (1-q₀)^(j^2) := by
    …

    Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.CrossingBridge.crossingEvent, OAI.GammaFPP.CrossingBridge.gridTrialTranslate

12. def OAI.GammaFPP.CrossingBridge.gridBinGood line 115

    Source documentation

    Grid-bin failure bound from a lower bound on the origin crossing probability.

    noncomputable def gridBinGood (shape rate b m K : ℝ) (X h w l : ℤ) (j : ℕ) :
        Set (Edge → ℝ) :=
    …

13. theorem OAI.GammaFPP.CrossingBridge.gridBinGood_failure_bound line 123