OAI/Probability/GammaPassage/SurvivalRounding.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.gammaRoundedSurvival line 15
2. def OAI.GammaFPP.gammaRoundedCost line 18
3. lemma OAI.GammaFPP.gammaRoundedSurvival_nonneg line 21
4. lemma OAI.GammaFPP.gammaRoundedSurvival_le line 26
5. lemma OAI.GammaFPP.gammaRoundedSurvival_tendsto line 33
6. lemma OAI.GammaFPP.gammaRoundedSurvival_eventually_pos line 40
7. lemma OAI.GammaFPP.gammaRoundedCost_ge line 45
8. lemma OAI.GammaFPP.gammaRoundedCost_tendsto line 50
9. lemma OAI.GammaFPP.gammaRoundedSurvival_finite_iff line 65

   Source documentation

   Every finite-bit scalar decoder has the intended extended meaning. In particular the zero rank is infinite, even though the real totalization is zero.

   lemma gammaRoundedSurvival_finite_iff (t : ℕ) {x : ℝ} (hx : 0 ≤ x) :
       gammaSurvivalQuantileExtended hs hr
         (gammaRoundedSurvival (shape := shape) (rate := rate) t x) ≠ ⊤ ↔
   …

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