[Merged by Bors] - feat : Add Gamma distribution #9408
Conversation
There was a problem hiding this comment.
I've left a bunch of comments. Most of these are just code-style fixes and "golf". The only comment of substance is that I think pow_exp_integral_Ioi should be proved in more generality (allowing complex exponents and deducing the real case from that) and moved to a different file.
Thank you, I'll take a good look tomorrow! Regarding some style comments: I took everything from Probability/Distributions/Exponential.lean and tried to stick as closely to that as possible; I should've probably double-checked style, I'll do that tomorrow! |
JADekker
added
awaiting-review
awaiting-CI
new-contributor
Add pdf, CDF and measure of Gamma distribution. Add proof that this is indeed a probability distribution. Add proofs that relate the various definitions. TODO: Refactor Probability/Distributions/Exponential.lean using calls to the results in this file.
Add pow_exp_integral_Ioi_complex, this extends pow_exp_integral_Ioi to complex numbers. Should probably be moved to one of the files for the Gamma functions. Fix some style issues.
Move pow_exp_integral_Ioi_complex to SpecialFunctions/Gamma/Basic and rename it. Once we agree on the definitive location, pow_exp_integral_Ioi in Distributions/Gamma should be reduced to a call to this result.
Rename pow_exp_integral_Ioi to integral_rpow_mul_exp_neg_mul_Ioi Rename pow_exp_integral_Ioi_complex to integral_cpow_mul_exp_neg_mul_Ioi Move integral_cpow_mul_exp_neg_mul_Ioi to SpecialFunctions/Gamma/Basic Remove lintegral_Iic_eq_lintegral_Iio_add_Icc and lintegral_eq_lintegral_Ici_add_Iio from Distributions/Exponential, these are now imported through Distributions/Gamma, as Gamma should precede Exponential after refactoring. Important sorry: deriving integral_rpow_mul_exp_neg_mul_Ioi from integral_cpow_mul_exp_neg_mul_Ioi is incomplete!
Move integral_rpow_mul_exp_neg_mul_Ioi to SpecialFunctions/Gamma/Basic Remove duplicate theorem from Distributions/Gamma
refactor integral_rpow_mul_exp_neg_mul_Ioi using integral_cpow_mul_exp_neg_mul_Ioi.
collares
force-pushed
the
JADekker_gamma_distribution
branch
from
e203bf7
to
30e2d9b
Compare
Rename instIsProbabilityMeasureGamma to IsProbabilityMeasureGamma
|
I'm very sorry, I was not aware that that would happen. Somehow I bogged up my git and asked for help from @collares to set back my branch; I wasn't aware of these consequences... Is there some way to fix this? Your version is the most up-to-date version, so I'm more than happy if you use that one and make a new PR with it/overwrite the current one entirely, if that is possible! |
|
Don't worry; I manually copy-pasted the changes from my local git branch to somewhere else, downloaded the new git branch, and I'm now back on track. BTW, judging from the latest comments on zulip, it looks like I gave you misleading advice about instance parameters – sorry for that! |
|
No worries! I'm fighting with git on another branch right now, I'll make sure I don't touch this one! |
|
I've pushed a commit which shortens the proofs in |
There was a problem hiding this comment.
Here are some comment. I've tried to fix the spelling / grammar errors in the docstrings for you, since they aren't your fault. (Just in case you aren't aware: you can apply all the suggestions I've made as a batch, by going to the "Files changed" view – that hopefully makes dealing with pedantic reviewers slightly less tedious 😄)
Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
refactor lintegral_gammaPdf_eq_one, removes pow_exp_integral_Ioi_insert_1 as this is superfluous now. minor style changes.
|
Thank you for all the fixes, I'll try to be more critical of spelling and grammar in the future as well! I forgot about the batch apply, thank you for reminding me! |
|
@loefflerd would you like me to start refactoring Probability/Distributions/Exponential.lean and tag that along to this PR, or wait until this PR has merged? I think I'd also like to add the chi-squared distribution as a special case of the Gamma distribution, as it opens up the way for things like t-distributions; if there is no need for that, I'm happy to wait though! |
|
I did some golfing on I'd advise waiting for a little while (until this gets merged) until you start work on the next stage. Since I am not a maintainer myself, somebody else will have to give the final OK to this, and they might ask for yet more changes; and it's always a pain to forward-port changes between multiple PR's in a series. |
|
OK, this looks good to me now! I suggest posting on the zulip "PR reviews" queue, asking for a maintainer to make the final merge decision. |
|
I’ll wait until it builds and then post it there! Thank you! Feel free to add yourself to the copyright statement of course, if you like! |
|
✌️ JADekker can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
|
bors r+ |
Add pdf, CDF and measure of Gamma distribution. Add proof that this is indeed a probability distribution. Add proofs that relate the various definitions. TODO: Refactor Probability/Distributions/Exponential.lean using calls to the results in this file. Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Add pdf, CDF and measure of Gamma distribution.
Add proof that this is indeed a probability distribution. Add proofs that relate the various definitions.
TODO: Refactor Probability/Distributions/Exponential.lean using calls to
the results in this file.