Commit 2025-11-15 01:45 1631dc15

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 theMeasureTheory 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 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.