# 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.

def SmoothBumpCovering.embeddingPiTangent {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] [] [hi : ] {s : Set M} (f : ) :
ContMDiffMap I (modelWithCornersSelf (ιE × )) M (ιE × )

Smooth embedding of M into (E × ℝ) ^ ι.

Equations
• f.embeddingPiTangent = fun (x : M) (i : ι) => ((f.toFun i) x (extChartAt I (f.c i)) x, (f.toFun i) x),
Instances For
theorem SmoothBumpCovering.embeddingPiTangent_coe {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] [] [hi : ] {s : Set M} (f : ) :
f.embeddingPiTangent = fun (x : M) (i : ι) => ((f.toFun i) x (extChartAt I (f.c i)) x, (f.toFun i) x)
theorem SmoothBumpCovering.embeddingPiTangent_injOn {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] [] [hi : ] {s : Set M} (f : ) :
Set.InjOn (f.embeddingPiTangent) s
theorem SmoothBumpCovering.embeddingPiTangent_injective {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] [] [hi : ] (f : ) :
Function.Injective f.embeddingPiTangent
theorem SmoothBumpCovering.comp_embeddingPiTangent_mfderiv {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] [] [hi : ] {s : Set M} (f : ) (x : M) (hx : x s) :
(.comp (ContinuousLinearMap.proj (f.ind x hx))).comp (mfderiv I (modelWithCornersSelf (ιE × )) (f.embeddingPiTangent) x) = mfderiv I I ((chartAt H (f.c (f.ind x hx)))) x
theorem SmoothBumpCovering.embeddingPiTangent_ker_mfderiv {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] [] [hi : ] {s : Set M} (f : ) (x : M) (hx : x s) :
LinearMap.ker (mfderiv I (modelWithCornersSelf (ιE × )) (f.embeddingPiTangent) x) =
theorem SmoothBumpCovering.embeddingPiTangent_injective_mfderiv {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] [] [hi : ] {s : Set M} (f : ) (x : M) (hx : x s) :
Function.Injective (mfderiv I (modelWithCornersSelf (ιE × )) (f.embeddingPiTangent) x)
theorem SmoothBumpCovering.exists_immersion_euclidean {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] [] [] (f : ) :
∃ (n : ) (e : M), Smooth I () e ∀ (x : M), Function.Injective (mfderiv I () 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} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] [] [] :
∃ (n : ) (e : M), Smooth I () e ∀ (x : M), Function.Injective (mfderiv I () 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.