OAI/Probability/GammaPassage/Quantile.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.gammaQuantileReal line 11
2. lemma OAI.GammaFPP.gammaQuantileReal_spec line 17
3. lemma OAI.GammaFPP.gammaQuantileReal_nonneg line 24
4. lemma OAI.GammaFPP.gammaQuantileReal_le_iff line 30
5. lemma OAI.GammaFPP.gammaQuantileReal_zero line 44
6. lemma OAI.GammaFPP.gammaQuantileReal_measurable line 50
7. def OAI.GammaFPP.unitUniform line 73

   Source documentation

   Lebesgue probability on the closed unit interval.

   noncomputable def unitUniform : Measure ℝ := volume.restrict (Icc 0 1)

8. lemma OAI.GammaFPP.unitUniform_eq_Ico line 75
9. instance OAI.GammaFPP.unitUniform_probability line 78
10. lemma OAI.GammaFPP.gammaQuantileReal_map line 81
11. def OAI.GammaFPP.gammaQuantileExtended line 113

    Source documentation

    The extended Gamma quantile used for upper rounding takes the value infinity at u = 1.

    noncomputable def gammaQuantileExtended (shape rate : ℝ) (hs : 0 < shape) (hr : 0 < rate)
        (u : ℝ) : ℝ≥0∞ :=
    …

12. lemma OAI.GammaFPP.gammaQuantileExtended_one line 117
13. lemma OAI.GammaFPP.gammaQuantileExtended_measurable line 121
14. lemma OAI.GammaFPP.gammaQuantileExtended_map line 127

    Source documentation

    The extended quantile has the Gamma law embedded into ℝ≥0∞; its endpoint value affects no probability.

    lemma gammaQuantileExtended_map {shape rate : ℝ} (hs : 0 < shape) (hr : 0 < rate) :
        Measure.map (gammaQuantileExtended shape rate hs hr) unitUniform =
          Measure.map ENNReal.ofReal (gammaMeasure shape rate) := by
    …

    Mentions: OAI.GammaFPP.gammaQuantileExtended, OAI.GammaFPP.unitUniform