diracProba

Stream: mathlib4

[Kim Morrison]

@Kalle Kytölä, @Rémy Degenne, I just noticed we have the declaration diracProba, introduced way back in #11815.

I think this sort of abbreviation is contrary to the naming scheme; there don't seem to be any other abbreviations of "Probability" to "Proba". Could this be fixed?

[Rémy Degenne]

We have a number of lemmas that use prob to refer to a Measure with the property IsProbabilityMeasure. diracProba is not in that case: it's a ProbabilityMeasure. We don't have other objects of that type named iirc. Perhaps diracProb would be better then?

[Rémy Degenne]

Or since the Measure def is Measure.dirac, perhaps ProbabilityMeasure.dirac.

[Yaël Dillies]

My vote goes to ProbabilityMeasure.dirac

[Yaël Dillies]

"proba" is the (canonical?) French abbreviation for "probability"

[Kalle Kytölä]

(The fact that "proba" is used by essentially all French probabilists I know definitely played a role in my original naming choice, but I do think that consistency of Mathlib naming is a more important goal.)

Among the suggestions, I find ProbabilityMeasure.dirac the most compelling, since (with my limited understanding of Mathlib naming) it seems consistent with a lot of Mathlib naming. I will just note that since ProbabilityMeasure is already in the namespace MeasureTheory, the full name MeasureTheory.ProbabilityMeasure.dirac starts to become fairly long. I guess we can expect people to have the at least the MeasureTheory namespace open when they use this, so probably that is not an issue. I am in favor of renaming to that.