Disc sublevels at nondegenerate extrema

Near a nondegenerate minimum, small closed sublevels are closed Euclidean discs. Near a nondegenerate maximum the analogous statement holds for superlevels. The homeomorphisms retain the value of the function as the squared radial coordinate; for positive radii the endpoint level corresponds to the boundary sphere.

For a unique global minimum, one compact sublevel strictly above the minimum suffices to make this a description of the whole small sublevel, not just its intersection with a chart. No properness, global Morse condition, metric on the manifold, or compactness of the manifold is required. All statements include zero-dimensional manifolds.

The local construction uses the normalized Morse charts of TauCeti.IsManifoldNondegenerateCriticalPoint.exists_normalized_morseChart.

References

• J. Milnor, Morse Theory, Princeton University Press, 1963, Sections 2 and 3.

theorem TauCeti.IsManifoldNondegenerateCriticalPoint.exists_local_sublevel_homeomorph_closedBall {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {x : M} [IsManifold I (↑⊤) M] (hf : ∀ᶠ (y : M) in nhds x, ContMDiffAt I (modelWithCornersSelf ℝ ℝ) (↑⊤) f y) (h : IsManifoldNondegenerateCriticalPoint I f x) (hidx : manifoldMorseIndex I f x = 0) : ∃ (U : Set M), IsOpen U ∧ x ∈ U ∧ ∃ R > 0, ∀ (r : ℝ), 0 ≤ r → r < R → ∃ (e : { y : M // y ∈ U ∧ f y ≤ f x + r ^ 2 } ≃ₜ ↑(Metric.closedBall 0 r)), ∀ (y : { y : M // y ∈ U ∧ f y ≤ f x + r ^ 2 }), f ↑y = f x + ‖↑(e y)‖ ^ 2

A neighbourhood of a nondegenerate critical point of index zero has small closed sublevels homeomorphic to closed Euclidean discs. The function is its minimum value plus the squared radial coordinate. The radius-zero case is included.

theorem TauCeti.IsManifoldNondegenerateCriticalPoint.exists_sublevel_component_homeomorph_closedBall {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {x : M} [IsManifold I (↑⊤) M] [T2Space M] (hf : ∀ᶠ (y : M) in nhds x, ContMDiffAt I (modelWithCornersSelf ℝ ℝ) (↑⊤) f y) (h : IsManifoldNondegenerateCriticalPoint I f x) (hidx : manifoldMorseIndex I f x = 0) : ∃ R > 0, ∀ (r : ℝ), 0 ≤ r → r < R → Nonempty (↑(connectedComponentIn {y : M | f y ≤ f x + r ^ 2} x) ≃ₜ ↑(Metric.closedBall 0 r))

On a Hausdorff manifold, the component of a sufficiently small sublevel containing a nondegenerate index-zero critical point is a closed Euclidean disc.

theorem TauCeti.IsManifoldNondegenerateCriticalPoint.exists_local_superlevel_homeomorph_closedBall {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {x : M} [IsManifold I (↑⊤) M] (hf : ∀ᶠ (y : M) in nhds x, ContMDiffAt I (modelWithCornersSelf ℝ ℝ) (↑⊤) f y) (h : IsManifoldNondegenerateCriticalPoint I f x) (hidx : manifoldMorseIndex I f x = Module.finrank ℝ E) : ∃ (U : Set M), IsOpen U ∧ x ∈ U ∧ ∃ R > 0, ∀ (r : ℝ), 0 ≤ r → r < R → ∃ (e : { y : M // y ∈ U ∧ f x - r ^ 2 ≤ f y } ≃ₜ ↑(Metric.closedBall 0 r)), ∀ (y : { y : M // y ∈ U ∧ f x - r ^ 2 ≤ f y }), f ↑y = f x - ‖↑(e y)‖ ^ 2

Near a nondegenerate critical point of full Morse index, small closed superlevels are closed discs, with the deficit from the maximum equal to the squared radial coordinate.

theorem TauCeti.IsManifoldNondegenerateCriticalPoint.exists_sublevel_homeomorph_closedBall {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {x : M} [IsManifold I (↑⊤) M] (hf : ∀ᶠ (y : M) in nhds x, ContMDiffAt I (modelWithCornersSelf ℝ ℝ) (↑⊤) f y) (h : IsManifoldNondegenerateCriticalPoint I f x) {a : ℝ} (hcompact : IsCompact {y : M | f y ≤ a}) (hcont : ContinuousOn f {y : M | f y ≤ a}) (ha : f x < a) (hmin : ∀ (y : M), f y ≤ f x → y = x) : ∃ R > 0, ∀ (r : ℝ), 0 ≤ r → r < R → ∃ (e : { y : M // f y ≤ f x + r ^ 2 } ≃ₜ ↑(Metric.closedBall 0 r)), ∀ (y : { y : M // f y ≤ f x + r ^ 2 }), f ↑y = f x + ‖↑(e y)‖ ^ 2

If a function has a unique global minimum at a nondegenerate critical point and one compact sublevel strictly above it on which it is continuous, all sufficiently small whole sublevels are closed discs. The radial coordinate records the function value.

theorem TauCeti.IsManifoldNondegenerateCriticalPoint.exists_superlevel_homeomorph_closedBall {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {x : M} [IsManifold I (↑⊤) M] (hf : ∀ᶠ (y : M) in nhds x, ContMDiffAt I (modelWithCornersSelf ℝ ℝ) (↑⊤) f y) (h : IsManifoldNondegenerateCriticalPoint I f x) {a : ℝ} (hcompact : IsCompact {y : M | a ≤ f y}) (hcont : ContinuousOn f {y : M | a ≤ f y}) (ha : a < f x) (hmax : ∀ (y : M), f x ≤ f y → y = x) : ∃ R > 0, ∀ (r : ℝ), 0 ≤ r → r < R → ∃ (e : { y : M // f x - r ^ 2 ≤ f y } ≃ₜ ↑(Metric.closedBall 0 r)), ∀ (y : { y : M // f x - r ^ 2 ≤ f y }), f ↑y = f x - ‖↑(e y)‖ ^ 2

The dual of IsManifoldNondegenerateCriticalPoint.exists_sublevel_homeomorph_closedBall: if a function has a unique global maximum at a nondegenerate critical point and one compact superlevel strictly below it on which it is continuous, all sufficiently small whole superlevels are closed discs. The radial coordinate records the function value, subtracted from the maximum value.