Topological support of the gamma distribution

This file identifies the support of a gamma law with positive shape and rate. Although the law is almost surely strictly positive, every neighbourhood of zero has positive mass, so the support is the closed nonnegative half-line.

@[simp]

theorem TauCeti.Probability.support_gammaMeasure {a r : ℝ} (ha : 0 < a) (hr : 0 < r) : (ProbabilityTheory.gammaMeasure a r).support = Set.Ici 0

A gamma law with positive shape and rate has topological support [0, ∞).