Geometric distribution

Stream: Is there code for X?

[Josha Dekker]

I've noticed that there is no code for the geometric distribution at this point, is there any work on this? Otherwise, I'm happy to write up some very basic API, to add a missing element of https://leanprover-community.github.io/undergrad_todo.html

[Josha Dekker]

This is now #9561, any input is welcome! I'm not too happy with writing the requirement on p like this, it feels a bit clumsy, so in particular suggestions on how to rewrite that are very welcome!

[Winston Yin (尹維晨)]

Very nice! Some minor comments:

1. Pmf should be spelt PMF, following rule 6 of the naming convention
2. There's a dedicated docs#PMF type. Maybe state your definition/results in terms of that?

I'm not familiar with this part of the library, so I cannot offer more detailed advice.

Question to those who are familiar: why is docs#PMF a subtype and not a structure?

[Winston Yin (尹維晨)]

Same comments apply to your other thread

[Josha Dekker]

Thanks! I use the dedicated type PMF around line 70, but I first set up the PMF as a real function in the file, to have a somewhat more workable object!

[Josha Dekker]

So I know that we also write Pdf (the continuous analogue) instead of PDF/pdf in Probability/Distributions/Exponential, should we be consistent and write PDF everywhere? In my PR, I have e.g. geometricPdfReal, should that (and such names) become geometricPDFReal (in which case it becomes harder to parse visually for me) or geometricPDF_Real in this case? I'm happy to fix this for the exponential and gamma distributions as well, let me know what you think!

[Josha Dekker]

when I'm looking at the definitions of e.g. the cgf and pgf in Probability/Moments, I'd think that it would perhaps be more consistent to write pmf rather than PMF?

[Winston Yin (尹維晨)]

Pdf should be PDF also when used in camelCase. PMF is a type, so it’s capitalised. Terms of PMF should be named in camelCase, which could be for example pmfPoisson or poissonPMF

[Winston Yin (尹維晨)]

So, geometricPDFReal

[Winston Yin (尹維晨)]

If you have to rename a bunch of things it’s probably best to open another PR for renames only.

[Josha Dekker]

okay, let me do a renaming sweep of all the files in Probability/Distributions/ after the other PRs that I have open have merged!

[Winston Yin (尹維晨)]

Ah yes, I miss the part where you defined a PMF. Consistent naming sounds good!

[Josha Dekker]

Great! I have 3 PR's running that all deal with stuff in Probability/Distributions/ which I expect to not take too long to get accepted (#9462, #9554, #9561), all of which deal with files that probably need some renaming, so I'll need to wait for them to be merged; then I'll open a PR with renaming!