OAI/Probability/GammaPassage/CDF.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.gamma_nullSingleton line 15
2. lemma OAI.GammaFPP.gamma_cdf_continuous line 19
3. lemma OAI.GammaFPP.gamma_Ioc_pos line 34
4. lemma OAI.GammaFPP.gamma_cdf_strictMonoOn line 53
5. lemma OAI.GammaFPP.gamma_cdf_zero line 62
6. lemma OAI.GammaFPP.gamma_cdf_lt_one line 73
7. lemma OAI.GammaFPP.gamma_cdf_existsUnique line 80

   Source documentation

   Every u ∈ [0, 1) has a unique nonnegative Gamma quantile.

   lemma gamma_cdf_existsUnique (hs : 0 < shape) (hr : 0 < rate)
       {u : ℝ} (hu : 0 ≤ u) (hu1 : u < 1) :
       ∃! x : ℝ, 0 ≤ x ∧ cdf (gammaMeasure shape rate) x = u := by
   …