OAI/Geometry/EinsteinFour/JacobiODELimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Determinant convergence from the same preconjugate Jacobi ODE data.

  1. theorem OAI.PositiveEinsteinFour.Jacobi.RegularJacobi.endpoint_position_tendsto line 19
  2. theorem OAI.PositiveEinsteinFour.Jacobi.RegularJacobi.normalizedDiscrete_eventually_isUnit line 45
  3. theorem OAI.PositiveEinsteinFour.Jacobi.RegularJacobi.curvatureDirichlet_det_tendsto line 68