Support of chi-squared laws

Positive-degree chi-squared laws have topological support [0, ∞). At degree zero the support is the singleton zero; negative degrees give empty support. This also describes the components used in Poisson mixtures of chi-squared laws.

@[simp]

theorem TauCeti.Probability.support_chiSquaredMeasure (k : ℝ) : (chiSquaredMeasure k).support = if k = 0 then {0} else if 0 < k then Set.Ici 0 else ∅

The topological support of a chi-squared law, in every degree regime.