OAI/Probability/GammaPassage/SurvivalQuantile.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.gammaSurvival line 12
2. def OAI.GammaFPP.gammaSurvivalQuantile line 15
3. def OAI.GammaFPP.gammaSurvivalQuantileExtended line 18
4. lemma OAI.GammaFPP.gammaSurvival_mem line 21
5. lemma OAI.GammaFPP.gammaQuantileReal_cdf line 27
6. lemma OAI.GammaFPP.gammaSurvivalQuantile_inverse line 32
7. lemma OAI.GammaFPP.gammaSurvivalQuantile_antitoneOn line 36
8. lemma OAI.GammaFPP.gammaQuantileReal_continuousOn line 48

   Source documentation

   Inverse continuity includes the one-sided probability endpoint zero. The arbitrary real value at probability one is not used.

   lemma gammaQuantileReal_continuousOn :
       ContinuousOn (gammaQuantileReal shape rate hs hr) (Ico (0 : ℝ) 1) := by
   …

   Mentions: OAI.GammaFPP.gammaQuantileReal

9. lemma OAI.GammaFPP.gammaSurvivalQuantile_continuousOn line 82
10. lemma OAI.GammaFPP.gammaSurvivalQuantileExtended_zero line 89
11. lemma OAI.GammaFPP.gammaSurvivalQuantileExtended_of_pos line 93
12. lemma OAI.GammaFPP.gammaSurvivalQuantileExtended_ne_top_iff line 100

    Source documentation

    On the finite-bit domain, the infinity guard is exactly positive survival.

    lemma gammaSurvivalQuantileExtended_ne_top_iff {v : ℝ} (hv : v ∈ Icc (0 : ℝ) 1) :
        gammaSurvivalQuantileExtended hs hr v ≠ ⊤ ↔ 0 < v := by
    …

    Mentions: OAI.GammaFPP.gammaSurvivalQuantileExtended

13. lemma OAI.GammaFPP.gammaSurvivalQuantileExtended_toReal line 112
14. lemma OAI.GammaFPP.gammaSurvivalQuantileExtended_antitoneOn line 117
15. lemma OAI.GammaFPP.gammaSurvivalQuantile_upper_cost line 132

    Source documentation

    Lower survival rounding gives upper actual real cost whenever its guard holds.

    lemma gammaSurvivalQuantile_upper_cost {x v : ℝ} (hx : 0 ≤ x)
        (hv : 0 < v) (hvs : v ≤ gammaSurvival shape rate x) :
        x ≤ gammaSurvivalQuantile hs hr v := by
    …

    Mentions: OAI.GammaFPP.gammaSurvival, OAI.GammaFPP.gammaSurvivalQuantile