Hadamard's identity in the… to Riemann's removable singularity…

TheoremHadamard's identity in the algebra of smooth functions#

A pointwise factorization of g - g x through the functions c i, with coefficients a i, is an identity between the bundled smooth maps themselves, the constants appearing as the images of algebraMap.

This is the pointwise-to-bundled transport: the hypothesis speaks of values, the conclusion of elements of C^n⟮I, M; 𝕜⟯, and the two are related by evaluation being a ring homomorphism.

TauCeti.sub_algebraMap_eq_sum_mul_sub_algebraMap.{u_1, u_2, u_3, u_4, u_5} {𝕜 : Type u_1}
  [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3}
  [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M]
  [ChartedSpace H M] {n : WithTop ℕ∞} {ι : Type u_5} [Fintype ι] (x : M)
  (g : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n)
  (a c : ι → ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n)
  (h : ∀ (y : M), g y - g x = ∑ i, (a i) y * ((c i) y - (c i) x)) :
  g - (algebraMap 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n)) (g x) =
    ∑ i, a i * (c i - (algebraMap 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n)) ((c i) x))

Lean

Formalized in Tau Ceti as TauCeti.sub_algebraMap_eq_sum_mul_sub_algebraMap.

Sources

• Tau Ceti documentation: TauCeti.sub_algebraMap_eq_sum_mul_sub_algebraMap
• Source of TauCeti.sub_algebraMap_eq_sum_mul_sub_algebraMap in TauCeti/Geometry/Manifold/Algebra/SmoothFunctions.lean

LeanTauCeti.sub_algebraMap_eq_sum_mul_sub_algebraMap

Used by 3

Used byHunt's lemma · Kronecker's criterion · The closed-subgroup theorem, with its model space

TheoremHadamard's lemma in coordinates#

Subtracting its value at x writes a smooth real function as a combination of the coordinate functions of any finitely-indexed basis, each taken relative to its own value at x, with smooth coefficients. At the base point those coefficients are the directional derivatives along the basis.

ContMDiffMap.exists_hadamard_coords.{u_1, u_2} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] {ι : Type u_2} [Fintype ι]
  (f : ContMDiffMap (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ ℝ) E ℝ ↑⊤) (x : E)
  (b : Module.Basis ι ℝ E) :
  ∃ a,
    (∀ (i : ι), (a i) x = (fderiv ℝ (⇑f) x) (b i)) ∧
      ∀ (y : E), f y - f x = ∑ i, (a i) y * ((b.coord i) y - (b.coord i) x)

Lean

Formalized in Tau Ceti as ContMDiffMap.exists_hadamard_coords.

Other forms

Hadamard's lemma for holomorphic germs. Formalized in Tau Ceti as OpenPartialHomeomorph.exists_eq_sum_holomorphicLinearCoordinateGerm_mul.

OpenPartialHomeomorph.exists_eq_sum_holomorphicLinearCoordinateGerm_mul.{u_1, u_2} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type} [TopologicalSpace X] [ChartedSpace E X]
  (e : OpenPartialHomeomorph X E) (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ E) ⊤ X)
  {x : X} [FiniteDimensional ℂ E] {ι : Type u_2} (b : Module.Basis ι ℂ E) [Fintype ι]
  (hx : x ∈ e.source)
  {s : ↑((TauCeti.holomorphicStructureSheaf (modelWithCornersSelf ℂ E) X).presheaf.stalk x)}
  (hs : (TauCeti.holomorphicStructureSheaf.eval (modelWithCornersSelf ℂ E) X x) s = 0) {φ : X → ℂ}
  (hφ :
    (TauCeti.holomorphicStructureSheaf.toFilterGerm (modelWithCornersSelf ℂ E) X x (nhds x) ⋯) s =
      ↑φ) :
  ∃ q,
    s =
        ∑ i,
          e.holomorphicLinearCoordinateGerm he x (LinearMap.toContinuousLinearMap (b.coord i)) hx *
            q i ∧
      ∀ (i : ι),
        (TauCeti.holomorphicStructureSheaf.eval (modelWithCornersSelf ℂ E) X x) (q i) =
          (fderiv ℂ (φ ∘ ↑e.symm) (↑e x)) (b i)

Hadamard's lemma for the vanishing ideal. Formalized in Tau Ceti as TauCeti.mem_smoothVanishingIdeal_sq_of_mvfderiv_eq_zero.

TauCeti.mem_smoothVanishingIdeal_sq_of_mvfderiv_eq_zero.{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]
  [FiniteDimensional ℝ E] [IsManifold I (↑⊤) M] [T2Space M] {x : M} (hx : I.IsInteriorPoint x)
  {f : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤} (hf₀ : f x = 0) (hf₁ : d% ⇑f x = 0) :
  f ∈ TauCeti.smoothVanishingIdeal I x ^ 2

Sources

• Tau Ceti documentation: ContMDiffMap.exists_hadamard_coords
• Source of ContMDiffMap.exists_hadamard_coords in TauCeti/Geometry/Manifold/ContMDiffMap/Hadamard.lean

LeanContMDiffMap.exists_hadamard_coords · OpenPartialHomeomorph.exists_eq_sum_holomorphicLinearCoordinateGerm_mul · TauCeti.mem_smoothVanishingIdeal_sq_of_mvfderiv_eq_zero

Uses 1 · Used by 3

Proof usesHadamard's lemma along a graph

Used byHunt's lemma · Kronecker's criterion · The closed-subgroup theorem, with its model space

TheoremThe identity theorem on analytic manifolds#

On a preconnected C^ω manifold modelled without boundary on a locally connected space, two C^ω functions with values in a normed space that agree on a neighbourhood of a point are equal.

ContMDiff.eq_of_eventuallyEq.{u_1, u_2, u_3, u_4, u_8} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H]
  {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M]
  [ChartedSpace H M] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
  [LocallyConnectedSpace E] [IsManifold I ⊤ M] [PreconnectedSpace M] {f g : M → F}
  (hf : ContMDiff I (modelWithCornersSelf 𝕜 F) ⊤ f)
  (hg : ContMDiff I (modelWithCornersSelf 𝕜 F) ⊤ g) {x₀ : M} (hfg : f =ᶠ[nhds x₀] g) : f = g

Lean

Formalized in Tau Ceti as ContMDiff.eq_of_eventuallyEq.

Other forms

The identity theorem on analytic manifolds. Formalized in Tau Ceti as TauCeti.eqOn_of_preconnected_of_eventuallyEq_of_contMDiffAt.

TauCeti.eqOn_of_preconnected_of_eventuallyEq_of_contMDiffAt.{u_1, u_2, u_3, u_4, u_8} {𝕜 : Type u_1}
  [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3}
  [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] {M : Type u_4}
  [TopologicalSpace M] [ChartedSpace H M] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
  [LocallyConnectedSpace E] [IsManifold I ⊤ M] {f g : M → F} {U : Set M}
  (hf : ∀ x ∈ U, ContMDiffAt I (modelWithCornersSelf 𝕜 F) ⊤ f x)
  (hg : ∀ x ∈ U, ContMDiffAt I (modelWithCornersSelf 𝕜 F) ⊤ g x) (hU : IsPreconnected U) {x₀ : M}
  (h₀ : x₀ ∈ U) (hfg : f =ᶠ[nhds x₀] g) : Set.EqOn f g U

Sources

• Tau Ceti documentation: ContMDiff.eq_of_eventuallyEq
• Source of ContMDiff.eq_of_eventuallyEq in TauCeti/Geometry/Manifold/ContMDiff/Analytic.lean

LeanContMDiff.eq_of_eventuallyEq · TauCeti.eqOn_of_preconnected_of_eventuallyEq_of_contMDiffAt

TheoremThe integrated Bochner identity#

For a compactly supported smooth function on a boundaryless manifold, ∫ (|Hess f|² + Ric(grad f, grad f)) = ∫ (Δ f)². Both integrands are integrable, and the identity holds in every pointwise orthonormal basis.

TauCeti.Manifold.integral_sum_hessian_sq_add_ricci.{u_1, u_2, u_3, u_4} {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 (↑⊤) M] [I.Boundaryless] [MeasurableSpace M]
  [BorelSpace M] [Bundle.RiemannianBundle fun x => TangentSpace I x]
  [IsContMDiffRiemannianBundle I (↑⊤) E fun x => TangentSpace I x]
  [IsContinuousRiemannianBundle E fun x => TangentSpace I x] {f : M → ℝ} {ι : Type u_4} [Fintype ι]
  [SigmaCompactSpace M] (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f)
  (hfc : HasCompactSupport f) (b : (x : M) → OrthonormalBasis ι ℝ (TangentSpace I x)) :
  ∫ (x : M),
      ∑ i, ∑ j, TauCeti.Manifold.hessian I f x ((b x) i) ((b x) j) ^ 2 +
        (((CovariantDerivative.leviCivitaConnection I M).ricciTensor x)
            (TauCeti.Manifold.mgradient I f x))
          (TauCeti.Manifold.mgradient I f x) ∂TauCeti.riemannianVolume I M =
    ∫ (x : M), TauCeti.Manifold.laplaceBeltrami I f x ^ 2 ∂TauCeti.riemannianVolume I M

Lean

Formalized in Tau Ceti as TauCeti.Manifold.integral_sum_hessian_sq_add_ricci.

Sources

• Tau Ceti documentation: TauCeti.Manifold.integral_sum_hessian_sq_add_ricci
• Source of TauCeti.Manifold.integral_sum_hessian_sq_add_ricci in TauCeti/Geometry/Manifold/Riemannian/Bochner/Integral.lean

LeanTauCeti.Manifold.integral_sum_hessian_sq_add_ricci

Uses 4

Proof usesThe Bochner formula · The divergence theorem on a manifold without boundary · Green's first identity on a manifold without boundary · The Koszul formula

TheoremThe inverse function theorem for manifolds#

If f is C^n on an open set s with 1 ≤ n, x belongs to s and is an interior point, and the differential at x is a continuous linear equivalence, then f is a C^n local diffeomorphism at x.

Mathlib's Mathlib/Geometry/Manifold/LocalDiffeomorph.lean lists this implication as a TODO.

TauCeti.isLocalDiffeomorphAt_of_mfderiv_eq.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} {𝕂 : Type u_1}
  [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3}
  [NormedAddCommGroup F] [NormedSpace 𝕂 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5}
  [TopologicalSpace G] {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7}
  [TopologicalSpace N] [ChartedSpace G N] [CompleteSpace E] {I : ModelWithCorners 𝕂 E H}
  {J : ModelWithCorners 𝕂 F G} {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold J n N] {f : M → N}
  {s : Set M} {x : M} (hf : ContMDiffOn I J n f s) (hs : IsOpen s) (hx : x ∈ s)
  (hIx : I.IsInteriorPoint x) (hn : 1 ≤ n) {e : TangentSpace I x ≃L[𝕂] TangentSpace J (f x)}
  (he : ↑e = mfderiv% f x) : IsLocalDiffeomorphAt I J n f x

Lean

Formalized in Tau Ceti as TauCeti.isLocalDiffeomorphAt_of_mfderiv_eq.

Other forms

The inverse function theorem for manifolds, global form. Formalized in Tau Ceti as TauCeti.isLocalDiffeomorph_of_mfderiv_eq.

TauCeti.isLocalDiffeomorph_of_mfderiv_eq.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} {𝕂 : Type u_1}
  [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3}
  [NormedAddCommGroup F] [NormedSpace 𝕂 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5}
  [TopologicalSpace G] {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_7}
  [TopologicalSpace N] [ChartedSpace G N] [CompleteSpace E] {I : ModelWithCorners 𝕂 E H}
  {J : ModelWithCorners 𝕂 F G} {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold J n N] {f : M → N}
  [BoundarylessManifold I M] (hf : ContMDiff I J n f) (hn : 1 ≤ n)
  (he : ∀ (y : M), ∃ e, ↑e = mfderiv% f y) : IsLocalDiffeomorph I J n f

The inverse function theorem in one variable. Formalized in Tau Ceti as TauCeti.isLocalDiffeomorph_of_deriv_ne_zero.

TauCeti.isLocalDiffeomorph_of_deriv_ne_zero.{u_1} {𝕂 : Type u_1} [RCLike 𝕂] {n : WithTop ℕ∞}
  {g : 𝕂 → 𝕂} (hg : ContDiff 𝕂 n g) (hn : 1 ≤ n) (hg' : ∀ (x : 𝕂), deriv g x ≠ 0) :
  IsLocalDiffeomorph (modelWithCornersSelf 𝕂 𝕂) (modelWithCornersSelf 𝕂 𝕂) n g

Sources

• Tau Ceti documentation: TauCeti.isLocalDiffeomorphAt_of_mfderiv_eq
• Source of TauCeti.isLocalDiffeomorphAt_of_mfderiv_eq in TauCeti/Geometry/Manifold/LocalDiffeomorph/Basic.lean

LeanTauCeti.isLocalDiffeomorphAt_of_mfderiv_eq · TauCeti.isLocalDiffeomorph_of_mfderiv_eq · TauCeti.isLocalDiffeomorph_of_deriv_ne_zero

Uses 1 · Used by 7

Proof usesThe inverse function theorem, with a C^n inverse on the whole target

Used byThe Hopf–Rinow theorem · TauCeti.Nil.semidirectProductIsomMulEquiv · The closed-subgroup theorem, with its model space · Closed normal disc theorem for a closed smooth submanifold · The relative ambient disc theorem · Smooth Euclidean tubular neighbourhood theorem · Smooth Riemannian tubular neighbourhood theorem

TheoremJacobi's formula on a manifold#

If the entries of a matrix-valued function A are differentiable at x and A x has invertible determinant, then along a tangent vector v the derivative of det A is det (A x) * trace ((A x)⁻¹ * dA (v)), where dA (v) is the matrix of the derivatives of the entries of A along v.

TauCeti.mvfderiv_det_apply.{u_1, u_2, u_3, u_4, u_5} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
  [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3}
  [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M]
  [ChartedSpace H M] {n : Type u_5} [Fintype n] [DecidableEq n] {A : M → Matrix n n 𝕜} {x : M}
  (hA : ∀ (i j : n), (MDiffAt fun y => A y i j) x) (hdet : IsUnit (A x).det)
  (v : TangentSpace I x) :
  ((d% fun y => (A y).det) x) v =
    (A x).det * ((A x)⁻¹ * Matrix.of fun i j => ((d% fun y => A y i j) x) v).trace

Lean

Formalized in Tau Ceti as TauCeti.mvfderiv_det_apply.

Sources

• Tau Ceti documentation: TauCeti.mvfderiv_det_apply
• Source of TauCeti.mvfderiv_det_apply in TauCeti/Geometry/Manifold/MFDeriv/Det.lean

LeanTauCeti.mvfderiv_det_apply

Uses 1 · Used by 1

Proof usesJacobi's inverse formula

Used byThe divergence theorem on a manifold without boundary

TheoremThe joint holomorphic implicit function theorem in charts#

Suppose G : M × N → P is holomorphic near u, and the partial derivative in the N coordinate of its representative in holomorphic charts e, d, c is invertible at u. There is a solution ψ : M × P → N, holomorphic near (u.1, G u), taking that point to u.2. Near (u, G u), the equation G (z, v) = w is equivalent to ψ (z, w) = v. In particular solutions sufficiently near u.2 are unique. Only the parameter and unknown model spaces need be assumed finite-dimensional; invertibility of the partial derivative forces the level model to have the same dimension as the unknown model. No separation or global countability assumptions are needed.

TauCeti.exists_jointImplicitFunction_of_eventually_mdifferentiableAt.{u_1, u_2, u_3, u_4, u_5, u_6}
  {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E]
  [FiniteDimensional ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [FiniteDimensional ℂ F]
  [NormedAddCommGroup K] [NormedSpace ℂ K] {M : Type u_4} {N : Type u_5} {P : Type u_6}
  [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N]
  [TopologicalSpace P] [ChartedSpace K P] {G : M × N → P} {u : M × N}
  {e : OpenPartialHomeomorph M E} {d : OpenPartialHomeomorph N F} {c : OpenPartialHomeomorph P K}
  (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ E) 1 M)
  (hd : d ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ F) 1 N)
  (hc : c ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ K) 1 P) (hu : u.1 ∈ e.source)
  (hv : u.2 ∈ d.source) (hw : G u ∈ c.source) (hG : ∀ᶠ (q : M × N) in nhds u, MDiffAt G q)
  (hinv :
    (fderiv ℂ (fun q => ↑c (G (↑e.symm q.1, ↑d.symm q.2))) (↑e u.1, ↑d u.2) ∘SL
        ContinuousLinearMap.inr ℂ E F).IsInvertible) :
  ∃ ψ,
    (∀ᶠ (p : M × P) in nhds (u.1, G u), MDiffAt ψ p) ∧
      ψ (u.1, G u) = u.2 ∧
        (∀ᶠ (p : M × P) in nhds (u.1, G u), G (p.1, ψ p) = p.2) ∧
          ∀ᶠ (q : (M × N) × P) in nhds (u, G u), G q.1 = q.2 ↔ ψ (q.1.1, q.2) = q.1.2

Lean

Formalized in Tau Ceti as TauCeti.exists_jointImplicitFunction_of_eventually_mdifferentiableAt.

Sources

• Tau Ceti documentation: TauCeti.exists_jointImplicitFunction_of_eventually_mdifferentiableAt
• Source of TauCeti.exists_jointImplicitFunction_of_eventually_mdifferentiableAt in TauCeti/Geometry/Manifold/Complex/ImplicitFunction.lean

LeanTauCeti.exists_jointImplicitFunction_of_eventually_mdifferentiableAt

Uses 1

Proof usesThe joint holomorphic implicit function theorem

TheoremThe Koszul formula#

for a Levi-Civita connection, 2 ⟪∇_X Y, Z⟫ is the Koszul expression of the metric. Mathlib's CovariantDerivative.IsLeviCivitaConnection.apply_eq is the same identity with the expression written out; this form is the one TauCeti.Manifold.koszul controls.

CovariantDerivative.IsLeviCivitaConnection.two_inner_eq_koszul.{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]
  [Bundle.RiemannianBundle fun x => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 2 M]
  [IsContMDiffRiemannianBundle I 1 E fun x => TangentSpace I x]
  {cov : CovariantDerivative I E fun x => TangentSpace I x} {X Y Z : (x : M) → TangentSpace I x}
  {x : M} (h : CovariantDerivative.IsLeviCivitaConnection I cov)
  (hX : (MDiffAt fun x => ⟨x, X x⟩) x) (hY : (MDiffAt fun x => ⟨x, Y x⟩) x)
  (hZ : (MDiffAt fun x => ⟨x, Z x⟩) x) :
  2 * inner ℝ ((↑cov Y x) (X x)) (Z x) = TauCeti.Manifold.koszul I X Y Z x

Lean

Formalized in Tau Ceti as CovariantDerivative.IsLeviCivitaConnection.two_inner_eq_koszul.

Other forms

The Koszul formula. Formalized in Tau Ceti as CovariantDerivative.two_inner_leviCivitaConnection_eq_koszul.

CovariantDerivative.two_inner_leviCivitaConnection_eq_koszul.{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]
  [Bundle.RiemannianBundle fun x => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 2 M]
  [IsContMDiffRiemannianBundle I 1 E fun x => TangentSpace I x] {X Y Z : (x : M) → TangentSpace I x}
  {x : M} (hX : (MDiffAt fun x => ⟨x, X x⟩) x) (hY : (MDiffAt fun x => ⟨x, Y x⟩) x)
  (hZ : (MDiffAt fun x => ⟨x, Z x⟩) x) :
  2 * inner ℝ ((↑(CovariantDerivative.leviCivitaConnection I M) Y x) (X x)) (Z x) =
    TauCeti.Manifold.koszul I X Y Z x

The Koszul formula. Formalized in Tau Ceti as TauCeti.Manifold.ContMDiffNondegenerateMetric.IsLeviCivitaConnection.two_apply_eq_koszul.

TauCeti.Manifold.ContMDiffNondegenerateMetric.IsLeviCivitaConnection.two_apply_eq_koszul.{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]
  [IsManifold I (↑⊤) M] {g : TauCeti.Manifold.ContMDiffNondegenerateMetric}
  {cov : CovariantDerivative I E fun x => TangentSpace I x} {X Y Z : (x : M) → TangentSpace I x}
  {x : M} [FiniteDimensional ℝ E] (h : g.IsLeviCivitaConnection cov)
  (hX : (MDiffAt fun x => ⟨x, X x⟩) x) (hY : (MDiffAt fun x => ⟨x, Y x⟩) x)
  (hZ : (MDiffAt fun x => ⟨x, Z x⟩) x) :
  2 * ((g.toContMDiffSection x) ((↑cov Y x) (X x))) (Z x) = g.koszul X Y Z x

The Koszul formula through a local isometry. Formalized in Tau Ceti as TauCeti.Manifold.ContMDiffNondegenerateMetric.IsLocalIsometry.two_apply_mfderiv_eq_koszul.

TauCeti.Manifold.ContMDiffNondegenerateMetric.IsLocalIsometry.two_apply_mfderiv_eq_koszul.{u_1, u_2,
    u_3, u_4, u_5, u_6}
  {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]
  [IsManifold I (↑⊤) M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_5}
  [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N]
  [ChartedSpace H' N] [IsManifold J (↑⊤) N] {g : TauCeti.Manifold.ContMDiffNondegenerateMetric}
  {g' : TauCeti.Manifold.ContMDiffNondegenerateMetric} {f : M → N}
  {X Y Z : (y : N) → TangentSpace J y} {x : M} [FiniteDimensional ℝ E]
  {cov : CovariantDerivative I E fun x => TangentSpace I x} (hf : g.IsLocalIsometry g' f)
  (h : g.IsLeviCivitaConnection cov) (hX : (MDiffAt fun y => ⟨y, X y⟩) (f x))
  (hY : (MDiffAt fun y => ⟨y, Y y⟩) (f x)) (hZ : (MDiffAt fun y => ⟨y, Z y⟩) (f x))
  {v : TangentSpace I x} (hXv : X (f x) = (mfderiv% f x) v) :
  2 *
      ((g'.toContMDiffSection (f x)) ((mfderiv% f x) ((↑cov (VectorField.mpullback I J f Y) x) v)))
        (Z (f x)) =
    g'.koszul X Y Z (f x)

Sources

• Tau Ceti documentation: CovariantDerivative.IsLeviCivitaConnection.two_inner_eq_koszul
• Source of CovariantDerivative.IsLeviCivitaConnection.two_inner_eq_koszul in TauCeti/Geometry/Manifold/VectorBundle/CovariantDerivative/LeviCivita/Basic.lean

LeanCovariantDerivative.IsLeviCivitaConnection.two_inner_eq_koszul · CovariantDerivative.two_inner_leviCivitaConnection_eq_koszul · TauCeti.Manifold.ContMDiffNondegenerateMetric.IsLeviCivitaConnection.two_apply_eq_koszul · TauCeti.Manifold.ContMDiffNondegenerateMetric.IsLocalIsometry.two_apply_mfderiv_eq_koszul

Used by 36

Used byA compact Riemannian manifold is geodesically complete · The first variation of the Levi-Civita connection · The Gauss lemma · The Hopf–Rinow theorem · TauCeti.Nil.semidirectProductIsomMulEquiv · TauCeti.UpperHalfSpace.hyperbolicMetric · Thurston's Euler class inequality · Yazdi's theorem refutes the Euler class one conjecture · Closed normal disc theorem for a closed smooth submanifold · Green's first identity on a manifold without boundary · Green's second identity on a manifold without boundary · The Bochner formula · The Christoffel formula of the first kind · The contracted Ricci identity for the gradient · The divergence theorem on a manifold without boundary · The Gauss formula · The integrated Bochner identity · The Lichnerowicz estimate · The Ricci identity · Smooth Riemannian tubular neighbourhood theorem · Bundle.ContMDiffRiemannianMetric.concordant_iff_exists_isCollaredConcordance · Bundle.ContMDiffRiemannianMetric.equivalence_concordant · Bundle.ContMDiffRiemannianMetric.HasPositiveScalarCurvature · Compact families of metrics of positive scalar curvature have a uniform scalar gap · Scalar curvature of the round sphere · Shrinking a compact factor of positive scalar curvature · The scalar curvature of a product metric · Bundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat · Local conformal flatness forces the Weyl tensor to vanish · Scalar curvature of a conformal metric · TauCeti.Yamabe.conformalLaplacian · The Yamabe equation · Volume-normalized total scalar curvature of a conformal metric · Weyl–Schouten in dimension three, on a model space · Weyl tensor under conformal change · Li's theorem refutes Waldhausen's conjecture

TheoremThe Lichnerowicz estimate#

On a closed manifold of dimension n ≥ 2 with Ric ≥ (n - 1) k g, every positive eigenvalue with a nonzero smooth eigenfunction is at least n k. The eigen-equation is stated for the native Δ = div grad. The real lower bound k need not be positive.

TauCeti.Manifold.finrank_mul_le_of_laplaceBeltrami_eq_neg_mul.{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] [Bundle.RiemannianBundle fun x => TangentSpace I x] {f : M → ℝ} {k lam : ℝ}
  [T2Space M] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun x => TangentSpace I x]
  [I.Boundaryless] [CompactSpace M] [MeasurableSpace M] [BorelSpace M] (hn : 2 ≤ Module.finrank ℝ E)
  (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hlam : 0 < lam)
  (heig : ∀ (x : M), TauCeti.Manifold.laplaceBeltrami I f x = -lam * f x) (hne : ∃ x, f x ≠ 0)
  (hRic :
    ∀ (x : M) (v : TangentSpace I x),
      (↑(Module.finrank ℝ E) - 1) * k * ‖v‖ ^ 2 ≤
        (((CovariantDerivative.leviCivitaConnection I M).ricciTensor x) v) v) :
  ↑(Module.finrank ℝ E) * k ≤ lam

Lean

Formalized in Tau Ceti as TauCeti.Manifold.finrank_mul_le_of_laplaceBeltrami_eq_neg_mul.

Sources

• Tau Ceti documentation: TauCeti.Manifold.finrank_mul_le_of_laplaceBeltrami_eq_neg_mul
• Source of TauCeti.Manifold.finrank_mul_le_of_laplaceBeltrami_eq_neg_mul in TauCeti/Geometry/Manifold/Riemannian/Lichnerowicz/Basic.lean

LeanTauCeti.Manifold.finrank_mul_le_of_laplaceBeltrami_eq_neg_mul

Uses 4

Proof usesThe Bochner formula · The divergence theorem on a manifold without boundary · Green's first identity on a manifold without boundary · The Koszul formula

TheoremThe local Frobenius theorem (TauCeti.IsInvolutiveDistribution.exists_flatChart)#

An involutive C^m distribution D of rank k, for 1 ≤ m, on a C^n manifold with m + 1 ≤ n, modelled on a finite-dimensional real space, is constant in a suitable chart around any interior point x: there are a chart e of the C^m maximal atlas whose domain contains x and a k-dimensional subspace W of the model space such that the differential of I ∘ e carries D y onto W at every point y of the domain of e. On a boundaryless manifold BoundarylessManifold.isInteriorPoint gives the interior hypothesis at every point.

TauCeti.IsInvolutiveDistribution.exists_flatChart.{u, u_1, u_2} {E : Type u} {H : Type u_1}
  {M : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E]
  [IsManifold I 1 M] {m : ℕ∞} (hm : 1 ≤ m) {n : WithTop ℕ∞} (hmn : ↑m + 1 ≤ n) [IsManifold I n M]
  {k : ℕ} {D : (x : M) → Submodule ℝ (TangentSpace I x)}
  (hinv : TauCeti.IsInvolutiveDistribution I D) (hD : TauCeti.IsContMDiffDistribution I (↑m) k D)
  {x : M} (hx : I.IsInteriorPoint x) :
  ∃ e W,
    e ∈ IsManifold.maximalAtlas I (↑m) M ∧
      x ∈ e.source ∧
        Module.finrank ℝ ↥W = k ∧ ∀ y ∈ e.source, Submodule.map (↑(mfderiv% (↑I ∘ ↑e) y)) (D y) = W

Lean

Formalized in Tau Ceti as TauCeti.IsInvolutiveDistribution.exists_flatChart.

Other forms

The local Frobenius theorem in product coordinates. Formalized in Tau Ceti as TauCeti.IsDistributionFrameOn.exists_openPartialHomeomorph_map_fderiv_eq_ker_snd.

TauCeti.IsDistributionFrameOn.exists_openPartialHomeomorph_map_fderiv_eq_ker_snd.{u} {E F : Type u}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F]
  [NormedSpace ℝ F] [FiniteDimensional ℝ F] {n : ℕ∞} {D : E × F → Submodule ℝ (E × F)}
  {U : Set (E × F)} (hU : IsOpen U)
  {X : Fin (Module.finrank ℝ E) → (p : E × F) → TangentSpace (modelWithCornersSelf ℝ (E × F)) p}
  (hX : TauCeti.IsDistributionFrameOn (modelWithCornersSelf ℝ (E × F)) (↑n + 1) D X U)
  (hinv : TauCeti.IsInvolutiveDistributionOn (modelWithCornersSelf ℝ (E × F)) D U) {p₀ : E × F}
  (hp₀U : p₀ ∈ U) (hp₀ : Disjoint (D p₀) (LinearMap.fst ℝ E F).ker) :
  ∃ φ,
    p₀ ∈ φ.source ∧
      ↑φ p₀ = p₀ ∧
        ContDiffOn ℝ (↑n + 1) (↑φ) φ.source ∧
          ContDiffOn ℝ (↑n + 1) (↑φ.symm) φ.target ∧
            ∀ p ∈ φ.source, Submodule.map (↑(fderiv ℝ (↑φ) p)) (D p) = (LinearMap.snd ℝ E F).ker

Sources

• Tau Ceti documentation: TauCeti.IsInvolutiveDistribution.exists_flatChart
• Source of TauCeti.IsInvolutiveDistribution.exists_flatChart in TauCeti/Geometry/Manifold/Distribution/FlatChart.lean

LeanTauCeti.IsInvolutiveDistribution.exists_flatChart · TauCeti.IsDistributionFrameOn.exists_openPartialHomeomorph_map_fderiv_eq_ker_snd

Uses 1

Proof usesThe inverse function theorem, with a C^n inverse on the whole target

TheoremMilnor's cell attachment theorem#

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 with pairwise disjoint sources, indexed by the critical points p on the level f⁻¹(c), with ψ p p = 0, with the closed ball of radius √(2ε₀) in the target of ψ p, and in which f = c - Σ_{i < λ} yᵢ² + Σ_{i ≥ λ} yᵢ², where λ is the Morse index of f at p. For every width 0 < ε ≤ ε₀, the cell at p is the disc {‖y‖² ≤ ε, yᵢ = 0 for i ≥ λ} of its negative coordinates, read in M through ψ p.

The lower sublevel {f ≤ c - ε} with these cells attached is a strong deformation retract of {f ≤ c + ε}, for every such ε: there is a retraction of {f ≤ c + ε} onto it, and a homotopy in {f ≤ c + ε} from this retraction to the identity which fixes it pointwise.

TauCeti.IsMorse.exists_sublevel_union_cells_deformation.{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 → ℝ} {c : ℝ}
  [FiniteDimensional ℝ E] [I.Boundaryless] [IsManifold I (↑⊤) M] [T2Space M]
  (hf : TauCeti.IsMorse I f) {δ : ℝ} (hδ : 0 < δ)
  (hcompact : IsCompact (f ⁻¹' Set.Icc (c - δ) (c + δ))) :
  ∃ ε₀,
    0 < ε₀ ∧
      ε₀ ≤ δ ∧
        ∃ ψ,
          Pairwise (Function.onFun Disjoint fun p => (ψ p).source) ∧
            (∀ (p : ↑(TauCeti.criticalPoints I f ∩ f ⁻¹' {c})),
                ↑p ∈ (ψ p).source ∧
                  ↑(ψ 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) ∧
              ∀ (ε : ℝ),
                0 < ε →
                  ε ≤ ε₀ →
                    ∃ r,
                      (∀
                          (x :
                            ↑({x | f x ≤ c + ε} ∩
                                ({x | f x ≤ c - ε} ∪
                                  ⋃ p,
                                    (ψ p).source ∩
                                      ↑(ψ p).toPartialEquiv ⁻¹'
                                        {y |
                                          ‖y‖ ^ 2 ≤ ε ∧
                                            ∀ (i : Fin (Module.finrank ℝ E)),
                                              TauCeti.manifoldMorseIndex I f ↑p ≤ ↑i →
                                                y.ofLp i = 0}))),
                          r ((ContinuousMap.inclusion ⋯) x) = x) ∧
                        Nonempty
                          (((ContinuousMap.inclusion ⋯).comp r).HomotopyRel
                            (ContinuousMap.id ↑{x | f x ≤ c + ε})
                            {x |
                              ↑x ∈
                                {x | f x ≤ c - ε} ∪
                                  ⋃ p,
                                    (ψ p).source ∩
                                      ↑(ψ p).toPartialEquiv ⁻¹'
                                        {y |
                                          ‖y‖ ^ 2 ≤ ε ∧
                                            ∀ (i : Fin (Module.finrank ℝ E)),
                                              TauCeti.manifoldMorseIndex I f ↑p ≤ ↑i →
                                                y.ofLp i = 0}})

Lean

Formalized in Tau Ceti as TauCeti.IsMorse.exists_sublevel_union_cells_deformation.

Other forms

Milnor's cell attachment theorem in CW form. Formalized in Tau Ceti as TauCeti.IsMorse.exists_relCWComplex_sublevel_deformation.

TauCeti.IsMorse.exists_relCWComplex_sublevel_deformation.{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 → ℝ} {c δ : ℝ}
  (hf : TauCeti.IsMorse I f) (hδ : 0 < δ) (hcompact : IsCompact (f ⁻¹' Set.Icc (c - δ) (c + δ))) :
  ∃ ε,
    0 < ε ∧
      ε ≤ δ ∧
        ∃ C x,
          ∃ (_ : Topology.RelCWComplex.Finite C) (hC : C ⊆ {x | f x ≤ c + ε}),
            (∀ (m : ℕ),
                Nonempty
                  (Topology.RelCWComplex.cell C m ≃
                    { p // TauCeti.manifoldMorseIndex I f ↑p = m })) ∧
              ∃ r,
                (∀ (x : ↑C), r ((ContinuousMap.inclusion hC) x) = x) ∧
                  Nonempty
                    (((ContinuousMap.inclusion hC).comp r).HomotopyRel
                      (ContinuousMap.id ↑{x | f x ≤ c + ε}) {x | ↑x ∈ C})

Milnor's cell attachment theorem, in pushout form. Formalized in Tau Ceti as TauCeti.IsMorse.exists_morseCellAttachment_deformation.

TauCeti.IsMorse.exists_morseCellAttachment_deformation.{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 → ℝ} {c : ℝ} (hf : TauCeti.IsMorse I f)
  {δ : ℝ} (hδ : 0 < δ) (hcompact : IsCompact (f ⁻¹' Set.Icc (c - δ) (c + δ))) :
  ∃ ε,
    ∃ (hε : 0 < ε),
      ε ≤ δ ∧
        ∃ ψ,
          Pairwise (Function.onFun Disjoint fun p => (ψ p).source) ∧
            (∀ (p : ↑(TauCeti.criticalPoints I f ∩ f ⁻¹' {c})),
                ↑p ∈ (ψ p).source ∧ ↑(ψ p).toPartialEquiv ↑p = 0) ∧
              ∃ (hball :
                ∀ (p : ↑(TauCeti.criticalPoints I f ∩ f ⁻¹' {c})),
                  Metric.closedBall 0 √ε ⊆ (ψ p).target)
                (hψ :
                ∀ (p : ↑(TauCeti.criticalPoints I f ∩ f ⁻¹' {c})),
                  ∀ y ∈ (ψ p).source,
                    f y =
                      c +
                        ∑ i,
                          (if ↑i < TauCeti.manifoldMorseIndex I f ↑p then -1 else 1) *
                            (↑(ψ p).toPartialEquiv y).ofLp i ^ 2),
                ∃ g,
                  Function.LeftInverse ⇑g
                      ⇑(CategoryTheory.ConcreteCategory.hom
                          (TauCeti.morseCellComparison (fun p => (ψ p).toOpenPartialHomeomorph)
                            (fun x => TauCeti.manifoldMorseIndex I f ↑x) ⋯ ⋯ hball hψ)) ∧
                    (ContinuousMap.id ↑↧↑{x | f x ≤ c + ε}).HomotopicRel
                      ((TopCat.Hom.hom
                            (TauCeti.morseCellComparison (fun p => (ψ p).toOpenPartialHomeomorph)
                              (fun x => TauCeti.manifoldMorseIndex I f ↑x) ⋯ ⋯ hball hψ)).comp
                        g)
                      (Set.range
                        ⇑(CategoryTheory.ConcreteCategory.hom
                            (TauCeti.morseCellComparison (fun p => (ψ p).toOpenPartialHomeomorph)
                              (fun x => TauCeti.manifoldMorseIndex I f ↑x) ⋯ ⋯ hball hψ)))

Sources

• Tau Ceti documentation: TauCeti.IsMorse.exists_sublevel_union_cells_deformation
• Source of TauCeti.IsMorse.exists_sublevel_union_cells_deformation in TauCeti/Geometry/Manifold/Morse/Cell/Attachment.lean

LeanTauCeti.IsMorse.exists_sublevel_union_cells_deformation · TauCeti.IsMorse.exists_relCWComplex_sublevel_deformation · TauCeti.IsMorse.exists_morseCellAttachment_deformation

Uses 2 · Used by 3

Proof usesAdmissible Morse charts at a critical level · Deformation of sublevels across a band without critical points (Milnor, Theorem 3.1)

Used byThe 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

TheoremMilnor's index bound on a smooth affine complete intersection#

On the common zero set in ℂ^σ of a polynomial family with surjective Jacobian at every common zero, every critical point of the Euclidean squared distance from a point a has real Morse index at most the complex dimension |σ| - |ι| of the zero set.

TauCeti.manifoldMorseIndex_norm_sq_sub_toLp_affineZeroLocus_le.{u_1, u_2} {σ : Type u_1}
  {ι : Type u_2} [Fintype σ] [Fintype ι] {p : ι → MvPolynomial σ ℂ}
  (hp : ∀ x ∈ TauCeti.affineZeroLocus p, Function.Surjective (TauCeti.jacobiMatrixAt p x).mulVec)
  (a : EuclideanSpace ℂ σ) (x : ↑(TauCeti.affineZeroLocus p))
  (hcrit : (d% fun y => ‖WithLp.toLp 2 ↑y - a‖ ^ 2) x = 0) :
  TauCeti.manifoldMorseIndex (modelWithCornersSelf ℝ (Fin (Fintype.card σ - Fintype.card ι) → ℂ))
      (fun y => ‖WithLp.toLp 2 ↑y - a‖ ^ 2) x ≤
    Fintype.card σ - Fintype.card ι

Lean

Formalized in Tau Ceti as TauCeti.manifoldMorseIndex_norm_sq_sub_toLp_affineZeroLocus_le.

Sources

• Tau Ceti documentation: TauCeti.manifoldMorseIndex_norm_sq_sub_toLp_affineZeroLocus_le
• Source of TauCeti.manifoldMorseIndex_norm_sq_sub_toLp_affineZeroLocus_le in TauCeti/Geometry/Manifold/RegularValue/Polynomial.lean

LeanTauCeti.manifoldMorseIndex_norm_sq_sub_toLp_affineZeroLocus_le

Uses 2

Proof usesThe index bound for strongly q-pseudoconvex functions on a complex manifold · TauCeti.leviForm

TheoremNoncompact Euclidean tubular neighbourhood theorem#

A C² immersion inducing the source topology admits a positive continuous radius on which its normal addition map is an open embedding.

TauCeti.exists_isOpenEmbedding_normalTubeOfRadius.{u_1, u_2, u_3, u_4} {V : Type u_1} {E : Type u_2}
  {H : Type u_3} {M : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
  [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ V] [FiniteDimensional ℝ E]
  [I.Boundaryless] [IsManifold I 2 M] {f : M → V} (hf : ContMDiff I (modelWithCornersSelf ℝ V) 2 f)
  (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (hind : Topology.IsInducing f) :
  ∃ r,
    (∀ (x : M), 0 < r x) ∧
      Topology.IsOpenEmbedding
        ((TauCeti.normalTubeOfRadius I f ⇑r).domRestrict fun p => f p.1 + p.2)

Lean

Formalized in Tau Ceti as TauCeti.exists_isOpenEmbedding_normalTubeOfRadius.

Sources

• Tau Ceti documentation: TauCeti.exists_isOpenEmbedding_normalTubeOfRadius
• Source of TauCeti.exists_isOpenEmbedding_normalTubeOfRadius in TauCeti/Geometry/Manifold/TubularNeighborhood/Noncompact.lean

LeanTauCeti.exists_isOpenEmbedding_normalTubeOfRadius

Uses 1 · Used by 1

Proof usesThe inverse function theorem, with a C^n inverse on the whole target

Used bySmooth Euclidean tubular neighbourhood theorem

TheoremThe oriented common-centre disc theorem#

Two smooth embeddings that preserve the chosen orientations at the origin and have the same centre are smoothly isotopic relative to that centre. No orientation condition away from the origin is required.

TauCeti.SmoothEmbedding.exists_smoothIsotopy_of_isOrientationPreservingAt.{u_1, u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {M : Type u_2}
  [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M]
  {ι : Type u_3} [Fintype ι]
  (f g : TauCeti.SmoothEmbedding (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E) (↑⊤) E M)
  (hcentre : f 0 = g 0) (o : TauCeti.Manifold.Orientation (modelWithCornersSelf ℝ E) E ι)
  (oM : TauCeti.Manifold.Orientation (modelWithCornersSelf ℝ E) M ι)
  (hf : o.IsOrientationPreservingAt oM (⇑f) 0) (hg : o.IsOrientationPreservingAt oM (⇑g) 0) :
  ∃ G, ∀ (t : ↑unitInterval), G (t, 0) = f 0

Lean

Formalized in Tau Ceti as TauCeti.SmoothEmbedding.exists_smoothIsotopy_of_isOrientationPreservingAt.

Sources

• Tau Ceti documentation: TauCeti.SmoothEmbedding.exists_smoothIsotopy_of_isOrientationPreservingAt
• Source of TauCeti.SmoothEmbedding.exists_smoothIsotopy_of_isOrientationPreservingAt in TauCeti/Geometry/Manifold/SmoothIsotopy/Orientation.lean

LeanTauCeti.SmoothEmbedding.exists_smoothIsotopy_of_isOrientationPreservingAt

Uses 1

Proof usesThe disc theorem in a manifold

TheoremThe Poincaré lemma on manifolds#

A C^r form of positive degree, r ≥ 1, that is closed near a point x is, on a neighbourhood of x, the exterior derivative of a C^r form defined on the whole manifold. The manifold may have boundary or corners.

The coefficient space is complete: with values in the finitely supported sequences there is a smooth closed 1-form on ℝ with no local primitive. Finite dimensionality of the model and the Hausdorff property are used only to cut the local primitive off by a smooth bump function.

TauCeti.exists_mextDeriv_eq_nhds.{u_1, u_2, u_3, u_4} {E : Type u_1} {H : Type u_2} {M : Type u_3}
  {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F]
  [NormedSpace ℝ F] [CompleteSpace F] {k : ℕ} [FiniteDimensional ℝ E] [T2Space M]
  [IsManifold I (↑⊤) M] {r : ℕ∞} (hr : 1 ≤ r) {φ : TauCeti.RoughForm I M F (k + 1)}
  (hφ : TauCeti.IsSmoothForm I (↑r) φ) {x : M}
  (hclosed : ∀ᶠ (y : M) in nhds x, TauCeti.mextDeriv φ y = 0) :
  ∃ U ∈ nhds x, ∃ ψ, TauCeti.IsSmoothForm I (↑r) ψ ∧ ∀ y ∈ U, TauCeti.mextDeriv ψ y = φ y

Lean

Formalized in Tau Ceti as TauCeti.exists_mextDeriv_eq_nhds.

Other forms

The Poincaré lemma on a normed space. Formalized in Tau Ceti as TauCeti.exactForms_succ_eq_closedForms_normedSpace.

TauCeti.exactForms_succ_eq_closedForms_normedSpace.{u_1} (E : Type u_1) [NormedAddCommGroup E]
  [NormedSpace ℝ E] (k : ℕ) :
  TauCeti.exactForms (modelWithCornersSelf ℝ E) E (k + 1) =
    TauCeti.closedForms (modelWithCornersSelf ℝ E) E (k + 1)

Sources

• Tau Ceti documentation: TauCeti.exists_mextDeriv_eq_nhds
• Source of TauCeti.exists_mextDeriv_eq_nhds in TauCeti/Geometry/Manifold/DifferentialForm/Poincare.lean

LeanTauCeti.exists_mextDeriv_eq_nhds · TauCeti.exactForms_succ_eq_closedForms_normedSpace

Uses 2 · Used by 4

Proof usesThe Poincaré lemma · The relative Poincaré lemma

Used byThe compactly supported Poincaré lemma on the line · The de Rham cohomology of a normed space vanishes in positive degrees · The fundamental theorem of calculus for path classes · Stokes' theorem on singular 1-chains

TheoremThe Poincaré–Wirtinger inequality on a closed Riemannian manifold#

Let 1 ≤ p < ∞, on a compact connected manifold without boundary with a continuous Riemannian metric. There is a constant C such that ‖u - ⨍ u‖_{Lᵖ} ≤ C ‖∇u‖_{Lᵖ} for every C¹ function u, where ⨍ u is the mean of u with respect to the Riemannian volume.

TauCeti.Manifold.exists_eLpNorm_sub_average_le_mul_eLpNorm_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} [I.Boundaryless] {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] [MeasurableSpace M] [BorelSpace M]
  [CompactSpace M] [PreconnectedSpace M] {p : ENNReal} (hp : 1 ≤ p) (hp' : p ≠ ⊤) :
  ∃ C,
    ∀ (u : M → ℝ),
      ContMDiff I (modelWithCornersSelf ℝ ℝ) 1 u →
        MeasureTheory.eLpNorm (fun x => u x - ⨍ (y : M), u y ∂TauCeti.riemannianVolume I M) p
            (TauCeti.riemannianVolume I M) ≤
          ↑C *
            MeasureTheory.eLpNorm (fun x => ‖TauCeti.Manifold.mgradient I u x‖) p
              (TauCeti.riemannianVolume I M)

Lean

Formalized in Tau Ceti as TauCeti.Manifold.exists_eLpNorm_sub_average_le_mul_eLpNorm_mgradient.

Sources

• Tau Ceti documentation: TauCeti.Manifold.exists_eLpNorm_sub_average_le_mul_eLpNorm_mgradient
• Source of TauCeti.Manifold.exists_eLpNorm_sub_average_le_mul_eLpNorm_mgradient in TauCeti/Geometry/Manifold/Riemannian/Poincare.lean

LeanTauCeti.Manifold.exists_eLpNorm_sub_average_le_mul_eLpNorm_mgradient

Uses 2

Proof usesHölder's bound on an average · The Poincaré–Wirtinger inequality on a ball

TheoremThe regular-fibre theorem#

A regular fibre over an interior value of a C^m map, m ≥ 1, from a finite-dimensional boundaryless real manifold to a finite-dimensional real manifold admits a C^m manifold structure of dimension dim M - dim N, with its subspace topology, for which the inclusion is a C^m smooth embedding and has tangent image ker df. No separation or countability assumptions are needed, and an empty fibre is allowed.

TauCeti.exists_regularFiber_smoothEmbedding.{u_1, u_2, u_3, u_4, u_5, u_6} {E : Type u_1}
  {H : Type u_2} {M : Type u_3} {F : Type u_4} {G : Type u_5} {N : Type u_6} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
  [I.Boundaryless] {m : WithTop ℕ∞} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I m M]
  [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace G]
  {J : ModelWithCorners ℝ F G} [TopologicalSpace N] [ChartedSpace G N] [IsManifold J m N]
  {f : M → N} {c : N} (hm : 1 ≤ m) (hf : ContMDiff I J m f) (hc : J.IsInteriorPoint c)
  (hreg : TauCeti.IsRegularValue I J f c) :
  ∃ a,
    IsManifold (modelWithCornersSelf ℝ (Fin (Module.finrank ℝ E - Module.finrank ℝ F) → ℝ)) m
        { x // f x = c } ∧
      Manifold.IsSmoothEmbedding
          (modelWithCornersSelf ℝ (Fin (Module.finrank ℝ E - Module.finrank ℝ F) → ℝ)) I m
          Subtype.val ∧
        ∀ (z : { x // f x = c }), (↑(mfderiv% Subtype.val z)).range = (↑(mfderiv% f ↑z)).ker

Lean

Formalized in Tau Ceti as TauCeti.exists_regularFiber_smoothEmbedding.

Sources

• Tau Ceti documentation: TauCeti.exists_regularFiber_smoothEmbedding
• Source of TauCeti.exists_regularFiber_smoothEmbedding in TauCeti/Geometry/Manifold/RegularValue/ManifoldLevel.lean

LeanTauCeti.exists_regularFiber_smoothEmbedding

Uses 2

Proof usesHomeomorph.pullbackChartedSpace · Homeomorph.pullbackDiffeomorph

TheoremThe relative ambient disc theorem#

Let f and g be smooth embeddings of E into a Hausdorff boundaryless manifold M modelled on E, preserving the orientations o of E and oM of M at the origin, with images in a preconnected open set U. On every compact subset A of E, g is f followed by the final diffeomorphism of a smooth diffeotopy of M fixing every point outside a compact subset of U. Points outside U, for instance protected discs and collars, are not moved.

TauCeti.SmoothEmbedding.exists_diffeotopy_eqOn_of_isOrientationPreservingAt_of_range_subset.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {M : Type u_2}
  [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M]
  {ι : Type u_3} [Fintype ι] [T2Space M] {U : Set M} (hU : IsOpen U) (hUc : IsPreconnected U)
  (f g : TauCeti.SmoothEmbedding (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E) (↑⊤) E M)
  (hfU : Set.range ⇑f ⊆ U) (hgU : Set.range ⇑g ⊆ U)
  (o : TauCeti.Manifold.Orientation (modelWithCornersSelf ℝ E) E ι)
  (oM : TauCeti.Manifold.Orientation (modelWithCornersSelf ℝ E) M ι)
  (hf : o.IsOrientationPreservingAt oM (⇑f) 0) (hg : o.IsOrientationPreservingAt oM (⇑g) 0)
  {A : Set E} (hA : IsCompact A) :
  ∃ Φ K,
    IsCompact K ∧
      K ⊆ U ∧
        (∀ (t : ↑unitInterval), ∀ y ∉ K, (fun p => (Φ.toDiffeomorph p).2) (t, y) = y) ∧
          Set.EqOn (⇑Φ.final ∘ ⇑f) (⇑g) A

Informally uses

• The ambient disc theorem in a manifold

Lean

Formalized in Tau Ceti as TauCeti.SmoothEmbedding.exists_diffeotopy_eqOn_of_isOrientationPreservingAt_of_range_subset.

Sources

• Tau Ceti documentation: TauCeti.SmoothEmbedding.exists_diffeotopy_eqOn_of_isOrientationPreservingAt_of_range_subset
• Source of TauCeti.SmoothEmbedding.exists_diffeotopy_eqOn_of_isOrientationPreservingAt_of_range_subset in TauCeti/Geometry/Manifold/SmoothIsotopy/Orientation.lean

LeanTauCeti.SmoothEmbedding.exists_diffeotopy_eqOn_of_isOrientationPreservingAt_of_range_subset

Uses 1 · Used by 1

Proof usesThe inverse function theorem for manifolds

Used byThe ambient disc theorem in a manifold

TheoremThe Ricci identity#

For a torsion-free connection ∇ᵀ on the tangent bundle, the antisymmetric part of the second covariant derivative of a smooth section σ is the curvature of ∇ applied to σ: ∇²σ(u, v) - ∇²σ(v, u) = R(u, v) σ.

CovariantDerivative.secondCovariantDerivative_sub_swap_of_isTorsionFree.{u_1, u_2, u_3, u_4, u_5}
  {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]
  [IsManifold I (↑⊤) M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5}
  [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)]
  [(x : M) → _root_.Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)]
  [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [FiberBundle F V]
  [VectorBundle ℝ F V] (cov : CovariantDerivative I F V) [cov.ContMDiffCovariantDerivative ↑⊤]
  (covT : CovariantDerivative I E (TangentSpace I)) {σ : (y : M) → V y} [FiniteDimensional ℝ E]
  [T2Space M] [FiniteDimensional ℝ F] [ContMDiffVectorBundle (↑⊤) F V I] (ht : covT.IsTorsionFree)
  (hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun y => ⟨y, σ y⟩) (x : M)
  (u v : TangentSpace I x) :
  ((cov.secondCovariantDerivative covT σ x) u) v - ((cov.secondCovariantDerivative covT σ x) v) u =
    (((cov.curvatureTensor x) u) v) (σ x)

Lean

Formalized in Tau Ceti as CovariantDerivative.secondCovariantDerivative_sub_swap_of_isTorsionFree.

Other forms

The Ricci identity, with its torsion correction. Formalized in Tau Ceti as CovariantDerivative.secondCovariantDerivative_sub_swap.

CovariantDerivative.secondCovariantDerivative_sub_swap.{u_1, u_2, u_3, u_4, u_5} {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]
  [IsManifold I (↑⊤) M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5}
  [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)]
  [(x : M) → _root_.Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)]
  [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [FiberBundle F V]
  [VectorBundle ℝ F V] (cov : CovariantDerivative I F V) [cov.ContMDiffCovariantDerivative ↑⊤]
  (covT : CovariantDerivative I E (TangentSpace I)) {σ : (y : M) → V y} [FiniteDimensional ℝ E]
  [T2Space M] [FiniteDimensional ℝ F] [ContMDiffVectorBundle (↑⊤) F V I]
  (hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun y => ⟨y, σ y⟩) (x : M)
  (u v : TangentSpace I x) :
  ((cov.secondCovariantDerivative covT σ x) u) v - ((cov.secondCovariantDerivative covT σ x) v) u =
    (((cov.curvatureTensor x) u) v) (σ x) - (↑cov σ x) (((covT.torsion x) u) v)

The Ricci identity for the Hessian. Formalized in Tau Ceti as TauCeti.Manifold.mvfderiv_hessian_sub_swap.

TauCeti.Manifold.mvfderiv_hessian_sub_swap.{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 (↑⊤) M] [Bundle.RiemannianBundle fun x => TangentSpace I x]
  [IsContMDiffRiemannianBundle I (↑⊤) E fun x => TangentSpace I x] {φ : M → ℝ}
  (hφ : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) φ) {X Y Z : (x : M) → TangentSpace I x}
  (hX : ContMDiff I I.tangent ↑⊤ fun x => ⟨x, X x⟩)
  (hY : ContMDiff I I.tangent ↑⊤ fun x => ⟨x, Y x⟩)
  (hZ : ContMDiff I I.tangent ↑⊤ fun x => ⟨x, Z x⟩) (x : M) :
  ((d% fun y => TauCeti.Manifold.hessian I φ y (X y) (Y y)) x) (Z x) -
              ((d% fun y => TauCeti.Manifold.hessian I φ y (X y) (Z y)) x) (Y x) -
            TauCeti.Manifold.hessian I φ x
              ((↑(CovariantDerivative.leviCivitaConnection I M) X x) (Z x)) (Y x) -
          TauCeti.Manifold.hessian I φ x (X x)
            ((↑(CovariantDerivative.leviCivitaConnection I M) Y x) (Z x)) +
        TauCeti.Manifold.hessian I φ x ((↑(CovariantDerivative.leviCivitaConnection I M) X x) (Y x))
          (Z x) +
      TauCeti.Manifold.hessian I φ x (X x)
        ((↑(CovariantDerivative.leviCivitaConnection I M) Z x) (Y x)) =
    inner ℝ
      (((((CovariantDerivative.leviCivitaConnection I M).curvatureTensor x) (Z x)) (Y x))
        (TauCeti.Manifold.mgradient I φ x))
      (X x)

Sources

• Tau Ceti documentation: CovariantDerivative.secondCovariantDerivative_sub_swap_of_isTorsionFree
• Source of CovariantDerivative.secondCovariantDerivative_sub_swap_of_isTorsionFree in TauCeti/Geometry/Manifold/VectorBundle/CovariantDerivative/Curvature/SecondCovariantDerivative.lean

LeanCovariantDerivative.secondCovariantDerivative_sub_swap_of_isTorsionFree · CovariantDerivative.secondCovariantDerivative_sub_swap · TauCeti.Manifold.mvfderiv_hessian_sub_swap

Uses 1 · Used by 2

Proof usesThe Koszul formula

Used byThe contracted Ricci identity for the gradient · Weyl–Schouten in dimension three, on a model space

TheoremRiemann's removable singularity theorem on complex curves#

A map between complex curves that is continuous at x and holomorphic at every point of a punctured neighbourhood of x is holomorphic at x. This is Mathlib's Complex.differentiableOn_compl_singleton_and_continuousAt_iff read in charts.

TauCeti.mdifferentiableAt_of_continuousAt_of_eventually_nhdsNE.{u_1, u_2} {X : Type u_1}
  {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y]
  {f : X → Y} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X]
  [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] (hc : ContinuousAt f x)
  (hf : ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, MDiffAt f y) : MDiffAt f x

Lean

Formalized in Tau Ceti as TauCeti.mdifferentiableAt_of_continuousAt_of_eventually_nhdsNE.

Sources

• Tau Ceti documentation: TauCeti.mdifferentiableAt_of_continuousAt_of_eventually_nhdsNE
• Source of TauCeti.mdifferentiableAt_of_continuousAt_of_eventually_nhdsNE in TauCeti/Geometry/Manifold/Complex/Chart.lean

LeanTauCeti.mdifferentiableAt_of_continuousAt_of_eventually_nhdsNE

Used by 2

Used byAnalytic Belyi pairs are classified by finite covers of the thrice-punctured sphere · The superelliptic curve is the analytic Belyi pair of the torus triple

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.