Commit 2025-06-20 12:59 372e50b2

feat(MeasureTheory/Measure): bound Hausdorff measure under orthogonal projection (#25759) Formalisation that Hausdorff measure is non-increasing under orthogonal projection onto a finite-dimensional Euclidean subspace. This includes:

• a bound on the norm of orthogonal projections;
• a proof that orthogonal projection is 1-Lipschitz;
• the main result: the s-dimensional Hausdorff measure of the projection of a set is less than or equal to that of the original set. This formalises Lemma 3.5 from Julian Fox’s REU paper:
  Besicovitch Sets, Kakeya Sets, and Their Properties, UChicago REU, 2021.
  https://math.uchicago.edu/~may/REU2021/REUPapers/Fox.pdf