Whitney embedding theorem

In this file we prove a version of the Whitney embedding theorem: for any compact real manifold M, for sufficiently large n there exists a smooth embedding M → ℝ^n.

TODO

• Prove the weak Whitney embedding theorem: any σ-compact smooth m-dimensional manifold can be embedded into ℝ^(2m+1). This requires a version of Sard's theorem: for a locally Lipschitz continuous map f : ℝ^m → ℝ^n, m < n, the range has Hausdorff dimension at most m, hence it has measure zero.

Tags

partition of unity, smooth bump function, whitney theorem

Whitney embedding theorem

In this section we prove a version of the Whitney embedding theorem: for any compact real manifold M, for sufficiently large n there exists a smooth embedding M → ℝ^n.

theorem SmoothBumpCovering.exists_immersion_euclidean {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] {ι : Type u_1} [Finite ι] (f : SmoothBumpCovering ι I M) : ∃ (n : ℕ) (e : M → EuclideanSpace ℝ (Fin n)), ContMDiff I (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (↑⊤) e ∧ Function.Injective e ∧ ∀ (x : M), Function.Injective ⇑(mfderiv% e x)

Baby version of the Whitney weak embedding theorem: if M admits a finite covering by supports of bump functions, then for some n it can be immersed into the n-dimensional Euclidean space.

theorem exists_embedding_euclidean_of_compact {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [CompactSpace M] : ∃ (n : ℕ) (e : M → EuclideanSpace ℝ (Fin n)), ContMDiff I (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (↑⊤) e ∧ Topology.IsClosedEmbedding e ∧ ∀ (x : M), Function.Injective ⇑(mfderiv% e x)

Baby version of the Whitney weak embedding theorem: if M admits a finite covering by supports of bump functions, then for some n it can be embedded into the n-dimensional Euclidean space.