Robbin–Salamon Corrigendum… to Weierstrass preparation theorem…

TheoremRobbin–Salamon Corrigendum Lemma B (on arbitrary real normed spaces under C² regularity)#

if i² = -1, j(q)² = -1, α(q)(i a) + j(q)(α(q) a) = 0, mixedTerm i α j q = 0, and verticalTerm j q = 0 on a neighborhood of p, then the fibre vector field y ↦ horizontalTerm i α j (p.1, y) a b has vanishing endomorphism Lie derivative on j(p.1, ·) at p.2.

TauCeti.ComplexStructureFamily.lieDerivEndomorphism_horizontalTerm_eq_zero.{u_1, u_2} {B : Type u_1}
  {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V]
  {i : B →L[ℝ] B} (hi : ∀ (a : B), i (i a) = -a) {α : B × V → B →L[ℝ] V} {j : B × V → V →L[ℝ] V}
  {p : B × V} (hα : ContDiffAt ℝ 2 α p) (hj : ContDiffAt ℝ 2 j p)
  (hj_sq : ∀ᶠ (q : B × V) in nhds p, ∀ (v : V), (j q) ((j q) v) = -v)
  (hαj : ∀ᶠ (q : B × V) in nhds p, ∀ (a : B), (α q) (i a) + (j q) ((α q) a) = 0)
  (hmix :
    ∀ᶠ (q : B × V) in nhds p,
      ∀ (a : B) (v : V), TauCeti.ComplexStructureFamily.mixedTerm i α j q a v = 0)
  (hvert :
    ∀ᶠ (q : B × V) in nhds p, ∀ (v w : V), TauCeti.ComplexStructureFamily.verticalTerm j q v w = 0)
  (a b : B) :
  TauCeti.lieDerivEndomorphism
      (fun y => TauCeti.ComplexStructureFamily.horizontalTerm i α j (p.1, y) a b)
      (fun y => j (p.1, y)) p.2 =
    0

Lean

Formalized in Tau Ceti as TauCeti.ComplexStructureFamily.lieDerivEndomorphism_horizontalTerm_eq_zero.

Sources

• Tau Ceti documentation: TauCeti.ComplexStructureFamily.lieDerivEndomorphism_horizontalTerm_eq_zero
• Source of TauCeti.ComplexStructureFamily.lieDerivEndomorphism_horizontalTerm_eq_zero in TauCeti/Geometry/Manifold/Complex/Family/Integrability.lean

LeanTauCeti.ComplexStructureFamily.lieDerivEndomorphism_horizontalTerm_eq_zero

Uses 1

Proof usesNijenhuis–Lie-derivative identity

TheoremSard's theorem for smooth maps#

The critical values of a smooth map from a boundaryless Lindelöf manifold with finite-dimensional model to a manifold with finite-dimensional model form a null set. The dimensions may differ.

ContMDiff.isNullSet_image_criticalPoints.{u_1, u_2, u_3, u_4, u_5, u_6} {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] [LindelofSpace M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E']
  [FiniteDimensional ℝ E'] [MeasurableSpace E'] [BorelSpace E'] {H' : Type u_5}
  [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N]
  [ChartedSpace H' N] {f : M → N} [I.Boundaryless] {n : WithTop ℕ∞} [IsManifold I n M]
  [IsManifold J n N] (hf : ContMDiff I J n f) (hn : ↑⊤ ≤ n) :
  TauCeti.IsNullSet J (f '' {x | ¬TauCeti.IsRegularPoint I J f x})

Lean

Formalized in Tau Ceti as ContMDiff.isNullSet_image_criticalPoints.

Other forms

Sard's theorem at the sharp regularity, in codimension at most two. Formalized in Tau Ceti as ContMDiff.isNullSet_image_criticalPoints_of_finrank_le_add_two.

ContMDiff.isNullSet_image_criticalPoints_of_finrank_le_add_two.{u_1, u_2, u_3, u_4, u_5, u_6}
  {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] [LindelofSpace M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E']
  [FiniteDimensional ℝ E'] [MeasurableSpace E'] [BorelSpace E'] {H' : Type u_5}
  [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N]
  [ChartedSpace H' N] {f : M → N} [I.Boundaryless] {n : WithTop ℕ∞} [IsManifold I n M]
  [IsManifold J n N] (hf : ContMDiff I J n f)
  (hcodim : Module.finrank ℝ E ≤ Module.finrank ℝ E' + 2)
  (hk : ↑(Module.finrank ℝ E - Module.finrank ℝ E' + 1) ≤ n) :
  TauCeti.IsNullSet J (f '' {x | ¬TauCeti.IsRegularPoint I J f x})

Sard's theorem at the sharp regularity, in codimension at most two. Formalized in Tau Ceti as TauCeti.isNullSet_image_of_not_isRegularPoint_of_finrank_le_add_two.

TauCeti.isNullSet_image_of_not_isRegularPoint_of_finrank_le_add_two.{u_1, u_2, u_3, u_4, u_5, u_6}
  {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] [LindelofSpace M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E']
  [FiniteDimensional ℝ E'] [MeasurableSpace E'] [BorelSpace E'] {H' : Type u_5}
  [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N]
  [ChartedSpace H' N] {f : M → N} {s : Set M} [I.Boundaryless] {n : WithTop ℕ∞} [IsManifold I n M]
  [IsManifold J n N] (hcodim : Module.finrank ℝ E ≤ Module.finrank ℝ E' + 2)
  (hk : ↑(Module.finrank ℝ E - Module.finrank ℝ E' + 1) ≤ n) (hf : ∀ x ∈ s, ContMDiffAt I J n f x)
  (hs : ∀ x ∈ s, ¬TauCeti.IsRegularPoint I J f x) : TauCeti.IsNullSet J (f '' s)

Sard's theorem in arbitrary dimensions. Formalized in Tau Ceti as TauCeti.isNullSet_image_of_not_isRegularPoint_of_contMDiffAt.

TauCeti.isNullSet_image_of_not_isRegularPoint_of_contMDiffAt.{u_1, u_2, u_3, u_4, u_5, u_6}
  {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] [LindelofSpace M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E']
  [FiniteDimensional ℝ E'] [MeasurableSpace E'] [BorelSpace E'] {H' : Type u_5}
  [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N]
  [ChartedSpace H' N] {f : M → N} {s : Set M} [I.Boundaryless] {n : WithTop ℕ∞} [IsManifold I n M]
  [IsManifold J n N] (hk : ↑(Module.finrank ℝ E * Module.finrank ℝ E + 1) ≤ n)
  (hf : ∀ x ∈ s, ContMDiffAt I J n f x) (hs : ∀ x ∈ s, ¬TauCeti.IsRegularPoint I J f x) :
  TauCeti.IsNullSet J (f '' s)

Sard's theorem in equal dimensions. Formalized in Tau Ceti as TauCeti.isNullSet_image_criticalPoints.

TauCeti.isNullSet_image_criticalPoints.{u_1, u_2, u_3, u_4, u_5, u_6} {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] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E']
  [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'}
  {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J 1 N] {f : M → N}
  [LindelofSpace M] [MeasurableSpace E'] [BorelSpace E']
  (hdim : Module.finrank ℝ E = Module.finrank ℝ E') (hf : MDiff f) :
  TauCeti.IsNullSet J (f '' {x | ¬TauCeti.IsRegularPoint I J f x})

Sard's theorem in equal dimensions, for a set of non-regular points. Formalized in Tau Ceti as TauCeti.isNullSet_image_of_not_isRegularPoint.

TauCeti.isNullSet_image_of_not_isRegularPoint.{u_1, u_2, u_3, u_4, u_5, u_6} {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] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E']
  [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'}
  {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J 1 N] {f : M → N} {s : Set M}
  [LindelofSpace M] [MeasurableSpace E'] [BorelSpace E']
  (hdim : Module.finrank ℝ E = Module.finrank ℝ E') (hf : ∀ x ∈ s, MDiffAt f x)
  (hs : ∀ x ∈ s, ¬TauCeti.IsRegularPoint I J f x) : TauCeti.IsNullSet J (f '' s)

Sard's theorem when the source has smaller dimension. Formalized in Tau Ceti as TauCeti.isNullSet_image_of_finrank_lt_finrank.

TauCeti.isNullSet_image_of_finrank_lt_finrank.{u_1, u_2, u_3, u_4, u_5, u_6} {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] [LindelofSpace M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E']
  [FiniteDimensional ℝ E'] [MeasurableSpace E'] [BorelSpace E'] {H' : Type u_5}
  [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N]
  [ChartedSpace H' N] {f : M → N} {s : Set M} [IsManifold I 1 M] [IsManifold J 1 N]
  (hdim : Module.finrank ℝ E < Module.finrank ℝ E') (hf : ∀ x ∈ s, MDiffAt f x) :
  TauCeti.IsNullSet J (f '' s)

Sard's theorem, in Baire category form. Formalized in Tau Ceti as TauCeti.isMeagre_image_of_not_isRegularPoint.

TauCeti.isMeagre_image_of_not_isRegularPoint.{u_1, u_2, u_3, u_4, u_5, u_6} {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 (↑⊤) M] {E' : Type u_4}
  [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5}
  [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} [J.Boundaryless] {N : Type u_6}
  [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J (↑⊤) N] {f : M → N} {s : Set M}
  [LindelofSpace ↑s] (hf : ∀ x ∈ s, ContMDiffAt I J (↑⊤) f x)
  (hs : ∀ x ∈ s, ¬TauCeti.IsRegularPoint I J f x) : IsMeagre (f '' s)

Sources

• Tau Ceti documentation: ContMDiff.isNullSet_image_criticalPoints
• Source of ContMDiff.isNullSet_image_criticalPoints in TauCeti/Geometry/Manifold/Sard/Basic.lean

LeanContMDiff.isNullSet_image_criticalPoints · ContMDiff.isNullSet_image_criticalPoints_of_finrank_le_add_two · TauCeti.isNullSet_image_of_not_isRegularPoint_of_finrank_le_add_two · TauCeti.isNullSet_image_of_not_isRegularPoint_of_contMDiffAt · TauCeti.isNullSet_image_criticalPoints · TauCeti.isNullSet_image_of_not_isRegularPoint · TauCeti.isNullSet_image_of_finrank_lt_finrank · TauCeti.isMeagre_image_of_not_isRegularPoint

Uses 3

Proof usesThe Morse--Sard theorem · Sard's lemma on the flat stratum · The Sard--Smale theorem

TheoremSchur's theorem (CovariantDerivative.eq_of_forall_hasSectionalCurvatureAt)#

Let a metric-compatible torsion-free connection on a preconnected manifold of dimension at least three have, at every point x, the same sectional curvature κ x on all tangent two-planes at x. Then κ is constant.

CovariantDerivative.eq_of_forall_hasSectionalCurvatureAt.{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]
  {cov : CovariantDerivative I E fun x => TangentSpace I x} [cov.ContMDiffCovariantDerivative ↑⊤]
  [PreconnectedSpace M] (hcov : cov.IsMetricCompatible) (ht : cov.torsion = 0)
  (hdim : 3 ≤ Module.finrank ℝ E) {κ : M → ℝ}
  (hκ : ∀ (x : M), cov.HasSectionalCurvatureAt hcov x (κ x)) (x y : M) : κ x = κ y

Lean

Formalized in Tau Ceti as CovariantDerivative.eq_of_forall_hasSectionalCurvatureAt.

Other forms

Schur's theorem, global form. Formalized in Tau Ceti as CovariantDerivative.hasConstantSectionalCurvature_of_forall_hasSectionalCurvatureAt.

CovariantDerivative.hasConstantSectionalCurvature_of_forall_hasSectionalCurvatureAt.{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]
  {cov : CovariantDerivative I E fun x => TangentSpace I x} [cov.ContMDiffCovariantDerivative ↑⊤]
  [PreconnectedSpace M] (hcov : cov.IsMetricCompatible) (ht : cov.torsion = 0)
  (hdim : 3 ≤ Module.finrank ℝ E) {κ : M → ℝ}
  (hκ : ∀ (x : M), cov.HasSectionalCurvatureAt hcov x (κ x)) (x₀ : M) :
  cov.HasConstantSectionalCurvature hcov (κ x₀)

Schur's theorem, local form. Formalized in Tau Ceti as CovariantDerivative.mfderiv_eq_zero_of_curvatureTensor_eq_smul_inner_sub.

CovariantDerivative.mfderiv_eq_zero_of_curvatureTensor_eq_smul_inner_sub.{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]
  {cov : CovariantDerivative I E fun x => TangentSpace I x} [cov.ContMDiffCovariantDerivative ↑⊤]
  (hcov : cov.IsMetricCompatible) (ht : cov.torsion = 0) (hdim : 3 ≤ Module.finrank ℝ E) {κ : M → ℝ}
  {x : M}
  (hκ :
    ∀ᶠ (y : M) in nhds x,
      ∀ (w u v : TangentSpace I y),
        (((cov.curvatureTensor y) w) u) v = κ y • (inner ℝ u v • w - inner ℝ w v • u)) :
  mfderiv% κ x = 0

Sources

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

LeanCovariantDerivative.eq_of_forall_hasSectionalCurvatureAt · CovariantDerivative.hasConstantSectionalCurvature_of_forall_hasSectionalCurvatureAt · CovariantDerivative.mfderiv_eq_zero_of_curvatureTensor_eq_smul_inner_sub

Uses 2

Proof usesCovariantDerivative.IsMetricCompatible.riemannCurvatureTensor_eq_of_forall_linearIndependent · The second Bianchi identity

TheoremSharp local Lipschitz bound for the extended chart#

For r > 1, near x every continuous linear map ℓ from T_x M to a real normed space, read in the extended chart at x, is (r ‖ℓ‖)-Lipschitz at x for the Riemannian distance.

TauCeti.Manifold.eventually_enorm_apply_extChartAt_sub_le.{u_1, u_2, u_3, u_4} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F]
  {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4}
  [PseudoEMetricSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun x => TangentSpace I x]
  [IsManifold I 1 M] [IsRiemannianManifold I M]
  [IsContinuousRiemannianBundle E fun x => TangentSpace I x] (x : M) {r : ℝ} (hr : 1 < r) :
  ∀ᶠ (y : M) in nhds x,
    ∀ (ℓ : TangentSpace I x →L[ℝ] F),
      ‖ℓ (↑(extChartAt I x) y - ↑(extChartAt I x) x)‖ₑ ≤ ENNReal.ofReal r * ‖ℓ‖ₑ * edist x y

Lean

Formalized in Tau Ceti as TauCeti.Manifold.eventually_enorm_apply_extChartAt_sub_le.

Sources

• Tau Ceti documentation: TauCeti.Manifold.eventually_enorm_apply_extChartAt_sub_le
• Source of TauCeti.Manifold.eventually_enorm_apply_extChartAt_sub_le in TauCeti/Geometry/Manifold/Riemannian/MetricBridge.lean

LeanTauCeti.Manifold.eventually_enorm_apply_extChartAt_sub_le

TheoremSmooth Euclidean tubular neighbourhood theorem#

The whole orthogonal normal bundle of a smooth immersion inducing the source topology is diffeomorphic to an open neighbourhood of its image, inside any prescribed open neighbourhood. The identification fixes the core. Neither compactness nor closedness of the image is required.

TauCeti.exists_diffeomorph_wholeNormalBundle_subset.{u_1, u_2, u_3, u_4, u_5} {V : Type u_1}
  {E : Type u_2} {F : Type u_3} {H : Type u_4} {M : Type u_5} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E]
  [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F]
  [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M]
  [ChartedSpace H M] [IsManifold I (↑⊤) M] {f : M → V}
  (hf : ContMDiff I (modelWithCornersSelf ℝ V) (↑⊤) f)
  (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (hind : Topology.IsInducing f)
  (hdim : Module.finrank ℝ F = Module.finrank ℝ V - Module.finrank ℝ E) {O : Set V} (hO : IsOpen O)
  (hfO : Set.range f ⊆ O) :
  ∃ W,
    ↑W ⊆ O ∧
      ∃ Φ, ∀ (x : M), ↑(Φ (Bundle.zeroSection F (fun x => ↥(TauCeti.normalSubspace I f x)) x)) = f x

Lean

Formalized in Tau Ceti as TauCeti.exists_diffeomorph_wholeNormalBundle_subset.

Sources

• Tau Ceti documentation: TauCeti.exists_diffeomorph_wholeNormalBundle_subset
• Source of TauCeti.exists_diffeomorph_wholeNormalBundle_subset in TauCeti/Geometry/Manifold/TubularNeighborhood/WholeBundle/Diffeomorph.lean

LeanTauCeti.exists_diffeomorph_wholeNormalBundle_subset

Uses 3

Proof usesThe inverse function theorem for manifolds · The inverse function theorem, with a C^n inverse on the whole target · Noncompact Euclidean tubular neighbourhood theorem

TheoremSmooth Riemannian tubular neighbourhood theorem#

The entire intrinsic normal bundle of a smooth embedding is diffeomorphic to an open neighbourhood inside any prescribed open neighbourhood of its image. The zero section is sent to the original embedding. Neither compactness nor closedness of the embedded image nor completeness of the ambient metric is required.

TauCeti.SmoothEmbedding.exists_diffeomorph_normalBundle_riemannian_subset.{u_1, u_2, u_3, u_4, u_5,
    u_6, u_7}
  {E : Type u_1} {V : Type u_2} {P : Type u_3} {H : Type u_4} {G : Type u_5} {M : Type u_6}
  {N : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup P]
  [NormedSpace ℝ P] [FiniteDimensional ℝ P] [TopologicalSpace H] [TopologicalSpace G]
  {I : ModelWithCorners ℝ E H} {J : ModelWithCorners ℝ V G} [TopologicalSpace M] [ChartedSpace H M]
  [TopologicalSpace N] [ChartedSpace G N] [IsManifold J (↑⊤) N] [I.Boundaryless] [J.Boundaryless]
  [T2Space N] [Bundle.RiemannianBundle fun y => TangentSpace J y]
  [IsContMDiffRiemannianBundle J (↑⊤) V fun y => TangentSpace J y] [IsManifold I (↑⊤) M]
  [SecondCountableTopology N] (f : TauCeti.SmoothEmbedding I J (↑⊤) M N)
  (hdim : Module.finrank ℝ P = Module.finrank ℝ V - Module.finrank ℝ E) {O : Set N} (hO : IsOpen O)
  (hfO : Set.range ⇑f ⊆ O) :
  have hn := TauCeti.SmoothEmbedding.exists_diffeomorph_normalBundle_riemannian_subset._proof_1;
  ∃ W, ↑W ⊆ O ∧ ∃ Φ, ∀ (x : M), ↑(Φ (Bundle.zeroSection P (fun x => f.NormalSpace x hn) x)) = f x

Lean

Formalized in Tau Ceti as TauCeti.SmoothEmbedding.exists_diffeomorph_normalBundle_riemannian_subset.

Sources

• Tau Ceti documentation: TauCeti.SmoothEmbedding.exists_diffeomorph_normalBundle_riemannian_subset
• Source of TauCeti.SmoothEmbedding.exists_diffeomorph_normalBundle_riemannian_subset in TauCeti/Geometry/Manifold/TubularNeighborhood/Riemannian/Coordinates.lean

LeanTauCeti.SmoothEmbedding.exists_diffeomorph_normalBundle_riemannian_subset

Uses 4 · Used by 1

Proof usesThe inverse function theorem for manifolds · The Koszul formula · TauCeti.CotangentBundle · TauCeti.Manifold.riemannianExp

Used bySmooth tubular neighbourhood theorem

TheoremSmooth tubular neighbourhood theorem#

The entire intrinsic normal bundle of a smooth embedding is diffeomorphic to an arbitrarily small open neighbourhood of its image, with the zero section sent to the embedding. No Riemannian metric is part of the input or output, and the image need not be closed or compact.

TauCeti.SmoothEmbedding.exists_diffeomorph_normalBundle_subset.{u_1, u_2, u_3, u_4, u_5, u_6, u_7}
  {E : Type u_1} {V : Type u_2} {P : Type u_3} {H : Type u_4} {G : Type u_5} {M : Type u_6}
  {N : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup P]
  [NormedSpace ℝ P] [FiniteDimensional ℝ P] [TopologicalSpace H] [TopologicalSpace G]
  {I : ModelWithCorners ℝ E H} {J : ModelWithCorners ℝ V G} [I.Boundaryless] [J.Boundaryless]
  [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [TopologicalSpace N]
  [ChartedSpace G N] [IsManifold J (↑⊤) N] [T2Space N] [SecondCountableTopology N]
  (f : TauCeti.SmoothEmbedding I J (↑⊤) M N)
  (hdim : Module.finrank ℝ P = Module.finrank ℝ V - Module.finrank ℝ E) {O : Set N} (hO : IsOpen O)
  (hfO : Set.range ⇑f ⊆ O) :
  have hn := TauCeti.SmoothEmbedding.exists_diffeomorph_normalBundle_subset._proof_1;
  ∃ W, ↑W ⊆ O ∧ ∃ Φ, ∀ (x : M), ↑(Φ (Bundle.zeroSection P (fun x => f.NormalSpace x hn) x)) = f x

Lean

Formalized in Tau Ceti as TauCeti.SmoothEmbedding.exists_diffeomorph_normalBundle_subset.

Sources

• Tau Ceti documentation: TauCeti.SmoothEmbedding.exists_diffeomorph_normalBundle_subset
• Source of TauCeti.SmoothEmbedding.exists_diffeomorph_normalBundle_subset in TauCeti/Geometry/Manifold/TubularNeighborhood/Existence.lean

LeanTauCeti.SmoothEmbedding.exists_diffeomorph_normalBundle_subset

Uses 1

Proof usesSmooth Riemannian tubular neighbourhood theorem

TheoremThe Sobolev inequality near a point#

Let 1 ≤ p and let p' be the Sobolev conjugate exponent, 1 / p' = 1 / p - 1 / n, on a manifold without boundary of dimension n > 0 with a continuous Riemannian metric. Every point c has a neighbourhood V with a constant C such that ‖u‖_{L^{p'}(V)} ≤ C (‖∇u‖_{Lᵖ} + ‖u‖_{Lᵖ}) for every C¹ function u.

TauCeti.Manifold.exists_mem_nhds_eLpNorm_restrict_le_mul_eLpNorm_mgradient_add.{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]
  [LindelofSpace M] {p p' : NNReal} (hp : 1 ≤ p) (hn : 0 < Module.finrank ℝ E)
  (hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑(Module.finrank ℝ E))⁻¹) (c : M) :
  ∃ V ∈ nhds c,
    ∃ C,
      ∀ (u : M → ℝ),
        ContMDiff I (modelWithCornersSelf ℝ ℝ) 1 u →
          MeasureTheory.eLpNorm u (↑p') ((TauCeti.riemannianVolume I M).restrict V) ≤
            ↑C *
              (MeasureTheory.eLpNorm (fun x => ‖TauCeti.Manifold.mgradient I u x‖) (↑p)
                  (TauCeti.riemannianVolume I M) +
                MeasureTheory.eLpNorm u (↑p) (TauCeti.riemannianVolume I M))

Lean

Formalized in Tau Ceti as TauCeti.Manifold.exists_mem_nhds_eLpNorm_restrict_le_mul_eLpNorm_mgradient_add.

Other forms

The Sobolev inequality for H¹ on a closed Riemannian manifold. Formalized in Tau Ceti as TauCeti.Manifold.exists_eLpNorm_le_mul_eLpNorm_mgradient_two_add.

TauCeti.Manifold.exists_eLpNorm_le_mul_eLpNorm_mgradient_two_add.{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] (hn : 2 < Module.finrank ℝ E) :
  ∃ C,
    ∀ (u : M → ℝ),
      ContMDiff I (modelWithCornersSelf ℝ ℝ) 1 u →
        MeasureTheory.eLpNorm u
            (ENNReal.ofReal (2 * ↑(Module.finrank ℝ E) / (↑(Module.finrank ℝ E) - 2)))
            (TauCeti.riemannianVolume I M) ≤
          ↑C *
            (MeasureTheory.eLpNorm (fun x => ‖TauCeti.Manifold.mgradient I u x‖) 2
                (TauCeti.riemannianVolume I M) +
              MeasureTheory.eLpNorm u 2 (TauCeti.riemannianVolume I M))

The Sobolev inequality on a closed Riemannian manifold. Formalized in Tau Ceti as TauCeti.Manifold.exists_eLpNorm_le_mul_eLpNorm_mgradient_add.

TauCeti.Manifold.exists_eLpNorm_le_mul_eLpNorm_mgradient_add.{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] {p p' : NNReal} (hp : 1 ≤ p) (hn : 0 < Module.finrank ℝ E)
  (hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑(Module.finrank ℝ E))⁻¹) :
  ∃ C,
    ∀ (u : M → ℝ),
      ContMDiff I (modelWithCornersSelf ℝ ℝ) 1 u →
        MeasureTheory.eLpNorm u (↑p') (TauCeti.riemannianVolume I M) ≤
          ↑C *
            (MeasureTheory.eLpNorm (fun x => ‖TauCeti.Manifold.mgradient I u x‖) (↑p)
                (TauCeti.riemannianVolume I M) +
              MeasureTheory.eLpNorm u (↑p) (TauCeti.riemannianVolume I M))

Sources

• Tau Ceti documentation: TauCeti.Manifold.exists_mem_nhds_eLpNorm_restrict_le_mul_eLpNorm_mgradient_add
• Source of TauCeti.Manifold.exists_mem_nhds_eLpNorm_restrict_le_mul_eLpNorm_mgradient_add in TauCeti/Geometry/Manifold/Riemannian/Sobolev.lean

LeanTauCeti.Manifold.exists_mem_nhds_eLpNorm_restrict_le_mul_eLpNorm_mgradient_add · TauCeti.Manifold.exists_eLpNorm_le_mul_eLpNorm_mgradient_two_add · TauCeti.Manifold.exists_eLpNorm_le_mul_eLpNorm_mgradient_add

TheoremThe straightening theorem [Lee, Thm. 9.22]#

Let v be a vector field on a C^n manifold with finite-dimensional boundaryless model, C^m on a neighbourhood of x, with 1 ≤ m, m + 1 ≤ n and v x ≠ 0. Then some chart e of the C^m maximal atlas whose domain contains x carries v to a constant nonzero vector field: the differential of I ∘ e sends v y to the same vector u ≠ 0 at every point y of the domain of e.

TauCeti.exists_chart_mfderiv_eq_const.{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] {m : ℕ∞}
  {n : WithTop ℕ∞} (hm : 1 ≤ m) (hmn : ↑m + 1 ≤ n) [IsManifold I 1 M] [IsManifold I n M]
  {v : (y : M) → TangentSpace I y} {U : Set M} {x : M}
  (hv : ContMDiffOn I I.tangent (↑m) (fun y => ⟨y, v y⟩) U) (hU : U ∈ nhds x) (hx : v x ≠ 0) :
  ∃ e u,
    e ∈ IsManifold.maximalAtlas I (↑m) M ∧
      x ∈ e.source ∧ u ≠ 0 ∧ ∀ y ∈ e.source, (mfderiv% (↑I ∘ ↑e) y) (v y) = u

Lean

Formalized in Tau Ceti as TauCeti.exists_chart_mfderiv_eq_const.

Sources

• Tau Ceti documentation: TauCeti.exists_chart_mfderiv_eq_const
• Source of TauCeti.exists_chart_mfderiv_eq_const in TauCeti/Geometry/Manifold/Flow/Straightening.lean

LeanTauCeti.exists_chart_mfderiv_eq_const

Uses 1

Proof usesThe straightening theorem (flow-box theorem)

TheoremThe transverse fibre-product theorem#

The actual equal-value subtype of two transverse C^n maps, n ≥ 1, is a C^n manifold of dimension dim X + dim Y - dim N with its subspace topology. Its inclusion is a smooth embedding, and its tangent image consists of pairs whose images under the two differentials agree. Empty fibre products are allowed; no separation or countability hypotheses are needed.

TauCeti.exists_isManifold_transverseFiberProduct_isSmoothEmbedding.{u_1, u_2, u_3, u_4, u_5, u_6,
    u_7, u_8, u_9}
  {EX : Type u_1} {HX : Type u_2} {X : Type u_3} {EY : Type u_4} {HY : Type u_5} {Y : Type u_6}
  {EN : Type u_7} {HN : Type u_8} {N : Type u_9} [NormedAddCommGroup EX] [NormedSpace ℝ EX]
  [TopologicalSpace HX] [NormedAddCommGroup EY] [NormedSpace ℝ EY] [TopologicalSpace HY]
  [NormedAddCommGroup EN] [NormedSpace ℝ EN] [TopologicalSpace HN] {IX : ModelWithCorners ℝ EX HX}
  {IY : ModelWithCorners ℝ EY HY} {IN : ModelWithCorners ℝ EN HN} [TopologicalSpace X]
  [ChartedSpace HX X] [TopologicalSpace Y] [ChartedSpace HY Y] [TopologicalSpace N]
  [ChartedSpace HN N] {n : WithTop ℕ∞} [IsManifold IN n N] {f : X → N} {g : Y → N}
  [IsManifold IX n X] [IsManifold IY n Y] [IX.Boundaryless] [IY.Boundaryless] [IN.Boundaryless]
  [FiniteDimensional ℝ EX] [FiniteDimensional ℝ EY] [FiniteDimensional ℝ EN] (hn : 1 ≤ n)
  (hf : ContMDiff IX IN n f) (hg : ContMDiff IY IN n g)
  (htrans :
    ∀ (p : X × Y),
      f p.1 = g p.2 →
        (↑(mfderiv% f p.1)).range ⊔
            (↑(↑(tangentSpaceCast IN (g p.2) (f p.1)) ∘SL mfderiv% g p.2)).range =
          ⊤) :
  ∃ cs,
    IsManifold
        (modelWithCornersSelf ℝ
          (Fin (Module.finrank ℝ EX + Module.finrank ℝ EY - Module.finrank ℝ EN) → ℝ))
        n { p // f p.1 = g p.2 } ∧
      Manifold.IsSmoothEmbedding
          (modelWithCornersSelf ℝ
            (Fin (Module.finrank ℝ EX + Module.finrank ℝ EY - Module.finrank ℝ EN) → ℝ))
          (IX.prod IY) n Subtype.val ∧
        ∀ (p : { p // f p.1 = g p.2 }) (v : TangentSpace (IX.prod IY) ↑p),
          v ∈ (↑(mfderiv% Subtype.val p)).range ↔
            (mfderiv% f (↑p).1) v.1 =
              (tangentSpaceCast IN (g (↑p).2) (f (↑p).1)) ((mfderiv% g (↑p).2) v.2)

Lean

Formalized in Tau Ceti as TauCeti.exists_isManifold_transverseFiberProduct_isSmoothEmbedding.

Sources

• Tau Ceti documentation: TauCeti.exists_isManifold_transverseFiberProduct_isSmoothEmbedding
• Source of TauCeti.exists_isManifold_transverseFiberProduct_isSmoothEmbedding in TauCeti/Geometry/Manifold/FiberProduct/Manifold.lean

LeanTauCeti.exists_isManifold_transverseFiberProduct_isSmoothEmbedding

Uses 2

Proof usesHomeomorph.pullbackChartedSpace · Homeomorph.pullbackDiffeomorph

TheoremTrudinger's inequality near a point#

Every point c of a manifold without boundary, of dimension n ≥ 2, with a continuous Riemannian metric, has a neighbourhood V with constants β > 0 and C such that ∫_V exp (β |u| ^ (n / (n - 1))) dV ≤ C for every C¹ function u with ‖∇u‖_{Lⁿ} + ‖u‖_{Lⁿ} ≤ 1.

TauCeti.Manifold.exists_mem_nhds_setLIntegral_exp_mul_abs_rpow_le.{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]
  [LindelofSpace M] (hn : 2 ≤ Module.finrank ℝ E) (c : M) :
  ∃ V ∈ nhds c,
    ∃ β > 0,
      ∃ C,
        ∀ (u : M → ℝ),
          ContMDiff I (modelWithCornersSelf ℝ ℝ) 1 u →
            MeasureTheory.eLpNorm (fun x => ‖TauCeti.Manifold.mgradient I u x‖)
                    (↑(Module.finrank ℝ E)) (TauCeti.riemannianVolume I M) +
                  MeasureTheory.eLpNorm u (↑(Module.finrank ℝ E)) (TauCeti.riemannianVolume I M) ≤
                1 →
              ∫⁻ (x : M) in V,
                  ENNReal.ofReal
                    (Real.exp
                      (β *
                        |u x| ^
                          (↑(Module.finrank ℝ E) /
                            (↑(Module.finrank ℝ E) - 1)))) ∂TauCeti.riemannianVolume I M ≤
                ↑C

Lean

Formalized in Tau Ceti as TauCeti.Manifold.exists_mem_nhds_setLIntegral_exp_mul_abs_rpow_le.

Other forms

Trudinger's inequality on a closed Riemannian manifold. Formalized in Tau Ceti as TauCeti.Manifold.exists_lintegral_exp_mul_abs_rpow_le.

TauCeti.Manifold.exists_lintegral_exp_mul_abs_rpow_le.{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] (hn : 2 ≤ Module.finrank ℝ E) :
  ∃ β > 0,
    ∃ C,
      ∀ (u : M → ℝ),
        ContMDiff I (modelWithCornersSelf ℝ ℝ) 1 u →
          MeasureTheory.eLpNorm (fun x => ‖TauCeti.Manifold.mgradient I u x‖)
                  (↑(Module.finrank ℝ E)) (TauCeti.riemannianVolume I M) +
                MeasureTheory.eLpNorm u (↑(Module.finrank ℝ E)) (TauCeti.riemannianVolume I M) ≤
              1 →
            ∫⁻ (x : M),
                ENNReal.ofReal
                  (Real.exp
                    (β *
                      |u x| ^
                        (↑(Module.finrank ℝ E) /
                          (↑(Module.finrank ℝ E) - 1)))) ∂TauCeti.riemannianVolume I M ≤
              ↑C

Sources

• Tau Ceti documentation: TauCeti.Manifold.exists_mem_nhds_setLIntegral_exp_mul_abs_rpow_le
• Source of TauCeti.Manifold.exists_mem_nhds_setLIntegral_exp_mul_abs_rpow_le in TauCeti/Geometry/Manifold/Riemannian/Trudinger.lean

LeanTauCeti.Manifold.exists_mem_nhds_setLIntegral_exp_mul_abs_rpow_le · TauCeti.Manifold.exists_lintegral_exp_mul_abs_rpow_le

Uses 1

Proof usesTrudinger's inequality on W^{1,n}_0(Ω)

TheoremTubular neighbourhood theorem#

Tubular neighbourhood theorem for a compact C² embedded submanifold of a Euclidean space: for some ε > 0, the map (x, v) ↦ f x + v is an open embedding of the normal vectors of length less than ε into V.

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

Lean

Formalized in Tau Ceti as TauCeti.exists_isOpenEmbedding_normalTube.

Other forms

Tubular neighbourhood theorem. Formalized in Tau Ceti as TauCeti.exists_isTubularNeighborhood_normalBundle.

TauCeti.exists_isTubularNeighborhood_normalBundle.{u_1, u_2, u_3, u_4} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {E : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_3}
  [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M]
  [ChartedSpace H M] [I.Boundaryless] [IsManifold I 2 M] [CompactSpace M] {f : M → V}
  (hf : ContMDiff I (modelWithCornersSelf ℝ V) 2 f)
  (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (hinj : Function.Injective f) :
  ∃ ε > 0, TauCeti.IsTubularNeighborhood f {p | ‖↑p.snd‖ < ε} fun p => f (↑p).proj + ↑(↑p).snd

Sources

• Tau Ceti documentation: TauCeti.exists_isOpenEmbedding_normalTube
• Source of TauCeti.exists_isOpenEmbedding_normalTube in TauCeti/Geometry/Manifold/TubularNeighborhood/Euclidean.lean

LeanTauCeti.exists_isOpenEmbedding_normalTube · TauCeti.exists_isTubularNeighborhood_normalBundle

Uses 1

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

TheoremWeierstrass division theorem in holomorphic stalks#

Given germs f and g at (x₀, w₀) such that the vertical power series of f has nonzero image in (𝒪_{E, x₀} ⧸ 𝔪_{x₀})⟦X⟧, there exist unique q ∈ 𝒪_{E × ℂ, (x₀, w₀)} and r ∈ (𝒪_{E, x₀})[X] forming a Weierstrass division of g by f.

TauCeti.holomorphicStructureSheaf.existsUnique_weierstrassDivision {E : Type} [NormedAddCommGroup E]
  [NormedSpace ℂ E] [FiniteDimensional ℂ E] {x₀ : E} {w₀ : ℂ}
  {f :
    ↑((TauCeti.holomorphicStructureSheaf (modelWithCornersSelf ℂ (E × ℂ)) (E × ℂ)).presheaf.stalk
        (x₀, w₀))}
  (hf :
    (PowerSeries.map
          (IsLocalRing.residue
            ↑((TauCeti.holomorphicStructureSheaf (modelWithCornersSelf ℂ E) E).presheaf.stalk x₀)))
        ((TauCeti.holomorphicStructureSheaf.verticalPowerSeries x₀ w₀) f) ≠
      0)
  (g :
    ↑((TauCeti.holomorphicStructureSheaf (modelWithCornersSelf ℂ (E × ℂ)) (E × ℂ)).presheaf.stalk
        (x₀, w₀))) :
  ∃! qr,
    ((TauCeti.holomorphicStructureSheaf.verticalPowerSeries x₀ w₀) g).IsWeierstrassDivision
      ((TauCeti.holomorphicStructureSheaf.verticalPowerSeries x₀ w₀) f)
      ((TauCeti.holomorphicStructureSheaf.verticalPowerSeries x₀ w₀) qr.1) qr.2

Lean

Formalized in Tau Ceti as TauCeti.holomorphicStructureSheaf.existsUnique_weierstrassDivision.

Sources

• Tau Ceti documentation: TauCeti.holomorphicStructureSheaf.existsUnique_weierstrassDivision
• Source of TauCeti.holomorphicStructureSheaf.existsUnique_weierstrassDivision in TauCeti/Geometry/Manifold/Complex/StructureSheaf/Weierstrass.lean

LeanTauCeti.holomorphicStructureSheaf.existsUnique_weierstrassDivision

Uses 2

Proof usesOsgood's lemma · Weierstrass preparation theorem in holomorphic stalks

TheoremWeierstrass preparation theorem in holomorphic stalks#

Every holomorphic germ f at (x₀, w₀) whose vertical power series has nonzero image in (𝒪_{E, x₀} ⧸ 𝔪_{x₀})⟦X⟧ admits a unique factorization f = evalVertical x₀ w₀ P * u into a distinguished polynomial P over 𝒪_{E, x₀} and a unit germ u at (x₀, w₀).

TauCeti.holomorphicStructureSheaf.existsUnique_weierstrassPreparation {E : Type}
  [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {x₀ : E} {w₀ : ℂ}
  {f :
    ↑((TauCeti.holomorphicStructureSheaf (modelWithCornersSelf ℂ (E × ℂ)) (E × ℂ)).presheaf.stalk
        (x₀, w₀))}
  (hf :
    (PowerSeries.map
          (IsLocalRing.residue
            ↑((TauCeti.holomorphicStructureSheaf (modelWithCornersSelf ℂ E) E).presheaf.stalk x₀)))
        ((TauCeti.holomorphicStructureSheaf.verticalPowerSeries x₀ w₀) f) ≠
      0) :
  ∃! pu,
    pu.1.IsDistinguishedAt
        (IsLocalRing.maximalIdeal
          ↑((TauCeti.holomorphicStructureSheaf (modelWithCornersSelf ℂ E) E).presheaf.stalk x₀)) ∧
      IsUnit pu.2 ∧ f = (TauCeti.holomorphicStructureSheaf.evalVertical x₀ w₀) pu.1 * pu.2

Lean

Formalized in Tau Ceti as TauCeti.holomorphicStructureSheaf.existsUnique_weierstrassPreparation.

Sources

• Tau Ceti documentation: TauCeti.holomorphicStructureSheaf.existsUnique_weierstrassPreparation
• Source of TauCeti.holomorphicStructureSheaf.existsUnique_weierstrassPreparation in TauCeti/Geometry/Manifold/Complex/StructureSheaf/Weierstrass.lean

LeanTauCeti.holomorphicStructureSheaf.existsUnique_weierstrassPreparation

Uses 1 · Used by 1

Proof usesComplex analytic Weierstrass preparation theorem

Used byWeierstrass division theorem in holomorphic stalks

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.