Cumulative distribution function of the inverse-gamma distribution

This file computes the inverse-gamma cdf as an upper regularized Gamma value.

Cumulative distribution function

@[simp]

theorem TauCeti.Probability.cdf_inverseGammaMeasure_eq {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (x : ℝ) : ↑(ProbabilityTheory.cdf (inverseGammaMeasure a r)) x = if x ≤ 0 then 0 else 1 - regularizedGamma a (r / x)

The cdf of a valid inverse-gamma law is the upper regularized Gamma value 1 - P(a, r / x) on the positive half-line and zero elsewhere.