Morse functions, sublevel topology and Morse–Bott attachments

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremThe Lusternik–Schnirelmann theorem#

On a compact boundaryless manifold M, the Lusternik–Schnirelmann count of M is at most the number of critical points of any smooth function on M. The critical points may be degenerate; if there are infinitely many, their count is ⊤.

TauCeti.lsCategoryCount_univ_le_totalCriticalCount.{u_1, u_2, u_3} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ}
  [FiniteDimensional ℝ E] [T2Space M] [I.Boundaryless] [IsManifold I (↑⊤) M] [CompactSpace M]
  (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) :
  TauCeti.lsCategoryCount M Set.univ ≤ TauCeti.totalCriticalCount I f
Lean

Formalized in Tau Ceti as TauCeti.lsCategoryCount_univ_le_totalCriticalCount.

Sources
LeanTauCeti.lsCategoryCount_univ_le_totalCriticalCount
Uses 1 · Used by 1
Proof usesThe Lusternik–Schnirelmann bound on sublevels
Used byThe Lusternik–Schnirelmann lower bound for c(M)

TheoremDeformation of sublevels across a band without critical points (Milnor, Theorem 3.1)#

If f is smooth, a ≤ b, and the band f⁻¹[a, b] is compact and contains no critical point of f, then the sublevel {f ≤ a} is a strong deformation retract of {f ≤ b}: there is a retraction r of {f ≤ b} onto {f ≤ a} and a homotopy from the inclusion of r to the identity fixing {f ≤ a} pointwise.

TauCeti.exists_sublevelDeformation.{u_1, u_2, u_3} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M]
  [I.Boundaryless] [IsManifold I (↑⊤) M] {f : M → ℝ} {a b : ℝ}
  (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hab : a ≤ b)
  (hcompact : IsCompact (f ⁻¹' Set.Icc a b))
  (hreg : ∀ (x : M), a ≤ f x → f x ≤ b → mfderiv% f x ≠ 0) :
  ∃ r,
    (∀ (x : ↑{x | f x ≤ a}), r ((TauCeti.sublevelInclusion f a b hab) x) = x) ∧
      Nonempty
        (((TauCeti.sublevelInclusion f a b hab).comp r).HomotopyRel
          (ContinuousMap.id ↑{x | f x ≤ b}) {x | f ↑x ≤ a})
Lean

Formalized in Tau Ceti as TauCeti.exists_sublevelDeformation.

Sources
LeanTauCeti.exists_sublevelDeformation
Used by 5
Used byAndreotti–Frankel theorem for proper holomorphic immersions · Milnor's cell attachment theorem · The Morse polynomial identity (TauCeti.IsMorse.exists_sum_range_monomial_eq_add_mul) · The strong Morse inequalities (TauCeti.IsMorse.sum_range_neg_one_pow_mul_finrank_singularHomology_le) · The weak Morse inequalities

TheoremSublevels on either side of a band without critical points are diffeomorphic (Milnor, Theorem 3.1)#

If f is smooth, a ≤ b, and the band f⁻¹[a, b] is compact and contains no critical point of f, then there is a diffeomorphism Φ of M carrying the sublevel {f ≤ b} onto {f ≤ a} and the level f⁻¹(b) onto f⁻¹(a).

TauCeti.exists_diffeomorph_sublevel.{u_1, u_2, u_3} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M]
  [I.Boundaryless] [IsManifold I (↑⊤) M] {f : M → ℝ} {a b : ℝ}
  (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hab : a ≤ b)
  (hcompact : IsCompact (f ⁻¹' Set.Icc a b))
  (hreg : ∀ (x : M), a ≤ f x → f x ≤ b → mfderiv% f x ≠ 0) :
  ∃ Φ, ∀ (x : M), (f (Φ x) ≤ a ↔ f x ≤ b) ∧ (f (Φ x) = a ↔ f x = b)
Lean

Formalized in Tau Ceti as TauCeti.exists_diffeomorph_sublevel.

Sources
LeanTauCeti.exists_diffeomorph_sublevel
Used by 1
Used byReeb's theorem (Milnor, *Morse Theory*, Theorem 4.1)

TheoremThe normalized Morse lemma on a manifold#

At a nondegenerate critical point x of a function f which is smooth near x, on a manifold with a boundaryless model, there is a partial diffeomorphism ψ onto an open subset of EuclideanSpace ℝ (Fin m), m = dim M, with ψ x = 0 and

f y = f x - Σ_{i < λ} (ψ y)ᵢ² + Σ_{i ≥ λ} (ψ y)ᵢ²

on its whole source, where λ is the manifold Morse index of f at x.

TauCeti.IsManifoldNondegenerateCriticalPoint.exists_normalized_morseChart.{u_1, u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2}
  {M : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless]
  [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {f : M → ℝ} {x : M}
  (hf : ∀ᶠ (y : M) in nhds x, ContMDiffAt I (modelWithCornersSelf ℝ ℝ) (↑⊤) f y)
  (h : TauCeti.IsManifoldNondegenerateCriticalPoint I f x) :
  ∃ ψ,
    x ∈ ψ.source ∧
      ↑ψ.toPartialEquiv x = 0 ∧
        ∀ y ∈ ψ.source,
          f y =
            f x +
              ∑ i,
                (if ↑i < TauCeti.manifoldMorseIndex I f x then -1 else 1) *
                  (↑ψ.toPartialEquiv y).ofLp i ^ 2
Lean

Formalized in Tau Ceti as TauCeti.IsManifoldNondegenerateCriticalPoint.exists_normalized_morseChart.

Other forms

The normalized Morse lemma. Formalized in Tau Ceti as TauCeti.MorseChart.eq_quadratic_normalizedChart.

TauCeti.MorseChart.eq_quadratic_normalizedChart.{u_1, u_2} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] {f : M → ℝ} {x : M}
  (φ : TauCeti.MorseChart E f x) [FiniteDimensional ℝ E] {y : M} (hy : y ∈ φ.toChart.source) :
  f y =
    f x +
      ∑ i,
        (if ↑i < TauCeti.manifoldMorseIndex (modelWithCornersSelf ℝ E) f x then -1 else 1) *
          (↑φ.normalizedChart.toPartialEquiv y).ofLp i ^ 2

The normalized Morse lemma in a prescribed neighbourhood. Formalized in Tau Ceti as TauCeti.IsManifoldNondegenerateCriticalPoint.exists_normalized_morseChart_subset.

TauCeti.IsManifoldNondegenerateCriticalPoint.exists_normalized_morseChart_subset.{u_1, u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2}
  {M : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless]
  [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {f : M → ℝ} {x : M}
  (hf : ∀ᶠ (y : M) in nhds x, ContMDiffAt I (modelWithCornersSelf ℝ ℝ) (↑⊤) f y)
  (h : TauCeti.IsManifoldNondegenerateCriticalPoint I f x) {U : Set M} (hU : U ∈ nhds x) :
  ∃ ψ,
    x ∈ ψ.source ∧
      ψ.source ⊆ U ∧
        ↑ψ.toPartialEquiv x = 0 ∧
          ∀ y ∈ ψ.source,
            f y =
              f x +
                ∑ i,
                  (if ↑i < TauCeti.manifoldMorseIndex I f x then -1 else 1) *
                    (↑ψ.toPartialEquiv y).ofLp i ^ 2
Sources
LeanTauCeti.IsManifoldNondegenerateCriticalPoint.exists_normalized_morseChart · TauCeti.MorseChart.eq_quadratic_normalizedChart · TauCeti.IsManifoldNondegenerateCriticalPoint.exists_normalized_morseChart_subset
Uses 1 · Used by 2
Proof usesThe Morse lemma on a manifold
Used byAdmissible Morse charts at a critical level · Reeb's theorem (Milnor, *Morse Theory*, Theorem 4.1)

TheoremA trajectory converging to a nondegenerate critical point converges exponentially fast in the Riemannian distance#

If the maximal integral curve γ of -grad f through x exists for all positive time and converges to a nondegenerate critical point p, then the Riemannian distance from γ t to p is at most C * exp (-μ * t) for some μ, C > 0 and all large t. This is the manifold counterpart, for an arbitrary C¹ metric, of the vector-space theorem IsIntegralCurveOn.exists_norm_sub_le_mul_exp_atTop.

TauCeti.exists_riemannianEDist_le_mul_exp_maximalIntegralCurve_neg_mgradient.{u_1, u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2}
  [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M]
  [ChartedSpace H M] [T2Space M] [IsManifold I 2 M] [BoundarylessManifold I M]
  [Bundle.RiemannianBundle fun x => TangentSpace I x]
  [IsContMDiffRiemannianBundle I 1 E fun x => TangentSpace I x] {f : M → ℝ} {x p : M}
  (hp : TauCeti.IsManifoldNondegenerateCriticalPoint I f p)
  (hx : Set.Ici 0 ⊆ maximalIntegralCurveInterval (-TauCeti.Manifold.mgradient I f) x)
  (hconv :
    Filter.Tendsto (maximalIntegralCurve (-TauCeti.Manifold.mgradient I f) x) Filter.atTop (nhds p))
  (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) :
  ∃ μ > 0,
    ∃ C > 0,
      ∀ᶠ (t : ℝ) in Filter.atTop,
        Manifold.riemannianEDist I (maximalIntegralCurve (-TauCeti.Manifold.mgradient I f) x t) p ≤
          ENNReal.ofReal (C * Real.exp (-(μ * t)))
Lean

Formalized in Tau Ceti as TauCeti.exists_riemannianEDist_le_mul_exp_maximalIntegralCurve_neg_mgradient.

Sources
LeanTauCeti.exists_riemannianEDist_le_mul_exp_maximalIntegralCurve_neg_mgradient
Uses 1
Proof usesThe Morse form of Łojasiewicz's gradient inequality on a Riemannian manifold

TheoremNegative gradient trajectories of a proper Morse function converge#

If f is a proper Morse function bounded below, the maximal integral curve of -grad f through any point converges to a critical point of f, for any C¹ Riemannian metric.

TauCeti.IsMorse.exists_tendsto_maximalIntegralCurve_neg_mgradient.{u_1, u_2, u_3} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2}
  [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M]
  [ChartedSpace H M] [T2Space M] [IsManifold I 2 M] [BoundarylessManifold I M]
  [Bundle.RiemannianBundle fun x => TangentSpace I x]
  [IsContMDiffRiemannianBundle I 1 E fun x => TangentSpace I x] {f : M → ℝ} [I.Boundaryless]
  (hf : TauCeti.IsMorse I f) (hp : IsProperMap f) (hbdd : BddBelow (Set.range f)) (x : M) :
  ∃ p ∈ TauCeti.criticalPoints I f,
    Filter.Tendsto (maximalIntegralCurve (-TauCeti.Manifold.mgradient I f) x) Filter.atTop (nhds p)
Lean

Formalized in Tau Ceti as TauCeti.IsMorse.exists_tendsto_maximalIntegralCurve_neg_mgradient.

Sources
LeanTauCeti.IsMorse.exists_tendsto_maximalIntegralCurve_neg_mgradient

DefinitionTauCeti.criticalHessian#

The critical Hessian of a real function f at a point x of a manifold: the second derivative at extChartAt I x x of the coordinate expression of f in the preferred extended chart, as a bilinear form on the tangent space at x.

Like TauCeti.manifoldMorseIndex, the definition makes sense at every point and carries no regularity hypotheses. At a critical point of a C² function on a manifold without boundary it is intrinsic: TauCeti.criticalHessian_apply_eq_of_mem_maximalAtlas computes it in an arbitrary chart there. At a noncritical point it depends on the preferred chart, and on a manifold with boundary or corners it may also depend on the chart inverse outside range I.

TauCeti.criticalHessian.{u_1, u_2, u_3} {E : Type u_1} {H : Type u_2} {M : Type u_3}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M]
  [ChartedSpace H M] (I : ModelWithCorners ℝ E H) (f : M → ℝ) (x : M) :
  TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ
Lean

Formalized in Tau Ceti as TauCeti.criticalHessian.

Sources
LeanTauCeti.criticalHessian
Used by 1
Used byAndreotti–Frankel theorem for proper holomorphic immersions

TheoremAdmissible Morse charts at a critical level#

Let f be a Morse function on a Hausdorff manifold whose band f⁻¹[c - δ, c + δ] is compact, for some 0 < δ. Then there are a width 0 < ε ≤ δ and normalized Morse charts ψ p, indexed by the critical points p on the level f⁻¹(c), such that

  • the only critical points in the band f⁻¹[c - ε, c + ε] are those on the level f⁻¹(c);
  • the chart sources are pairwise disjoint, and each lies in a prescribed neighbourhood U p;
  • ψ p p = 0, and f = c - Σ_{i < λ} (ψ p)ᵢ² + Σ_{i ≥ λ} (ψ p)ᵢ² on the source of ψ p, where λ is the Morse index of f at p;
  • the target of each chart contains the closed ball of radius √(2ε) about 0.

The last condition places Milnor's ellipsoid ‖u‖² + 2‖v‖² ≤ 2ε inside every chart. All of these conditions persist when ε is decreased.

TauCeti.IsMorse.exists_admissible_morseCharts.{u_1, u_2, u_3} {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] [IsManifold I (↑⊤) M] {f : M → ℝ} [T2Space M] (hf : TauCeti.IsMorse I f)
  {c δ : ℝ} (hδ : 0 < δ) (hcompact : IsCompact (f ⁻¹' Set.Icc (c - δ) (c + δ))) {U : M → Set M}
  (hU : ∀ x ∈ TauCeti.criticalPoints I f ∩ f ⁻¹' {c}, U x ∈ nhds x) :
  ∃ ε,
    0 < ε ∧
      ε ≤ δ ∧
        TauCeti.criticalPoints I f ∩ f ⁻¹' Set.Icc (c - ε) (c + ε) ⊆ f ⁻¹' {c} ∧
          ∃ ψ,
            Pairwise (Function.onFun Disjoint fun p => (ψ p).source) ∧
              ∀ (p : ↑(TauCeti.criticalPoints I f ∩ f ⁻¹' {c})),
                ↑p ∈ (ψ p).source ∧
                  (ψ p).source ⊆ U ↑p ∧
                    ↑(ψ p).toPartialEquiv ↑p = 0 ∧
                      Metric.closedBall 0 √(2 * ε) ⊆ (ψ p).target ∧
                        ∀ y ∈ (ψ p).source,
                          f y =
                            c +
                              ∑ i,
                                (if ↑i < TauCeti.manifoldMorseIndex I f ↑p then -1 else 1) *
                                  (↑(ψ p).toPartialEquiv y).ofLp i ^ 2
Lean

Formalized in Tau Ceti as TauCeti.IsMorse.exists_admissible_morseCharts.

Sources
LeanTauCeti.IsMorse.exists_admissible_morseCharts
Uses 1 · Used by 1
Proof usesThe normalized Morse lemma on a manifold
Used byMilnor's cell attachment theorem

TheoremMilnor's handle retraction#

If every fibre {v | (u, v) ∈ X} of X is star-shaped about the origin, then X ∩ quadraticSublevelUnionCell ε is a strong deformation retract of X: there is a retraction of X onto it, and a homotopy in X from this retraction to the identity which fixes X ∩ quadraticSublevelUnionCell ε. Both are restrictions of TauCeti.quadraticHandleRetraction ε and TauCeti.quadraticHandleDeformation ε.

TauCeti.exists_inter_quadraticSublevelUnionCell_deformation.{u_1, u_2} {Eᵤ : Type u_1}
  {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] [NormedSpace ℝ Eₛ]
  {X : Set (Eᵤ × Eₛ)} (hX : ∀ (u : Eᵤ), StarConvex ℝ 0 {v | (u, v) ∈ X}) (ε : ℝ) :
  ∃ r,
    (∀ (x : ↑(X ∩ TauCeti.quadraticSublevelUnionCell ε)), r ((ContinuousMap.inclusion ⋯) x) = x) ∧
      Nonempty
        (((ContinuousMap.inclusion ⋯).comp r).HomotopyRel (ContinuousMap.id ↑X)
          {x | ↑x ∈ TauCeti.quadraticSublevelUnionCell ε})
Lean

Formalized in Tau Ceti as TauCeti.exists_inter_quadraticSublevelUnionCell_deformation.

Sources
LeanTauCeti.exists_inter_quadraticSublevelUnionCell_deformation

TheoremFermat's theorem on a manifold#

A local extremum is a critical point.

IsLocalExtr.mem_criticalPoints.{u_1, u_2, u_3} {E : Type u_1} {H : Type u_2} {M : Type u_3}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
  [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {x : M} [I.Boundaryless]
  (h : IsLocalExtr f x) : x ∈ TauCeti.criticalPoints I f
Lean

Formalized in Tau Ceti as IsLocalExtr.mem_criticalPoints.

Sources
LeanIsLocalExtr.mem_criticalPoints
Used by 3
Used byThe boundary of a Liouville domain is of restricted contact type · Reeb's theorem (Milnor, *Morse Theory*, Theorem 4.1) · The Lusternik–Schnirelmann bound on sublevels

TheoremThe Lusternik–Schnirelmann bound on sublevels#

Let f be smooth and t < b, and suppose that the sublevel {f ≤ b} is compact and contains only finitely many critical points of f. Then the Lusternik–Schnirelmann count of {f ≤ t} is at most the number of critical points of f in {f ≤ t}. The critical points may be degenerate.

TauCeti.lsCategoryCount_sublevel_le_encard.{u_1, u_2, u_3} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3}
  [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} [FiniteDimensional ℝ E] [T2Space M]
  [I.Boundaryless] [IsManifold I (↑⊤) M] (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f)
  {t b : ℝ} (htb : t < b) (hb : IsCompact {x | f x ≤ b})
  (hfin : (TauCeti.criticalPoints I f ∩ {x | f x ≤ b}).Finite) :
  TauCeti.lsCategoryCount M {x | f x ≤ t} ≤ (TauCeti.criticalPoints I f ∩ {x | f x ≤ t}).encard
Informally uses
Lean

Formalized in Tau Ceti as TauCeti.lsCategoryCount_sublevel_le_encard.

Other forms

The Lusternik–Schnirelmann bound on a compact open part. Formalized in Tau Ceti as TauCeti.lsCategoryCount_univ_le_encard_criticalPoints_inter.

TauCeti.lsCategoryCount_univ_le_encard_criticalPoints_inter.{u_1, u_2, u_3} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ}
  [FiniteDimensional ℝ E] [T2Space M] [I.Boundaryless] [IsManifold I (↑⊤) M] {C : Set M}
  (hf : ContMDiffOn I (modelWithCornersSelf ℝ ℝ) (↑⊤) f C) (hCo : IsOpen C) (hCc : IsCompact C) :
  TauCeti.lsCategoryCount (↑C) Set.univ ≤ (TauCeti.criticalPoints I f ∩ C).encard
Sources
LeanTauCeti.lsCategoryCount_sublevel_le_encard · TauCeti.lsCategoryCount_univ_le_encard_criticalPoints_inter
Uses 1 · Used by 1
Proof usesFermat's theorem on a manifold
Used byThe Lusternik–Schnirelmann theorem

TheoremThe Lusternik–Schnirelmann lower bound for c(M)#

On a compact boundaryless manifold, every smooth function has at least as many critical points as the Lusternik–Schnirelmann count of M, so c(M) is bounded below by that count.

TauCeti.lsCategoryCount_univ_le_minCriticalCount.{u_1, u_2, u_3} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M]
  [I.Boundaryless] [CompactSpace M] [FiniteDimensional ℝ E] [T2Space M] [IsManifold I (↑⊤) M] :
  TauCeti.lsCategoryCount M Set.univ ≤ TauCeti.minCriticalCount I M
Lean

Formalized in Tau Ceti as TauCeti.lsCategoryCount_univ_le_minCriticalCount.

Sources
LeanTauCeti.lsCategoryCount_univ_le_minCriticalCount
Uses 1
Proof usesThe Lusternik–Schnirelmann theorem

TheoremThe Morse form of Łojasiewicz's gradient inequality on a Riemannian manifold#

Near a nondegenerate critical point p of f, the absolute energy difference |f y - f p| is bounded by a multiple of the squared Riemannian length of the gradient of f at y, for any continuous Riemannian metric.

TauCeti.IsManifoldNondegenerateCriticalPoint.exists_mul_abs_sub_le_norm_mgradient_sq.{u_1, u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2}
  [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M]
  [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun x => TangentSpace I x]
  [IsContinuousRiemannianBundle E fun x => TangentSpace I x] {f : M → ℝ} {p : M}
  (hp : TauCeti.IsManifoldNondegenerateCriticalPoint I f p) :
  ∃ lam > 0, ∀ᶠ (y : M) in nhds p, lam * |f y - f p| ≤ ‖TauCeti.Manifold.mgradient I f y‖ ^ 2
Lean

Formalized in Tau Ceti as TauCeti.IsManifoldNondegenerateCriticalPoint.exists_mul_abs_sub_le_norm_mgradient_sq.

Sources
LeanTauCeti.IsManifoldNondegenerateCriticalPoint.exists_mul_abs_sub_le_norm_mgradient_sq
Uses 1 · Used by 1
Proof usesThe Morse form of Łojasiewicz's gradient inequality
Used byA trajectory converging to a nondegenerate critical point converges exponentially fast in the Riemannian distance

TheoremThe Morse lemma on a manifold#

At a nondegenerate critical point x of a function f that is smooth at every point of a neighbourhood of x, on a manifold modelled on a finite-dimensional real normed space E, there is a Morse chart: a chart ψ of the maximal atlas, centred at x, and a linear change of coordinates L : E ≃ (Fin n → ℝ) such that on the source of ψ

f y = f x + (1/2) Σᵢ wᵢ (L (ψ y))ᵢ²,

where every weight wᵢ is -1 or 1 and the number of negative weights is the manifold Morse index of f at x.

TauCeti.IsManifoldNondegenerateCriticalPoint.nonempty_morseChart.{u_1, u_2} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M]
  {f : M → ℝ} {x : M} [FiniteDimensional ℝ E] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M]
  (hf :
    ∀ᶠ (y : M) in nhds x,
      ContMDiffAt (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ ℝ) (↑⊤) f y)
  (h : TauCeti.IsManifoldNondegenerateCriticalPoint (modelWithCornersSelf ℝ E) f x) :
  Nonempty (TauCeti.MorseChart E f x)
Lean

Formalized in Tau Ceti as TauCeti.IsManifoldNondegenerateCriticalPoint.nonempty_morseChart.

Sources
LeanTauCeti.IsManifoldNondegenerateCriticalPoint.nonempty_morseChart
Uses 1 · Used by 1
Proof usesThe local Morse lemma
Used byThe normalized Morse lemma on a manifold

TheoremThe Morse polynomial identity (TauCeti.IsMorse.exists_sum_range_monomial_eq_add_mul)#

For a Morse function f on a compact boundaryless manifold M, write bᵢ for the dimension of Hᵢ(M; V) and cᵢ for the number of critical points of index i. Then for every n ≥ dim M, ∑ᵢ₌₀ⁿ cᵢ dim V · tⁱ = ∑ᵢ₌₀ⁿ bᵢ tⁱ + (1 + t) Q(t) for a polynomial Q with natural number coefficients. The coefficient of tⁱ in Q is the gap (cᵢ - cᵢ₋₁ + ⋯ ± c₀) dim V - (bᵢ - bᵢ₋₁ + ⋯ ± b₀) in the i-th strong Morse inequality for i < n, and zero for i ≥ n.

TauCeti.IsMorse.exists_sum_range_monomial_eq_add_mul.{u, u_1, u_2} {E : Type u_1} {H : Type u_2}
  {M : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E]
  [I.Boundaryless] [IsManifold I (↑⊤) M] [T2Space M] {f : M → ℝ} {k : Type u} [DivisionRing k]
  (V : ModuleCat k) [Module.Finite k ↑V] [CompactSpace M] (hf : TauCeti.IsMorse I f) {n : ℕ}
  (hn : Module.finrank ℝ E ≤ n) :
  ∃ Q,
    ∑ i ∈ Finset.range (n + 1),
          (Polynomial.monomial i) ((TauCeti.criticalCount I f i).toNat * Module.finrank k ↑V) =
        ∑ i ∈ Finset.range (n + 1),
            (Polynomial.monomial i)
              (Module.finrank k
                ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) i).obj V).obj ↧M)) +
          (1 + Polynomial.X) * Q ∧
      (∀ i < n,
          ↑(Q.coeff i) =
            ↑(Module.finrank k ↑V) *
                ∑ j ∈ Finset.range (i + 1), (-1) ^ (i - j) * ↑(TauCeti.criticalCount I f j).toNat -
              ∑ j ∈ Finset.range (i + 1),
                (-1) ^ (i - j) *
                  ↑(Module.finrank k
                      ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) j).obj V).obj
                          ↧M))) ∧
        ∀ (i : ℕ), n ≤ i → Q.coeff i = 0
Lean

Formalized in Tau Ceti as TauCeti.IsMorse.exists_sum_range_monomial_eq_add_mul.

Other forms

The Morse polynomial identity for a band. Formalized in Tau Ceti as TauCeti.IsMorse.exists_sum_range_monomial_sublevelPair_eq_add_mul.

TauCeti.IsMorse.exists_sum_range_monomial_sublevelPair_eq_add_mul.{u, u_1, u_2} {E : Type u_1}
  {H : Type u_2} {M : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E]
  [I.Boundaryless] [IsManifold I (↑⊤) M] [T2Space M] {f : M → ℝ} {k : Type u} [DivisionRing k]
  (V : ModuleCat k) [Module.Finite k ↑V] (hf : TauCeti.IsMorse I f) {a b : ℝ} (hab : a ≤ b)
  (hcompact : IsCompact (f ⁻¹' Set.Icc a b))
  (ha : TauCeti.IsRegularValue I (modelWithCornersSelf ℝ ℝ) f a)
  (hb : TauCeti.IsRegularValue I (modelWithCornersSelf ℝ ℝ) f b) {n : ℕ}
  (hn : Module.finrank ℝ E ≤ n) :
  ∃ Q,
    ∑ i ∈ Finset.range (n + 1),
          (Polynomial.monomial i)
            ({x |
                  x ∈ TauCeti.criticalPoints I f ∩ f ⁻¹' Set.Ioc a b ∧
                    TauCeti.manifoldMorseIndex I f x = i}.ncard *
              Module.finrank k ↑V) =
        ∑ i ∈ Finset.range (n + 1),
            (Polynomial.monomial i)
              (Module.finrank k ↑((TauCeti.sublevelPair f hab).singularHomology V i)) +
          (1 + Polynomial.X) * Q ∧
      (∀ i < n,
          ↑(Q.coeff i) =
            ↑(Module.finrank k ↑V) *
                ∑ j ∈ Finset.range (i + 1),
                  (-1) ^ (i - j) *
                    ↑{x |
                          x ∈ TauCeti.criticalPoints I f ∩ f ⁻¹' Set.Ioc a b ∧
                            TauCeti.manifoldMorseIndex I f x = j}.ncard -
              ∑ j ∈ Finset.range (i + 1),
                (-1) ^ (i - j) *
                  ↑(Module.finrank k ↑((TauCeti.sublevelPair f hab).singularHomology V j))) ∧
        ∀ (i : ℕ), n ≤ i → Q.coeff i = 0
Sources
LeanTauCeti.IsMorse.exists_sum_range_monomial_eq_add_mul · TauCeti.IsMorse.exists_sum_range_monomial_sublevelPair_eq_add_mul
Uses 8
Proof usesDeformation of sublevels across a band without critical points (Milnor, Theorem 3.1) · Euler--Poincaré for cellular chains · The Mayer–Vietoris isomorphism of a sphere · Milnor's cell attachment theorem · The Morse polynomial identity (ChainComplex.sum_range_monomial_finrank_X_eq) · The relative small-chain theorem · The strong Morse inequalities for a CW pair · The weak Morse inequality for a CW pair

TheoremReeb's theorem (Milnor, *Morse Theory*, Theorem 4.1)#

A compact boundaryless manifold modelled on a real vector space of dimension n which carries a Morse function with exactly two critical points is homeomorphic to the sphere Sⁿ.

TauCeti.IsMorse.nonempty_homeomorph_sphere_of_totalCriticalCount_eq_two.{u_1, u_2, u_3}
  {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] [IsManifold I (↑⊤) M] [T2Space M] [CompactSpace M]
  {f : M → ℝ} (hf : TauCeti.IsMorse I f) (h2 : TauCeti.totalCriticalCount I f = 2) :
  Nonempty (M ≃ₜ ↑(Metric.sphere 0 1))
Lean

Formalized in Tau Ceti as TauCeti.IsMorse.nonempty_homeomorph_sphere_of_totalCriticalCount_eq_two.

Sources
LeanTauCeti.IsMorse.nonempty_homeomorph_sphere_of_totalCriticalCount_eq_two
Uses 3
Proof usesFermat's theorem on a manifold · The normalized Morse lemma on a manifold · Sublevels on either side of a band without critical points are diffeomorphic (Milnor, Theorem 3.1)

TheoremThe strong Morse inequalities (TauCeti.IsMorse.sum_range_neg_one_pow_mul_finrank_singularHomology_le)#

For a Morse function f on a compact boundaryless manifold M, write bᵢ for the dimension of Hᵢ(M; V) and cᵢ for the number of critical points of index i. Then bₙ - bₙ₋₁ + ⋯ ± b₀ ≤ (cₙ - cₙ₋₁ + ⋯ ± c₀) dim V.

TauCeti.IsMorse.sum_range_neg_one_pow_mul_finrank_singularHomology_le.{u, u_1, u_2} {E : Type u_1}
  {H : Type u_2} {M : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E]
  [I.Boundaryless] [IsManifold I (↑⊤) M] [T2Space M] {f : M → ℝ} {k : Type u} [DivisionRing k]
  (V : ModuleCat k) [Module.Finite k ↑V] [CompactSpace M] (hf : TauCeti.IsMorse I f) (n : ℕ) :
  ∑ i ∈ Finset.range (n + 1),
      (-1) ^ (n - i) *
        ↑(Module.finrank k
            ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) i).obj V).obj ↧M)) ≤
    ↑(Module.finrank k ↑V) *
      ∑ i ∈ Finset.range (n + 1), (-1) ^ (n - i) * ↑(TauCeti.criticalCount I f i).toNat
Lean

Formalized in Tau Ceti as TauCeti.IsMorse.sum_range_neg_one_pow_mul_finrank_singularHomology_le.

Other forms

The strong Morse inequalities for a band. Formalized in Tau Ceti as TauCeti.IsMorse.sum_range_neg_one_pow_mul_finrank_singularHomology_sublevelPair_le.

TauCeti.IsMorse.sum_range_neg_one_pow_mul_finrank_singularHomology_sublevelPair_le.{u, u_1, u_2}
  {E : Type u_1} {H : Type u_2} {M : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M]
  [FiniteDimensional ℝ E] [I.Boundaryless] [IsManifold I (↑⊤) M] [T2Space M] {f : M → ℝ}
  {k : Type u} [DivisionRing k] (V : ModuleCat k) [Module.Finite k ↑V] (hf : TauCeti.IsMorse I f)
  {a b : ℝ} (hab : a ≤ b) (hcompact : IsCompact (f ⁻¹' Set.Icc a b))
  (ha : TauCeti.IsRegularValue I (modelWithCornersSelf ℝ ℝ) f a)
  (hb : TauCeti.IsRegularValue I (modelWithCornersSelf ℝ ℝ) f b) (n : ℕ) :
  ∑ i ∈ Finset.range (n + 1),
      (-1) ^ (n - i) * ↑(Module.finrank k ↑((TauCeti.sublevelPair f hab).singularHomology V i)) ≤
    ↑(Module.finrank k ↑V) *
      ∑ i ∈ Finset.range (n + 1),
        (-1) ^ (n - i) *
          ↑{x |
                x ∈ TauCeti.criticalPoints I f ∩ f ⁻¹' Set.Ioc a b ∧
                  TauCeti.manifoldMorseIndex I f x = i}.ncard
Sources
LeanTauCeti.IsMorse.sum_range_neg_one_pow_mul_finrank_singularHomology_le · TauCeti.IsMorse.sum_range_neg_one_pow_mul_finrank_singularHomology_sublevelPair_le
Uses 7
Proof usesDeformation of sublevels across a band without critical points (Milnor, Theorem 3.1) · Euler--Poincaré for cellular chains · The Mayer–Vietoris isomorphism of a sphere · Milnor's cell attachment theorem · The relative small-chain theorem · The strong Morse inequalities for a CW pair · The weak Morse inequality for a CW pair

TheoremThe weak Morse inequalities#

For a Morse function f on a compact boundaryless manifold M, the singular homology Hₙ(M; V) has dimension at most dim V times the number of critical points of index n.

TauCeti.IsMorse.finrank_singularHomology_le.{u, u_1, u_2} {E : Type u_1} {H : Type u_2} {M : Type u}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
  [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [I.Boundaryless]
  [IsManifold I (↑⊤) M] [T2Space M] {f : M → ℝ} {k : Type u} [DivisionRing k] (V : ModuleCat k)
  [Module.Finite k ↑V] [CompactSpace M] (hf : TauCeti.IsMorse I f) (n : ℕ) :
  Module.finrank k ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) n).obj V).obj ↧M) ≤
    (TauCeti.criticalCount I f n).toNat * Module.finrank k ↑V
Lean

Formalized in Tau Ceti as TauCeti.IsMorse.finrank_singularHomology_le.

Other forms

The weak Morse inequalities across a critical level. Formalized in Tau Ceti as TauCeti.IsMorse.exists_isZero_and_finrank_le_singularHomology_sublevelPair.

TauCeti.IsMorse.exists_isZero_and_finrank_le_singularHomology_sublevelPair.{u, v, w, u_1, u_2}
  {E : Type u_1} {H : Type u_2} {M : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M]
  [FiniteDimensional ℝ E] [I.Boundaryless] [IsManifold I (↑⊤) M] [T2Space M] {f : M → ℝ} {c δ : ℝ}
  (hf : TauCeti.IsMorse I f) (hδ : 0 < δ) (hcompact : IsCompact (f ⁻¹' Set.Icc (c - δ) (c + δ))) :
  ∃ ε,
    ∃ (hε : 0 < ε),
      ε ≤ δ ∧
        (∀ {A : Type v} [inst : CategoryTheory.Category.{w, v} A]
            [inst_1 : CategoryTheory.Abelian A] [inst_2 : CategoryTheory.Limits.HasCoproducts A]
            (R : A) (n : ℕ),
            (∀ p ∈ TauCeti.criticalPoints I f ∩ f ⁻¹' {c}, TauCeti.manifoldMorseIndex I f p ≠ n) →
              CategoryTheory.Limits.IsZero ((TauCeti.sublevelPair f ⋯).singularHomology R n)) ∧
          ∀ (k : Type u) [inst : DivisionRing k] (V : ModuleCat k) [Module.Finite k ↑V] (n : ℕ),
            Module.Finite k ↑((TauCeti.sublevelPair f ⋯).singularHomology V n) ∧
              Module.finrank k ↑((TauCeti.sublevelPair f ⋯).singularHomology V n) ≤
                Nat.card { p // TauCeti.manifoldMorseIndex I f ↑p = n } * Module.finrank k ↑V

The weak Morse inequalities for a band. Formalized in Tau Ceti as TauCeti.IsMorse.finrank_singularHomology_sublevelPair_le.

TauCeti.IsMorse.finrank_singularHomology_sublevelPair_le.{u, u_1, u_2} {E : Type u_1} {H : Type u_2}
  {M : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E]
  [I.Boundaryless] [IsManifold I (↑⊤) M] [T2Space M] {f : M → ℝ} {k : Type u} [DivisionRing k]
  (V : ModuleCat k) [Module.Finite k ↑V] (hf : TauCeti.IsMorse I f) {a b : ℝ} (hab : a ≤ b)
  (hcompact : IsCompact (f ⁻¹' Set.Icc a b))
  (ha : TauCeti.IsRegularValue I (modelWithCornersSelf ℝ ℝ) f a)
  (hb : TauCeti.IsRegularValue I (modelWithCornersSelf ℝ ℝ) f b) (n : ℕ) :
  Module.finrank k ↑((TauCeti.sublevelPair f hab).singularHomology V n) ≤
    {x |
          x ∈ TauCeti.criticalPoints I f ∩ f ⁻¹' Set.Ioc a b ∧
            TauCeti.manifoldMorseIndex I f x = n}.ncard *
      Module.finrank k ↑V
Sources
LeanTauCeti.IsMorse.finrank_singularHomology_le · TauCeti.IsMorse.exists_isZero_and_finrank_le_singularHomology_sublevelPair · TauCeti.IsMorse.finrank_singularHomology_sublevelPair_le
Uses 7 · Used by 1
Proof usesDeformation of sublevels across a band without critical points (Milnor, Theorem 3.1) · Euler--Poincaré for cellular chains · The Mayer–Vietoris isomorphism of a sphere · Milnor's cell attachment theorem · The relative small-chain theorem · The strong Morse inequalities for a CW pair · The weak Morse inequality for a CW pair
Used byAndreotti–Frankel theorem for proper holomorphic immersions

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.