OAI/Geometry/EinsteinFour/JacobiScheme.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The concrete noncommuting kick-drift scheme and its Jacobi recurrence.

  1. def OAI.PositiveEinsteinFour.Jacobi.jacobiScheme line 14
  2. def OAI.PositiveEinsteinFour.Jacobi.discretePosition line 21
  3. def OAI.PositiveEinsteinFour.Jacobi.discreteVelocity line 23
  4. theorem OAI.PositiveEinsteinFour.Jacobi.discretePosition_zero line 25
  5. theorem OAI.PositiveEinsteinFour.Jacobi.discreteVelocity_zero line 28
  6. theorem OAI.PositiveEinsteinFour.Jacobi.discreteVelocity_succ line 31
  7. theorem OAI.PositiveEinsteinFour.Jacobi.discretePosition_succ line 35
  8. theorem OAI.PositiveEinsteinFour.Jacobi.discretePosition_one line 39
  9. theorem OAI.PositiveEinsteinFour.Jacobi.discretePosition_recurrence line 45

    Source documentation

    Matrix multiplication stays in its original order in the second-order recurrence. The curvature is sampled at the interior node.

    theorem discretePosition_recurrence (A : ℕ → R) (h : ℝ) (n : ℕ) :
    discretePosition A h (n + 2) =
      ((2 : ℝ) • (1 : R) - h ^ 2 • A (n + 1)) * discretePosition A h (n + 1) -
        discretePosition A h n := by
…

    Mentions: OAI.PositiveEinsteinFour.Jacobi.discretePosition

  10. def OAI.PositiveEinsteinFour.Jacobi.normalizedDiscrete line 57
  11. theorem OAI.PositiveEinsteinFour.Jacobi.normalizedDiscrete_zero line 60
  12. theorem OAI.PositiveEinsteinFour.Jacobi.normalizedDiscrete_one line 63
  13. theorem OAI.PositiveEinsteinFour.Jacobi.normalizedDiscrete_recurrence line 67