English
Let K be a subspace of a real inner product space E with an orthogonal projection. For all d ≥ 0, the d-dimensional Hausdorff measure of the orthogonal projection of any set s onto K is at most the d-dimensional Hausdorff measure of s: μ_H[d](K.orthogonalProjection '' s) ≤ μ_H[d] s.
Русский
Пусть K подпространство векторного пространства E с сквозным скалярным произведением. Проекция вдоль K не увеличивает размерность меры: μ_H[d](K.orthogonalProjection '' s) ≤ μ_H[d] s при d ≥ 0.
LaTeX
$$$\mu\!\_{H}^{d}(K.orthogonalProjection '' s) \leq \mu\!\_{H}^{d} s$ for d ≥ 0.$$
Lean4
/-- Let `s` be a subset of `𝕜`-inner product space, and `K` a subspace. Then the `d`-dimensional
Hausdorff measure of the orthogonal projection of `s` onto `K` is less than or equal to the
`d`-dimensional Hausdorff measure of `s`.
-/
theorem hausdorffMeasure_orthogonalProjection_le [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
[MeasurableSpace E] [BorelSpace E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (d : ℝ) (s : Set E)
(hs : 0 ≤ d) : μH[d] (K.orthogonalProjection '' s) ≤ μH[d] s := by
simpa using K.lipschitzWith_orthogonalProjection.hausdorffMeasure_image_le hs s
