Embedded Manifold Geometry

Proves that C² smooth embeddings of manifolds have local graph representations (via the inverse function theorem), and that general tubular neighborhoods yield the IsTubularNeighborhoodOfSubmanifold structure.

Main results

• exists_general_tubular_subneighborhood — For C² embedded submanifolds contained in an open set, construct a smaller general tubular neighborhood.
• general_tubular_of_smooth_embedding — For C² embedded submanifolds, a general tubular neighborhood directly gives the IsTubularNeighborhoodOfSubmanifold structure.
• general_to_metric_tubular — For compact C² embedded submanifolds, a general tubular neighborhood can be refined to a metric tubular sub-neighborhood.

Auxiliary lemmas

theorem PLAcceleratedNesterovLean.exists_tubular_subneighborhood_of_c3_pl {d : ℕ} (hd : 0 < d) {f : E d → ℝ} {μ : ℝ} {U : Set (E d)} (hU_open : IsOpen U) (hS_sub : argminSet f ⊆ U) (hPL : PolyakLojasiewicz f μ U) (hf_C3 : ContDiffOn ℝ 3 f U) : ∃ (U' : Set (E d)), IsOpen U' ∧ argminSet f ⊆ U' ∧ U' ⊆ U ∧ IsGeneralTubularNeighborhood (argminSet f) U' ∧ IsTubularNeighborhoodOfSubmanifold (argminSet f) U'

C³+PL on an open neighborhood of the minimizer set gives a smaller tubular sub-neighborhood of the minimizer set.

theorem PLAcceleratedNesterovLean.exists_general_tubular_subneighborhood {d n : ℕ} (M : Type u_1) [TopologicalSpace M] [ChartedSpace (ManifoldModel n) M] [IsManifold (modelI n) 2 M] (ι : M → E d) (hι : Manifold.IsSmoothEmbedding (modelI n) (modelWithCornersSelf ℝ (E d)) 2 ι) (U : Set (E d)) (hU_open : IsOpen U) (hS_sub : Set.range ι ⊆ U) : ∃ (U' : Set (E d)), IsOpen U' ∧ Set.range ι ⊆ U' ∧ U' ⊆ U ∧ IsGeneralTubularNeighborhood (Set.range ι) U'

A C² smooth embedded submanifold contained in an open set admits a smaller general tubular neighborhood contained in that open set.

theorem PLAcceleratedNesterovLean.general_to_metric_tubular {d n : ℕ} (M : Type u_1) [TopologicalSpace M] [ChartedSpace (ManifoldModel n) M] [IsManifold (modelI n) 2 M] [CompactSpace M] [Nonempty M] (ι : M → E d) (hι : Manifold.IsSmoothEmbedding (modelI n) (modelWithCornersSelf ℝ (E d)) 2 ι) (U : Set (E d)) (hU : IsGeneralTubularNeighborhood (Set.range ι) U) : ∃ (U' : Set (E d)), IsOpen U' ∧ Set.range ι ⊆ U' ∧ U' ⊆ U ∧ IsTubularNeighborhoodOfSubmanifold (Set.range ι) U'

For compact C² embedded submanifolds, a general tubular neighborhood can be refined to a metric tubular neighborhood with C² chart structure.

theorem PLAcceleratedNesterovLean.general_tubular_of_smooth_embedding {d n : ℕ} (M : Type u_1) [TopologicalSpace M] [ChartedSpace (ManifoldModel n) M] [IsManifold (modelI n) 2 M] (ι : M → E d) (hι : Manifold.IsSmoothEmbedding (modelI n) (modelWithCornersSelf ℝ (E d)) 2 ι) (U : Set (E d)) (hU : IsGeneralTubularNeighborhood (Set.range ι) U) : IsTubularNeighborhoodOfSubmanifold (Set.range ι) U

For C² embedded submanifolds, a general tubular neighborhood yields IsTubularNeighborhoodOfSubmanifold — the submanifold charts come from the pointwise IFT.