Gamma distribution

Stream: mathlib4

[Josha Dekker]

I noticed that the Gamma distribution is still missing. I started writing some code for this, which will hopefully allow us to refactor the definitions for the exponential distribution from this, and to facilitate an easy introduction of e.g. chi-squared and Erlang distributions. I'll tag a PR to this message once I think there is enough in there!

[Josha Dekker]

I have written up the API that generalises almost all of Exponential.lean to the Gamma distribution. I have also refactored all of Exponential.lean to use the proven results for the Gamma distribution. Shall I first make a PR for the gamma distribution and then for the refactoring, or do one bigger PR?

[Josha Dekker]

I'll add Chi-squared after the PR gets accepted to avoid doing double work!

[Josha Dekker]

Would we be interested in expressions for the moments of the Gamma distribution? We do not seem yet have that for the Exponential distribution. Adding these would be very straightforward, as the necessary integrals can be easily computed from an integral that I have already computed!

[David Loeffler]

How many lines of code is this? Generally it's better to go for multiple shorter PRs rather than one massive one – as a guideline, try to keep individual PR's to < 300 lines or so. (You write "generalises almost all of Exponential.lean", but there are several files in mathlib with that name, and their lengths vary from 50 to 2000 lines...)

[Josha Dekker]

Whoops, I meant Probability/Distributions/Exponential.lean, I forgot about the other uses of the word for a second :man_facepalming:. Setting up all properties for the Gamma distribution is +260 lines. Refactoring Distributions/Exponential.lean would remove around 200 and add around 150 lines.

[Josha Dekker]

I guess I could also add some more stuff like scaling by constants & the Radon-Nikodym derivatives, but these were not in Distributions/Exponential.lean as of yet, so I'd keep that for a follow-up PR.

[Josha Dekker]

The definitions and basic results for the Gamma distribution are now given in #9408. Once it merges, I will add a PR to refactor the Exponential distribution.

[Josha Dekker]

I've refactored the proofs in Probability/Distributions/Exponential to use those of Probability/Distributions/Gamma and tried to incorporate the style feedback that I got in #9408 here as well; e.g. the file now no longer uses Fact's, at the cost of replacing an instance instIsProbabilityMeasureExponential by a lemma isProbabilityMeasureExponential. The PR is #9462, I'm waiting to see if it builds to identify if there are any downstream uses of Probability/Distributions/Gamma that I've broken in making some arguments implicit; other than that a second pair of eyes to go over the material would be much appreciated!

[Sébastien Gouëzel]

Is it possible to get an instance that it is always a probability measure (without any Fact), by defining the measure to be what you think it should be when r > 0, and the Dirac mass at 0 otherwise (or any nice choice that would make as many results as possible true without the assumption r > 0)?

[Josha Dekker]

Sébastien Gouëzel said:

Is it possible to get an instance that it is always a probability measure (without any Fact), by defining the measure to be what you think it should be when r > 0, and the Dirac mass at 0 otherwise (or any nice choice that would make as many results as possible true without the assumption r > 0)?

That sounds like a good idea, I’ll take a look soon!

[Josha Dekker]

Sébastien Gouëzel said:

Is it possible to get an instance that it is always a probability measure (without any Fact), by defining the measure to be what you think it should be when r > 0, and the Dirac mass at 0 otherwise (or any nice choice that would make as many results as possible true without the assumption r > 0)?

I've experimented with this for the Poisson distribution (the small PR #9554), and this seems to work just fine; I see that the Gaussian distribution file does a similar thing. I'll wait until my PR #9642 for the exponential distribution has been merged and then I'll make a PR extending the results for gamma and exponential to NNReal!