doc(Probability): ensure only a single H1 header per file (#31659)

This PR ensures we only have a single H1 header per lean file in the `Probability` subdirectory. We do this for the following reasons:

- Having more than one H1 header per file is likely to hamper both assistive technologies and SEO, since it introduces ambiguity about what the title of the resulting documentation webpage actually is.
- The [documentation style guide](https://leanprover-community.github.io/contribute/doc.html) asks for the title of the file to be H1, any other header in the file-level docstring to be H2, and sectioning headers to be H3.

Author: harahu

Mathlib/Probability/Distributions/Uniform.lean

@@ -12,20 +12,20 @@ import Mathlib.Probability.ProbabilityMassFunction.Constructions
 # Uniform distributions and probability mass functions
 This file defines two related notions of uniform distributions, which will be unified in the future.
 
-# Uniform distributions
+## Uniform distributions
 
 Defines the uniform distribution for any set with finite measure.
 
-## Main definitions
+### Main definitions
 * `IsUniform X s ℙ μ` : A random variable `X` has uniform distribution on `s` under `ℙ` if the
   push-forward measure agrees with the rescaled restricted measure `μ`.
 
-# Uniform probability mass functions
+## Uniform probability mass functions
 
 This file defines a number of uniform `PMF` distributions from various inputs,
   uniformly drawing from the corresponding object.
 
-## Main definitions
+### Main definitions
 `PMF.uniformOfFinset` gives each element in the set equal probability,
   with `0` probability for elements not in the set.