OAI/Geometry/EinsteinFour/JacobiWronskian.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Symmetry of the discrete Jacobi ratios from their preserved Wronskian.

  1. theorem OAI.PositiveEinsteinFour.Jacobi.kick_wronskian line 13
  2. theorem OAI.PositiveEinsteinFour.Jacobi.drift_wronskian line 19
  3. theorem OAI.PositiveEinsteinFour.Jacobi.discrete_wronskian line 25
  4. theorem OAI.PositiveEinsteinFour.Jacobi.next_discrete_wronskian line 38
  5. theorem OAI.PositiveEinsteinFour.Jacobi.ratio_symmetric_of_wronskian line 45
  6. theorem OAI.PositiveEinsteinFour.Jacobi.discrete_ratio_symmetric line 60
  7. def OAI.PositiveEinsteinFour.Jacobi.pivotCoefficient line 70
  8. theorem OAI.PositiveEinsteinFour.Jacobi.one_add_pivotCoefficient_symmetric line 75

    Source documentation

    Symmetry also holds for the totalized coefficient before the mesh is known to be preconjugate: a singular position has inverse zero.

    theorem one_add_pivotCoefficient_symmetric (R : ℕ → NormalMatrix) {h : ℝ}
    (hh : h ≠ 0) (hR : ∀ i, (R i)ᵀ = R i) (i : ℕ) :
    ((1 : NormalMatrix) + ((1 : ℝ) / i) • pivotCoefficient R h i)ᵀ =
      1 + ((1 : ℝ) / i) • pivotCoefficient R h i := by
…

    Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.pivotCoefficient