Analytic Heegaard Floer homology

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 Sard--Smale theorem#

The critical values of a sufficiently smooth Fredholm map on a Lindelöf subset of a Banach space form a meagre set. The subset need not be open; smoothness is assumed at each of its points in the ambient space. Every subset of a separable Banach space is Lindelöf.

Sard's theorem itself is false in infinite dimensions, and "measure zero" has no meaning there; what survives is that the Fredholm condition confines the failure of regularity to a finite-dimensional direction, in which the finite-dimensional theorem applies fibrewise.

The regularity threshold is the pointwise one of TauCeti.exists_mem_nhds_isClosed_isNowhereDense_image_criticalPoints: at each point C^k with k ≥ (dim ker)² + 1. In particular n = ∞ needs no side condition.

TauCeti.isMeagre_image_criticalPoints_of_isFredholm.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F]
  [CompleteSpace E] [CompleteSpace F] {U : Set E} [LindelofSpace ↑U] {f : E → F} {n : WithTop ℕ∞}
  (hf : ∀ x ∈ U, ContDiffAt ℝ n f x) (hFred : ∀ x ∈ U, (fderiv ℝ f x).IsFredholm)
  (hn :
    ∀ x ∈ U,
      ↑(Module.finrank ℝ ↥(↑(fderiv ℝ f x)).ker * Module.finrank ℝ ↥(↑(fderiv ℝ f x)).ker + 1) ≤
        n) :
  IsMeagre (f '' (U ∩ {x | ¬Function.Surjective ⇑(fderiv ℝ f x)}))
Lean

Formalized in Tau Ceti as TauCeti.isMeagre_image_criticalPoints_of_isFredholm.

Other forms

Sard--Smale, in the form transversality arguments consume. Formalized in Tau Ceti as TauCeti.dense_compl_image_criticalPoints_of_isFredholm.

TauCeti.dense_compl_image_criticalPoints_of_isFredholm.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F]
  [CompleteSpace E] [CompleteSpace F] {U : Set E} [LindelofSpace ↑U] {f : E → F} {n : WithTop ℕ∞}
  (hf : ∀ x ∈ U, ContDiffAt ℝ n f x) (hFred : ∀ x ∈ U, (fderiv ℝ f x).IsFredholm)
  (hn :
    ∀ x ∈ U,
      ↑(Module.finrank ℝ ↥(↑(fderiv ℝ f x)).ker * Module.finrank ℝ ↥(↑(fderiv ℝ f x)).ker + 1) ≤
        n) :
  Dense (f '' (U ∩ {x | ¬Function.Surjective ⇑(fderiv ℝ f x)}))ᶜ

Sard--Smale, locally. Formalized in Tau Ceti as TauCeti.exists_mem_nhds_isClosed_isNowhereDense_image_criticalPoints.

TauCeti.exists_mem_nhds_isClosed_isNowhereDense_image_criticalPoints.{u_1, u_2} {E : Type u_1}
  {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F]
  [CompleteSpace E] [CompleteSpace F] {f : E → F} {a : E} {U : Set E} {n : WithTop ℕ∞}
  (hf : ContDiffAt ℝ n f a) (hFred : (fderiv ℝ f a).IsFredholm)
  (hn :
    ↑(Module.finrank ℝ ↥(↑(fderiv ℝ f a)).ker * Module.finrank ℝ ↥(↑(fderiv ℝ f a)).ker + 1) ≤ n)
  (hU : U ∈ nhds a) :
  ∃ N ∈ nhds a,
    N ⊆ U ∧
      IsClosed (f '' (N ∩ {x | ¬Function.Surjective ⇑(fderiv ℝ f x)})) ∧
        IsNowhereDense (f '' (N ∩ {x | ¬Function.Surjective ⇑(fderiv ℝ f x)}))
Sources
LeanTauCeti.isMeagre_image_criticalPoints_of_isFredholm · TauCeti.dense_compl_image_criticalPoints_of_isFredholm · TauCeti.exists_mem_nhds_isClosed_isNowhereDense_image_criticalPoints
Uses 1 · Used by 3
Proof usesThe Morse--Sard theorem
Used byGeneric absence of negative-index zeros · Generic regular zeros · Sard's theorem for smooth maps

TheoremThe Morse--Sard theorem#

The critical values of a sufficiently smooth map between finite-dimensional real normed spaces, that is the values it takes at the points where its Fréchet derivative is not surjective, form a set of additive Haar measure zero. No relation between the two dimensions is required.

ContDiff.addHaar_image_criticalPoints_eq_zero.{u, v} {E : Type u} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℝ F]
  [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] {f : E → F}
  (ν : MeasureTheory.Measure F) [ν.IsAddHaarMeasure] {n : WithTop ℕ∞} (hf : ContDiff ℝ n f)
  (hk : ↑(Module.finrank ℝ E * Module.finrank ℝ E + 1) ≤ n) :
  ν (f '' {x | ¬Function.Surjective ⇑(fderiv ℝ f x)}) = 0
Lean

Formalized in Tau Ceti as ContDiff.addHaar_image_criticalPoints_eq_zero.

Other forms

The Morse--Sard theorem on a set. Formalized in Tau Ceti as TauCeti.addHaar_image_criticalPoints_eq_zero.

TauCeti.addHaar_image_criticalPoints_eq_zero.{u, v} {E : Type u} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℝ F]
  [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] {U : Set E} {f : E → F}
  (ν : MeasureTheory.Measure F) [ν.IsAddHaarMeasure] {n : WithTop ℕ∞}
  (hf : ∀ x ∈ U, ContDiffAt ℝ n f x) (hk : ↑(Module.finrank ℝ E * Module.finrank ℝ E + 1) ≤ n) :
  ν (f '' (U ∩ {x | ¬Function.Surjective ⇑(fderiv ℝ f x)})) = 0

The Morse--Sard theorem, in the form that carries no measure-theoretic data. Formalized in Tau Ceti as TauCeti.interior_image_criticalPoints_eq_empty.

TauCeti.interior_image_criticalPoints_eq_empty.{u, v} {E : Type u} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℝ F]
  [FiniteDimensional ℝ F] {U : Set E} {f : E → F} {n : WithTop ℕ∞}
  (hf : ∀ x ∈ U, ContDiffAt ℝ n f x) (hk : ↑(Module.finrank ℝ E * Module.finrank ℝ E + 1) ≤ n) :
  interior (f '' (U ∩ {x | ¬Function.Surjective ⇑(fderiv ℝ f x)})) = ∅

The Morse--Sard theorem at the sharp regularity, in codimension at most two. Formalized in Tau Ceti as TauCeti.addHaar_image_criticalPoints_eq_zero_of_finrank_le_add_two.

TauCeti.addHaar_image_criticalPoints_eq_zero_of_finrank_le_add_two.{u, v} {E : Type u}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type v}
  [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F]
  [BorelSpace F] {U : Set E} {f : E → F} (ν : MeasureTheory.Measure F) [ν.IsAddHaarMeasure]
  {n : WithTop ℕ∞} (hf : ∀ x ∈ U, ContDiffAt ℝ n f x)
  (hcodim : Module.finrank ℝ E ≤ Module.finrank ℝ F + 2)
  (hk : ↑(Module.finrank ℝ E - Module.finrank ℝ F + 1) ≤ n) :
  ν (f '' (U ∩ {x | ¬Function.Surjective ⇑(fderiv ℝ f x)})) = 0

The Morse--Sard theorem at the sharp regularity, in codimension at most two, in the form that carries no measure-theoretic data. Formalized in Tau Ceti as TauCeti.interior_image_criticalPoints_eq_empty_of_finrank_le_add_two.

TauCeti.interior_image_criticalPoints_eq_empty_of_finrank_le_add_two.{u, v} {E : Type u}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type v}
  [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {U : Set E} {f : E → F}
  {n : WithTop ℕ∞} (hf : ∀ x ∈ U, ContDiffAt ℝ n f x)
  (hcodim : Module.finrank ℝ E ≤ Module.finrank ℝ F + 2)
  (hk : ↑(Module.finrank ℝ E - Module.finrank ℝ F + 1) ≤ n) :
  interior (f '' (U ∩ {x | ¬Function.Surjective ⇑(fderiv ℝ f x)})) = ∅
Sources
LeanContDiff.addHaar_image_criticalPoints_eq_zero · TauCeti.addHaar_image_criticalPoints_eq_zero · TauCeti.interior_image_criticalPoints_eq_empty · TauCeti.addHaar_image_criticalPoints_eq_zero_of_finrank_le_add_two · TauCeti.interior_image_criticalPoints_eq_empty_of_finrank_le_add_two
Uses 1 · Used by 3
Proof usesSard's theorem on the locus where the derivative vanishes
Used byThe Sard--Smale theorem · The sharp BV Sobolev bound · Sard's theorem for smooth maps

TheoremThe index of the trajectory operator is a difference of Morse indices#

Let A be a continuous family of operators on a finite-dimensional real inner product space with invertible symmetric limits A± at ±∞. Then the index of the trajectory operator u ↦ u' + A u from W^{1,2}(ℝ, E) to L²(ℝ, E) is the number of negative eigenvalues of A⁻ minus the number of negative eigenvalues of A⁺, counted with multiplicity: the dimensions of the sums of their eigenspaces at negative eigenvalues.

TauCeti.WeakDerivStep.index_trajectoryOperator_eq_finrank_pointSpectralSubspace_sub_finrank.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  {A : ℝ → E →L[ℝ] E} (hA : Continuous A) {Aminus Aplus : E →L[ℝ] E}
  (hsymminus : (↑Aminus).IsSymmetric) (hsymplus : (↑Aplus).IsSymmetric) {α : ℝ} (hα : 0 < α)
  (hminus : ∀ (v : E), α * ‖v‖ ≤ ‖Aminus v‖) (hplus : ∀ (v : E), α * ‖v‖ ≤ ‖Aplus v‖)
  (hbot : Filter.Tendsto A Filter.atBot (nhds Aminus))
  (htop : Filter.Tendsto A Filter.atTop (nhds Aplus))
  (AL : ↥(MeasureTheory.Lp (E →L[ℝ] E) ⊤ (MeasureTheory.volume.restrict ↑⊤)))
  (hAL : ↑↑AL =ᵐ[MeasureTheory.volume.restrict ↑⊤] A) :
  (TauCeti.WeakDerivStep.trajectoryOperator AL).index =
    ↑(Module.finrank ℝ ↥(Module.End.pointSpectralSubspace (↑Aminus) (Set.Iio 0))) -
      ↑(Module.finrank ℝ ↥(Module.End.pointSpectralSubspace (↑Aplus) (Set.Iio 0)))
Lean

Formalized in Tau Ceti as TauCeti.WeakDerivStep.index_trajectoryOperator_eq_finrank_pointSpectralSubspace_sub_finrank.

Sources
LeanTauCeti.WeakDerivStep.index_trajectoryOperator_eq_finrank_pointSpectralSubspace_sub_finrank
Uses 2
Proof usesThe fundamental theorem of calculus for weak derivatives on the line · Rellich–Kondrachov on bounded Lipschitz domains

TheoremTauCeti.IsNondegenerateCriticalPoint.exists_stableSet_isManifold#

The global stable set of a Morse critical point of a globally C^(n+1) function has a C^n manifold structure modelled on the stable Hessian subspace, with its subspace topology and a C^n inclusion into the ambient space. The dimension of the model plus the Morse index equals the ambient dimension.

TauCeti.IsNondegenerateCriticalPoint.exists_stableSet_isManifold.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E}
  {K : NNReal} (h : TauCeti.IsNondegenerateCriticalPoint f x) {n : ℕ} (hn : 1 ≤ n)
  (hfs : ContDiff ℝ (↑n + 1) f) (hf : LipschitzWith K (gradient f)) :
  ∃ C,
    IsManifold (modelWithCornersSelf ℝ ↥⋯.stableLinearSubspace) ↑n
        ↑((TauCeti.negativeGradientFlow f hf).stableSet x) ∧
      ContMDiff (modelWithCornersSelf ℝ ↥⋯.stableLinearSubspace) (modelWithCornersSelf ℝ E) (↑n)
        Subtype.val
Lean

Formalized in Tau Ceti as TauCeti.IsNondegenerateCriticalPoint.exists_stableSet_isManifold.

Sources
LeanTauCeti.IsNondegenerateCriticalPoint.exists_stableSet_isManifold

TheoremDarboux's theorem#

A closed C^r two-form ω (r ≥ 1) on an open subset of a finite-dimensional real normed space, nondegenerate at x₀, is constant in suitable coordinates near x₀: there is a C^r diffeomorphism ψ of the space fixing x₀ such that the pullback ψ^* ω equals the constant form ω(x₀) on a neighbourhood of x₀.

TauCeti.exists_diffeomorph_eventually_compContinuousLinearMap_fderiv_eq.{u_1} {V : Type u_1}
  [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {ω : V → V [⋀^Fin 2]→L[ℝ] ℝ}
  {W : Set V} {x₀ : V} {r : ℕ∞} (hr : 1 ≤ r) (hW : IsOpen W) (hx₀ : x₀ ∈ W)
  (hω : ContDiffOn ℝ (↑r) ω W) (hdω : ∀ x ∈ W, extDeriv ω x = 0)
  (hnd : ∀ (v : V), (∀ (w : V), (ω x₀) ![v, w] = 0) → v = 0) :
  ∃ ψ, ψ x₀ = x₀ ∧ ∀ᶠ (x : V) in nhds x₀, (ω (ψ x)).compContinuousLinearMap (fderiv ℝ (⇑ψ) x) = ω x₀
Lean

Formalized in Tau Ceti as TauCeti.exists_diffeomorph_eventually_compContinuousLinearMap_fderiv_eq.

Other forms

Darboux's theorem. Formalized in Tau Ceti as TauCeti.SmoothTwoForm.IsSymplectic.exists_darbouxChart.

TauCeti.SmoothTwoForm.IsSymplectic.exists_darbouxChart.{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} [TopologicalSpace M] [ChartedSpace H M]
  [IsManifold I (↑⊤) M] [BoundarylessManifold I M] {form : TauCeti.SmoothTwoForm I M}
  (hform : form.IsSymplectic) (x₀ : M) :
  ∃ chart form₀,
    x₀ ∈ chart.source ∧
      ↑chart.toPartialEquiv x₀ = 0 ∧
        ∀ x ∈ chart.source,
          ∀ (v w : TangentSpace I x),
            TauCeti.SmoothBundleForm.eval₂ form x v w =
              (fun v w => (form₀.toBilinForm v) w) ((d% ↑chart.toPartialEquiv x) v)
                ((d% ↑chart.toPartialEquiv x) w)

Darboux's theorem at an interior point. Formalized in Tau Ceti as TauCeti.SmoothTwoForm.IsSymplectic.exists_darbouxChart_of_isInteriorPoint.

TauCeti.SmoothTwoForm.IsSymplectic.exists_darbouxChart_of_isInteriorPoint.{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} [TopologicalSpace M]
  [ChartedSpace H M] [IsManifold I (↑⊤) M] {form : TauCeti.SmoothTwoForm I M}
  (hform : form.IsSymplectic) {x₀ : M} (hx₀ : I.IsInteriorPoint x₀) :
  ∃ chart form₀,
    x₀ ∈ chart.source ∧
      ↑chart.toPartialEquiv x₀ = 0 ∧
        ∀ x ∈ chart.source,
          ∀ (v w : TangentSpace I x),
            TauCeti.SmoothBundleForm.eval₂ form x v w =
              (fun v w => (form₀.toBilinForm v) w) ((d% ↑chart.toPartialEquiv x) v)
                ((d% ↑chart.toPartialEquiv x) w)

Darboux's theorem for a prescribed model symplectic form. Formalized in Tau Ceti as TauCeti.SmoothTwoForm.IsSymplectic.exists_darbouxChart_of_symplecticForm.

TauCeti.SmoothTwoForm.IsSymplectic.exists_darbouxChart_of_symplecticForm.{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} [TopologicalSpace M]
  [ChartedSpace H M] [IsManifold I (↑⊤) M] [BoundarylessManifold I M]
  {form : TauCeti.SmoothTwoForm I M} (hform : form.IsSymplectic) (form₀ : TauCeti.SymplecticForm E)
  (x₀ : M) :
  ∃ chart,
    x₀ ∈ chart.source ∧
      ↑chart.toPartialEquiv x₀ = 0 ∧
        ∀ x ∈ chart.source,
          ∀ (v w : TangentSpace I x),
            TauCeti.SmoothBundleForm.eval₂ form x v w =
              (fun v w => (form₀.toBilinForm v) w) ((d% ↑chart.toPartialEquiv x) v)
                ((d% ↑chart.toPartialEquiv x) w)

Darboux's theorem for a prescribed model symplectic form at an interior point. Formalized in Tau Ceti as TauCeti.SmoothTwoForm.IsSymplectic.exists_darbouxChart_of_symplecticForm_of_isInteriorPoint.

TauCeti.SmoothTwoForm.IsSymplectic.exists_darbouxChart_of_symplecticForm_of_isInteriorPoint.{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} [TopologicalSpace M]
  [ChartedSpace H M] [IsManifold I (↑⊤) M] {form : TauCeti.SmoothTwoForm I M}
  (hform : form.IsSymplectic) (form₀ : TauCeti.SymplecticForm E) {x₀ : M}
  (hx₀ : I.IsInteriorPoint x₀) :
  ∃ chart,
    x₀ ∈ chart.source ∧
      ↑chart.toPartialEquiv x₀ = 0 ∧
        ∀ x ∈ chart.source,
          ∀ (v w : TangentSpace I x),
            TauCeti.SmoothBundleForm.eval₂ form x v w =
              (fun v w => (form₀.toBilinForm v) w) ((d% ↑chart.toPartialEquiv x) v)
                ((d% ↑chart.toPartialEquiv x) w)
Sources
LeanTauCeti.exists_diffeomorph_eventually_compContinuousLinearMap_fderiv_eq · TauCeti.SmoothTwoForm.IsSymplectic.exists_darbouxChart · TauCeti.SmoothTwoForm.IsSymplectic.exists_darbouxChart_of_isInteriorPoint · TauCeti.SmoothTwoForm.IsSymplectic.exists_darbouxChart_of_symplecticForm · TauCeti.SmoothTwoForm.IsSymplectic.exists_darbouxChart_of_symplecticForm_of_isInteriorPoint
Uses 3
Proof usesLinear Darboux theorem · Moser's lemma, local form · The Poincaré lemma

TheoremThe symmetric power of a complex curve is a complex analytic manifold#

For a Hausdorff one-dimensional complex manifold α, the elementary-symmetric charts of Sym α n have analytic transition maps, so TauCeti.symChartedSpace makes Sym α n an analytic manifold modelled on Fin n → ℂ.

TauCeti.isManifold_symChartedSpace.{u_1} {α : Type u_1} [TopologicalSpace α] [T2Space α]
  [ChartedSpace ℂ α] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 α] {n : ℕ} :
  IsManifold (modelWithCornersSelf ℂ (Fin n → ℂ)) ⊤ (Sym α n)
Lean

Formalized in Tau Ceti as TauCeti.isManifold_symChartedSpace.

Sources
LeanTauCeti.isManifold_symChartedSpace
Uses 3
Proof usesCauchy's bound on the symmetric power · Newton's identities for a multiset · Vieta's formulas on the symmetric power

TheoremGeneric regular zeros#

For a residual set of parameters l, the zeros of s (·, l) form a C^n manifold of dimension the index d, with a C^n immersion into M whose tangent spaces are the kernels of the linearizations in the M direction.

TauCeti.eventually_residual_exists_isManifold_sectionZero.{u_1, u_2, u_3, u_4, u_5, u_6, u_7, u_8}
  {X : Type u_1} {Λ : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {EB : Type u_6}
  {HB : Type u_7} {E : B → Type u_8} [NormedAddCommGroup X] [NormedSpace ℝ X] [TopologicalSpace M]
  [ChartedSpace X M] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup EB]
  [NormedSpace ℝ EB] [TopologicalSpace HB] {I : ModelWithCorners ℝ EB HB} [TopologicalSpace B]
  [ChartedSpace HB B] [(a : B) → TopologicalSpace (E a)] [TopologicalSpace (Bundle.TotalSpace F E)]
  [(a : B) → AddCommGroup (E a)] [(a : B) → _root_.Module ℝ (E a)] [FiberBundle F E]
  [VectorBundle ℝ F E] {b : M × Λ → B} {s : (z : M × Λ) → E (b z)} [NormedAddCommGroup Λ]
  [NormedSpace ℝ Λ] [CompleteSpace X] [CompleteSpace Λ] [CompleteSpace F]
  [SecondCountableTopology ↑{z | s z = 0}] {n : WithTop ℕ∞}
  (hcont :
    ∀ (z : M × Λ),
      s z = 0 →
        ContMDiffAt ((modelWithCornersSelf ℝ X).prod (modelWithCornersSelf ℝ Λ))
          (I.prod (modelWithCornersSelf ℝ F)) n (fun w => ⟨b w, s w⟩) z)
  (hFred :
    ∀ (z : M × Λ),
      s z = 0 →
        (TauCeti.sectionLinearization (modelWithCornersSelf ℝ X) (fun y => b (y, z.2))
            (fun y => s (y, z.2)) z.1).IsFredholm)
  (htotal :
    ∀ (z : M × Λ),
      s z = 0 →
        Function.Surjective
          ⇑(TauCeti.sectionLinearization
              ((modelWithCornersSelf ℝ X).prod (modelWithCornersSelf ℝ Λ)) b s z))
  (hn :
    ∀ (z : M × Λ),
      s z = 0 →
        ↑(Module.finrank ℝ
                  ↥(↑(TauCeti.sectionLinearization (modelWithCornersSelf ℝ X) (fun y => b (y, z.2))
                          (fun y => s (y, z.2)) z.1)).ker ^
                2 +
              1) ≤
          n)
  {d : ℕ} [IsManifold (modelWithCornersSelf ℝ X) n M] [ContMDiffVectorBundle n F E I] (hn0 : n ≠ 0)
  (hindex :
    ∀ (z : M × Λ),
      s z = 0 →
        (↑(TauCeti.sectionLinearization (modelWithCornersSelf ℝ X) (fun y => b (y, z.2))
                (fun y => s (y, z.2)) z.1)).index =
          ↑d) :
  ∀ᶠ (l : Λ) in residual Λ,
    ∃ cs,
      IsManifold (modelWithCornersSelf ℝ (Fin d → ℝ)) n ↑{x | s (x, l) = 0} ∧
        Manifold.IsImmersionOfComplement F (modelWithCornersSelf ℝ (Fin d → ℝ))
            (modelWithCornersSelf ℝ X) n Subtype.val ∧
          ∀ (z : ↑{x | s (x, l) = 0}),
            (↑(mfderiv% Subtype.val z)).range =
              (↑(TauCeti.sectionLinearization (modelWithCornersSelf ℝ X) (fun y => b (y, l))
                    (fun y => s (y, l)) ↑z)).ker
Lean

Formalized in Tau Ceti as TauCeti.eventually_residual_exists_isManifold_sectionZero.

Sources
LeanTauCeti.eventually_residual_exists_isManifold_sectionZero
Uses 1
Proof usesThe Sard--Smale theorem

TheoremGeneric absence of negative-index zeros#

If the slice linearization is Fredholm of negative index at each zero and the total section is transverse to zero, zero-free parameters form a residual set. Second countability is needed only for the universal zero set.

TauCeti.mem_residual_setOf_forall_section_ne_zero_of_index_neg.{u_1, u_2, u_3, u_4, u_5, u_6, u_7,
    u_8}
  {X : Type u_1} {Λ : Type u_2} {M : Type u_3} {B : Type u_4} {F : Type u_5} {EB : Type u_6}
  {HB : Type u_7} {E : B → Type u_8} [NormedAddCommGroup X] [NormedSpace ℝ X] [TopologicalSpace M]
  [ChartedSpace X M] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup EB]
  [NormedSpace ℝ EB] [TopologicalSpace HB] {I : ModelWithCorners ℝ EB HB} [TopologicalSpace B]
  [ChartedSpace HB B] [(a : B) → TopologicalSpace (E a)] [TopologicalSpace (Bundle.TotalSpace F E)]
  [(a : B) → AddCommGroup (E a)] [(a : B) → _root_.Module ℝ (E a)] [FiberBundle F E]
  [VectorBundle ℝ F E] {b : M × Λ → B} {s : (z : M × Λ) → E (b z)} [NormedAddCommGroup Λ]
  [NormedSpace ℝ Λ] [CompleteSpace X] [CompleteSpace Λ] [CompleteSpace F]
  [IsManifold (modelWithCornersSelf ℝ X) 1 M] [SecondCountableTopology ↑{z | s z = 0}]
  {n : WithTop ℕ∞}
  (hcont :
    ∀ (z : M × Λ),
      s z = 0 →
        ContMDiffAt ((modelWithCornersSelf ℝ X).prod (modelWithCornersSelf ℝ Λ))
          (I.prod (modelWithCornersSelf ℝ F)) n (fun w => ⟨b w, s w⟩) z)
  (hFred :
    ∀ (z : M × Λ),
      s z = 0 →
        (TauCeti.sectionLinearization (modelWithCornersSelf ℝ X) (fun y => b (y, z.2))
            (fun y => s (y, z.2)) z.1).IsFredholm)
  (htotal :
    ∀ (z : M × Λ),
      s z = 0 →
        Function.Surjective
          ⇑(TauCeti.sectionLinearization
              ((modelWithCornersSelf ℝ X).prod (modelWithCornersSelf ℝ Λ)) b s z))
  (hn :
    ∀ (z : M × Λ),
      s z = 0 →
        ↑(Module.finrank ℝ
                  ↥(↑(TauCeti.sectionLinearization (modelWithCornersSelf ℝ X) (fun y => b (y, z.2))
                          (fun y => s (y, z.2)) z.1)).ker ^
                2 +
              1) ≤
          n)
  (hindex :
    ∀ (z : M × Λ),
      s z = 0 →
        (↑(TauCeti.sectionLinearization (modelWithCornersSelf ℝ X) (fun y => b (y, z.2))
                (fun y => s (y, z.2)) z.1)).index <
          0) :
  {l | ∀ (x : M), s (x, l) ≠ 0} ∈ residual Λ
Lean

Formalized in Tau Ceti as TauCeti.mem_residual_setOf_forall_section_ne_zero_of_index_neg.

Sources
LeanTauCeti.mem_residual_setOf_forall_section_ne_zero_of_index_neg
Uses 1
Proof usesThe Sard--Smale theorem

TheoremTauCeti.morseBoundary_comp_morseBoundary_eq_zero_iff#

The mod-two Morse boundary squares to zero exactly when, between any two critical points, the number of broken index-two trajectories is even.

TauCeti.morseBoundary_comp_morseBoundary_eq_zero_iff.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {K : NNReal} (hfs : ContDiff ℝ 2 f)
  (hf : LipschitzWith K (gradient f)) (hM : TauCeti.HasNondegenerateCriticalPointsOn f Set.univ)
  (hcompact : ∀ (c : ℝ), IsCompact {z | f z ≤ c}) (htr : TauCeti.IsMorseSmale f hf) :
  TauCeti.morseBoundary hfs hf hM hcompact htr ∘ₗ TauCeti.morseBoundary hfs hf hM hcompact htr = 0 ↔
    ∀ (p r : TauCeti.MorseCriticalPoint f), Even (TauCeti.morseBrokenTrajectorySet hf ↑p ↑r).ncard
Lean

Formalized in Tau Ceti as TauCeti.morseBoundary_comp_morseBoundary_eq_zero_iff.

Sources
LeanTauCeti.morseBoundary_comp_morseBoundary_eq_zero_iff
Uses 1
Proof usesThe Morse form of the convergence theorem

TheoremMoser's lemma, local form#

Let ω₀, ω₁ be closed C^r two-forms (r ≥ 1) on an open subset W of a finite-dimensional real normed space, with ω₁ - ω₀ = dα on W for a C^r one-form α vanishing at x₀ ∈ W. If ω₀ and ω₁ agree at x₀ and are nondegenerate there, then some C^r diffeomorphism ψ of the space pulls ω₁ back to ω₀ on a neighbourhood of x₀. Moreover ψ fixes, near x₀, every point at which α vanishes; in particular ψ x₀ = x₀.

TauCeti.exists_diffeomorph_eventually_compContinuousLinearMap_fderiv_eq_of_extDeriv_eq.{u_1}
  {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V]
  {ω₀ ω₁ : V → V [⋀^Fin 2]→L[ℝ] ℝ} {α : V → V [⋀^Fin 1]→L[ℝ] ℝ} {W : Set V} {x₀ : V} {r : ℕ∞}
  (hr : 1 ≤ r) (hW : IsOpen W) (hx₀ : x₀ ∈ W) (hω₀ : ContDiffOn ℝ (↑r) ω₀ W)
  (hω₁ : ContDiffOn ℝ (↑r) ω₁ W) (hα : ContDiffOn ℝ (↑r) α W) (hdω₀ : ∀ x ∈ W, extDeriv ω₀ x = 0)
  (hdω₁ : ∀ x ∈ W, extDeriv ω₁ x = 0) (hdα : ∀ x ∈ W, extDeriv α x = ω₁ x - ω₀ x) (hα₀ : α x₀ = 0)
  (heq : ω₁ x₀ = ω₀ x₀) (hnd : ∀ (v : V), (∀ (w : V), (ω₀ x₀) ![v, w] = 0) → v = 0) :
  ∃ ψ,
    (∀ᶠ (x : V) in nhds x₀, α x = 0 → ψ x = x) ∧
      ∀ᶠ (x : V) in nhds x₀, (ω₁ (ψ x)).compContinuousLinearMap (fderiv ℝ (⇑ψ) x) = ω₀ x
Lean

Formalized in Tau Ceti as TauCeti.exists_diffeomorph_eventually_compContinuousLinearMap_fderiv_eq_of_extDeriv_eq.

Sources
LeanTauCeti.exists_diffeomorph_eventually_compContinuousLinearMap_fderiv_eq_of_extDeriv_eq
Uses 1 · Used by 2
Proof usesMoser's identity
Used byDarboux's theorem · The relative Darboux theorem in adapted coordinates

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.