doc(MeasureTheory): ensure only a single H1 header per file (#31618)

This PR ensures we only have a single H1 header per lean file in the`MeasureTheory` 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.

I have used my own judgement to decide whether to demote the extra H1 headers to H2 or H3. I ask reviewers to verify that my choices makes sense to them.

Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

Author: harahu

Mathlib/MeasureTheory/Function/UnifTight.lean

@@ -21,7 +21,7 @@ is also proved later in the file.
   exists some measurable set `s` with finite measure such that the Lp-norm of
   `f i` restricted to `sᶜ` is smaller than `ε` for all `i`.
 
-# Main results
+## Main results
 
 * `MeasureTheory.unifTight_finite`: a finite sequence of Lp functions is uniformly
   tight.

Mathlib/MeasureTheory/Function/UniformIntegrable.lean

@@ -28,7 +28,7 @@ formulate the martingale convergence theorem.
   probability theory sense if it is uniformly integrable in the measure theory sense and
   has uniformly bounded Lp-norm.
 
-# Main results
+## Main results
 
 * `MeasureTheory.unifIntegrable_finite`: a finite sequence of Lp functions is uniformly
   integrable.

Mathlib/MeasureTheory/Integral/CircleAverage.lean

@@ -38,7 +38,7 @@ variable
 namespace Real
 
 /-!
-# Definition
+### Definition
 -/
 
 variable (f c R) in

Mathlib/MeasureTheory/Measure/HasOuterApproxClosedProd.lean

@@ -24,7 +24,7 @@ such that for any two families bounded continuous functions
 
 We specialize these results to the cases where one of the families contains only one type.
 
-# Main statements
+## Main statements
 
 * `ext_of_integral_prod_mul_prod_boundedContinuousFunction`: A finite measure `μ`
   over `(Π i, X i) × (Π j, Y j)` is determined by the values
@@ -46,7 +46,7 @@ We specialize these results to the cases where one of the families contains only
   `ν` is the only finite measure `ξ` such that for all real bounded continuous functions
   `f` and `g` we have `∫ z, f z.1 * g z.2 ∂ξ = ∫ x, f x ∂μ * ∫ y, g y ∂ν`.
 
-# Tags
+## Tags
 
 bounded continuous function, product measure
 -/

Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

@@ -386,7 +386,7 @@ section
 open MeasureTheory
 
 /-!
-# Almost everywhere measurable functions
+### Almost everywhere measurable functions
 
 A function is almost everywhere measurable if it coincides almost everywhere with a measurable
 function. We define this property, called `AEMeasurable f μ`. It's properties are discussed in