Euclidean cross-sections inside an affine subspace

This file contains one temporary support theorem adapted from mathlib PR #37910 by Weiyi Wang:

https://github.com/leanprover-community/mathlib4/pull/37910

The theorem extends the existing full-dimensional Hausdorff-measure slicing formula to a set contained in a lower-dimensional affine subspace. This is the form needed for the standard simplex, whose affine hull is a hyperplane in its ambient coordinate space.

TODO: If PR #37910 is merged into Mathlib, remove this file and replace uses of euclideanHausdorffMeasure_eq_lintegral_of_subset_affineSubspace by the upstream theorem EuclideanGeometry.euclideanHausdorffMeasure_eq_lintegral'.

theorem EuclideanGeometry.euclideanHausdorffMeasure_eq_lintegral_of_subset_affineSubspace {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [MetricSpace P] [NormedAddTorsor V P] [MeasurableSpace P] [BorelSpace P] (p : P) {v : V} (hv : v ≠ 0) {t : Set P} (ht : MeasurableSet t) {s : AffineSubspace ℝ P} (hvs : v ∈ s.direction) (hts : t ⊆ ↑s) [FiniteDimensional ℝ ↥s.direction] : (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ ↥s.direction)) t = ‖v‖ₑ * ∫⁻ (x : ℝ), (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ ↥s.direction - 1)) (t ∩ ↑(AffineSubspace.mk' (x • v +ᵥ p) (ℝ ∙ v)ᗮ))

Hausdorff measure of a measurable set contained in an affine subspace, expressed as the integral of its perpendicular cross-sections along a line in that subspace.

This proof is adapted from EuclideanGeometry.euclideanHausdorffMeasure_eq_lintegral' in mathlib PR #37910.