Why are uniform random variables in the pdf namespace?

Stream: mathlib4

[Etienne Marion]

Following #new members > Handling Probability with Uniform variables on I I want to add a bit of API to MeasureTheory.pdf.IsUniform, and also refactor it to use ProbabilityTheory.HasLaw. But I was surprised to see that this is in the MeasureTheory.pdf namespace, I think it would make much more sense to have it in the ProbabilityTheory namespace. I am checking here whether anyone disagrees, otherwise I'll do the change.

[Kexing Ying]

I think the only reason was that pdf was defined before HasLaw so it went into the pdf namespace. I agree that HasLaw makes a lot more sense

[Etienne Marion]

To be clear I don't think it should be ProbabilityTheory.HasLaw.IsUniform, but rather just ProbabilityTheory.IsUniform.

[Etienne Marion]

But I plan to use HasLaw in the definition instead of equality of the map.