Other results

Results named in the rest of Tau Ceti's TauCeti.Geometry modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremCartan's formula for a contact Hamiltonian vector field#

a differentiable contact Hamiltonian vector field X of f satisfies L_X α = (R_α f) α.

TauCeti.SmoothForm.IsContactHamiltonianVectorField.mlieDerivForm_eq.{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] [IsManifold I (↑⊤) M]
  {α : TauCeti.SmoothForm I M ℝ 1} {f : M → ℝ} {X : (x : M) → TangentSpace I x}
  (hX : α.IsContactHamiltonianVectorField f X) (hXd : MDiff fun y => ⟨y, X y⟩) :
  TauCeti.mlieDerivForm X ↑α = fun x => (d% f x) (α.reebVectorField x) • ↑α x
Lean

Formalized in Tau Ceti as TauCeti.SmoothForm.IsContactHamiltonianVectorField.mlieDerivForm_eq.

Other forms

Cartan's formula for a contact Hamiltonian vector field at a point where it is differentiable. Formalized in Tau Ceti as TauCeti.SmoothForm.IsContactHamiltonianVectorField.mlieDerivForm_apply_eq.

TauCeti.SmoothForm.IsContactHamiltonianVectorField.mlieDerivForm_apply_eq.{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]
  [IsManifold I (↑⊤) M] {α : TauCeti.SmoothForm I M ℝ 1} {f : M → ℝ}
  {X : (x : M) → TangentSpace I x} (hX : α.IsContactHamiltonianVectorField f X) {x : M}
  (hXd : (MDiffAt fun y => ⟨y, X y⟩) x) :
  TauCeti.mlieDerivForm X (↑α) x = (d% f x) (α.reebVectorField x) • ↑α x
Sources
LeanTauCeti.SmoothForm.IsContactHamiltonianVectorField.mlieDerivForm_eq · TauCeti.SmoothForm.IsContactHamiltonianVectorField.mlieDerivForm_apply_eq
Uses 1 · Used by 1
Proof usesCartan's magic formula
Used byThe Jacobi identity for the Jacobi bracket

TheoremCerf's theorem as a count of path components#

Cerf's theorem holds exactly when the diffeomorphism group of S³ has two path components.

TauCeti.cerfTheorem_iff_natCard_zerothHomotopy_eq_two :
  TauCeti.CerfTheorem ↔
    Nat.card
        (ZerothHomotopy
          (TauCeti.Diff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 3))) ↑(Metric.sphere 0 1)
            ↑⊤)) =
      2
Lean

Formalized in Tau Ceti as TauCeti.cerfTheorem_iff_natCard_zerothHomotopy_eq_two.

Sources
LeanTauCeti.cerfTheorem_iff_natCard_zerothHomotopy_eq_two
Uses 1
Proof usesThe Mayer–Vietoris isomorphism of a sphere

TheoremThe density theorem for rectifiable sets#

A countably k-rectifiable subset E of a finite-dimensional real inner product space, measurable for μHE[k] and with locally finite μHE[k] measure, has k-dimensional density one at μHE[k]-almost every point of E: μHE[k] (E ∩ closedBall x r) / (ω_k r ^ k) → 1 as r → 0⁺, where ω_k r ^ k is the volume of a ball of radius r in EuclideanSpace ℝ (Fin k).

TauCeti.CountablyRectifiable.ae_tendsto_euclideanHausdorffMeasure_inter_closedBall_div.{u_1}
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V] {k : ℕ} {E : Set V} (hE : TauCeti.CountablyRectifiable k E)
  (hEm : MeasureTheory.NullMeasurableSet E (MeasureTheory.Measure.euclideanHausdorffMeasure k))
  [MeasureTheory.IsLocallyFiniteMeasure
      ((MeasureTheory.Measure.euclideanHausdorffMeasure k).restrict E)] :
  ∀ᵐ (x : V) ∂MeasureTheory.Measure.euclideanHausdorffMeasure k,
    x ∈ E →
      Filter.Tendsto
        (fun r =>
          (MeasureTheory.Measure.euclideanHausdorffMeasure k) (E ∩ Metric.closedBall x r) /
            MeasureTheory.volume (Metric.closedBall 0 r))
        (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)
Lean

Formalized in Tau Ceti as TauCeti.CountablyRectifiable.ae_tendsto_euclideanHausdorffMeasure_inter_closedBall_div.

Sources
LeanTauCeti.CountablyRectifiable.ae_tendsto_euclideanHausdorffMeasure_inter_closedBall_div
Uses 2
Proof usesBrunn–Minkowski inequality · Lebesgue's density theorem in a k-plane

TheoremGordan's lemma#

The dual semigroup of a lattice-rational cone in an integral lattice is finitely generated. Salience is not required.

TauCeti.Toric.IsLatticeRational.fg_dualSemigroup.{u_1, u_2} {N : Type u_1} {V : Type u_2}
  [AddCommGroup N] [AddCommGroup V] [_root_.Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V}
  (hσ : TauCeti.Toric.IsLatticeRational i σ) (hi : TauCeti.Toric.IsIntegralLattice i) :
  AddMonoid.FG ↥(TauCeti.Toric.dualSemigroup hi σ)
Lean

Formalized in Tau Ceti as TauCeti.Toric.IsLatticeRational.fg_dualSemigroup.

Sources
LeanTauCeti.Toric.IsLatticeRational.fg_dualSemigroup
Used by 6
Used byTauCeti.Toric.Fan.algebraicAnalyticEquiv_smul · TauCeti.Toric.Fan.compactSpace_analyticRealization_iff_isComplete · TauCeti.Toric.Fan.exists_partialDiffeomorph_analyticBoundaryComponent_normalForm · TauCeti.Toric.Fan.isProperMap_analyticMap_starSubdivisionAlong · TauCeti.Toric.projectiveSpaceDiffeomorph · The cone-by-cone properness criterion

TheoremThe Jacobi identity for the Jacobi bracket#

For a contact form on a finite-dimensional manifold and C² functions f, g, k, {f, {g, k}_α}_α + {g, {k, f}_α}_α + {k, {f, g}_α}_α = 0.

TauCeti.SmoothForm.IsContactForm.jacobiBracket_jacobi.{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] [IsManifold I (↑⊤) M]
  {α : TauCeti.SmoothForm I M ℝ 1} {f g k : M → ℝ} [FiniteDimensional ℝ E] (hα : α.IsContactForm)
  (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f)
  (hg : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 g)
  (hk : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 k) (x : M) :
  α.jacobiBracket f (α.jacobiBracket g k) x + α.jacobiBracket g (α.jacobiBracket k f) x +
      α.jacobiBracket k (α.jacobiBracket f g) x =
    0
Lean

Formalized in Tau Ceti as TauCeti.SmoothForm.IsContactForm.jacobiBracket_jacobi.

Sources
LeanTauCeti.SmoothForm.IsContactForm.jacobiBracket_jacobi
Uses 2
Proof usesCartan's formula for a contact Hamiltonian vector field · TauCeti.SmoothForm.instModule

TheoremLebesgue's density theorem in a k-plane#

Let ι be an isometry from k-dimensional Euclidean space into X. Every subset S of its range has k-dimensional density one at μHE[k]-almost every point of S. No measurability of S is needed.

Isometry.ae_tendsto_euclideanHausdorffMeasure_inter_closedBall_div.{u_1} {X : Type u_1}
  [MetricSpace X] [MeasurableSpace X] [BorelSpace X] {k : ℕ} {ι : EuclideanSpace ℝ (Fin k) → X}
  (hι : Isometry ι) {S : Set X} (hS : S ⊆ Set.range ι) :
  ∀ᵐ (x : X) ∂MeasureTheory.Measure.euclideanHausdorffMeasure k,
    x ∈ S →
      Filter.Tendsto
        (fun r =>
          (MeasureTheory.Measure.euclideanHausdorffMeasure k) (S ∩ Metric.closedBall x r) /
            MeasureTheory.volume (Metric.closedBall 0 r))
        (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)
Lean

Formalized in Tau Ceti as Isometry.ae_tendsto_euclideanHausdorffMeasure_inter_closedBall_div.

Sources
LeanIsometry.ae_tendsto_euclideanHausdorffMeasure_inter_closedBall_div
Used by 1
Used byThe density theorem for rectifiable sets

TheoremThe Smale conjecture implies Cerf's theorem#

A homotopy equivalence is surjective on path components: if g is a homotopy inverse of the inclusion O(4) → Diff(S³), then every f is joined to the image of g f by the homotopy from the composite to the identity.

TauCeti.SmaleConjecture.cerfTheorem (h : TauCeti.SmaleConjecture) : TauCeti.CerfTheorem
Lean

Formalized in Tau Ceti as TauCeti.SmaleConjecture.cerfTheorem, assuming TauCeti.SmaleConjecture, a proposition Tau Ceti defines.

Sources
LeanTauCeti.SmaleConjecture.cerfTheorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.