English
In the setting of an inner-product space, the Hausdorff dimension of the projection of a set onto a subspace is controlled by the dimension of the original set.
Русский
В пространстве с скалярами по скалярному произведению размерность проекции множества на подпространство не превышает размерность исходного множества.
LaTeX
$$dimH ( K.orthogonalProjection '' s ) ≤ dimH s$$
Lean4
/-- The Hausdorff dimension of the orthogonal projection of a set `s` onto a subspace `K`
is less than or equal to the Hausdorff dimension of `s`.
-/
theorem dimH_orthogonalProjection_le {𝕜 E : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
(K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (s : Set E) : dimH (K.orthogonalProjection '' s) ≤ dimH s :=
K.lipschitzWith_orthogonalProjection.dimH_image_le s
