OAI/Probability/GammaPassage/BKRounded.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.BK.RoundedGood line 12
2. lemma OAI.GammaFPP.BK.rounded_original line 16
3. lemma OAI.GammaFPP.BK.rounded_path_tendsto line 21
4. lemma OAI.GammaFPP.BK.eventually_rounded line 29
5. def OAI.GammaFPP.BK.RoundedDisjoint line 39
6. lemma OAI.GammaFPP.BK.rounded_disjoint_original line 45
7. lemma OAI.GammaFPP.BK.list_eventually_rounded line 51
8. lemma OAI.GammaFPP.BK.disjoint_eventually_rounded line 64
9. lemma OAI.GammaFPP.BK.cell_survival line 88
10. lemma OAI.GammaFPP.BK.cell_path_iff line 95
11. lemma OAI.GammaFPP.BK.rounded_guard_is_finite line 114

    Source documentation

    Every guarded edge has finite extended cost; zero rank remains infinity.

    lemma rounded_guard_is_finite (t : ℕ) {w : Edge → ℝ} (hw : ∀ e, 0 ≤ w e)
        (p : StrictPathWitness) :
        (∀ e ∈ p.edges, gammaSurvivalQuantileExtended hs hr
          (gammaRoundedSurvival (shape := shape) (rate := rate) t (w e)) ≠ ⊤) ↔
    …

    Mentions: OAI.GammaFPP.BK.StrictPathWitness, OAI.GammaFPP.gammaSurvivalQuantileExtended, OAI.GammaFPP.gammaRoundedSurvival