Gamma distributions over ℝ #
Define the gamma measure over the reals.
Main definitions #
gammaPDFReal
: the functiona r x ↦ r ^ a / (Gamma a) * x ^ (a-1) * exp (-(r * x))
for0 ≤ x
or0
else, which is the probability density function of a gamma distribution with shapea
and rater
(whenha : 0 < a
andhr : 0 < r
).gammaPDF
:ℝ≥0∞
-valued pdf,gammaPDF a r = ENNReal.ofReal (gammaPDFReal a r)
.gammaMeasure
: a gamma measure onℝ
, parametrized by its shapea
and rater
.gammaCDFReal
: the CDF given by the definition of CDF inProbabilityTheory.CDF
applied to the gamma measure.
The pdf of the gamma distribution, as a function valued in ℝ≥0∞
Instances For
The gamma pdf is measurable.
The gamma pdf is strongly measurable
Measure defined by the gamma distribution
Equations
Instances For
CDF of the gamma distribution