OAI/Geometry/EinsteinFour/JacobiODEPositivity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Preconjugate positivity from the Jacobi ODE.

  1. def OAI.PositiveEinsteinFour.Jacobi.meshStep line 16
  2. def OAI.PositiveEinsteinFour.Jacobi.meshCurvature line 18
  3. theorem OAI.PositiveEinsteinFour.Jacobi.meshStep_tendsto line 21
  4. structure OAI.PositiveEinsteinFour.Jacobi.RegularJacobi line 28

    Source documentation

    Precisely the local ODE and regularity bounds used by the discretization. All constants can be chosen on a compact interval of a smooth Jacobi curve.

    structure RegularJacobi (t : ℝ) where
…
  5. def OAI.PositiveEinsteinFour.Jacobi.RegularJacobi.localError line 56
  6. def OAI.PositiveEinsteinFour.Jacobi.RegularJacobi.growth line 58
  7. def OAI.PositiveEinsteinFour.Jacobi.RegularJacobi.positionError line 60
  8. def OAI.PositiveEinsteinFour.Jacobi.RegularJacobi.velocityError line 62
  9. theorem OAI.PositiveEinsteinFour.Jacobi.RegularJacobi.positionError_tendsto line 65
  10. theorem OAI.PositiveEinsteinFour.Jacobi.RegularJacobi.velocityError_tendsto line 71
  11. theorem OAI.PositiveEinsteinFour.Jacobi.RegularJacobi.uniform_errors line 77
  12. theorem OAI.PositiveEinsteinFour.Jacobi.RegularJacobi.curvatureDirichlet_eventually_posDef line 119

    Source documentation

    The Jacobi ODE implies positivity of the finite curvature matrices.

    theorem curvatureDirichlet_eventually_posDef (ht : 0 < t)
    (hpre : ∀ s, 0 < s → s ≤ t → IsUnit (d.J s)) :
    ∀ᶠ N : ℕ in atTop,
      (curvatureDirichlet t (fun i : Fin N =>
        d.R (((i.val + 1 : ℕ) : ℝ) * meshStep t N) - 1)).PosDef := by
…

    Mentions: OAI.PositiveEinsteinFour.Jacobi.curvatureDirichlet, OAI.PositiveEinsteinFour.Jacobi.meshStep