OAI/Geometry/EinsteinFour/ActualJacobiODEMatrix.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The matrix Jacobi equation and its compact-interval regularity bounds. The coefficient is allowed to vary with time and need not commute with its values at other times.

  1. abbrev OAI.PositiveEinsteinFour.Jacobi.JacobiState line 19
  2. def OAI.PositiveEinsteinFour.Jacobi.jacobiStateOperator line 21
  3. theorem OAI.PositiveEinsteinFour.Jacobi.jacobiStateOperator_apply line 26
  4. theorem OAI.PositiveEinsteinFour.Jacobi.continuous_jacobiStateOperator line 29
  5. theorem OAI.PositiveEinsteinFour.Jacobi.norm_jacobiStateOperator_le line 36
  6. structure OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution line 53
  7. theorem OAI.PositiveEinsteinFour.Jacobi.exists_matrixJacobiSolution line 61
  8. theorem OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution.continuous_J line 83
  9. theorem OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution.continuous_V line 86
  10. theorem OAI.PositiveEinsteinFour.Jacobi.MatrixJacobiSolution.exists_regular line 91

    Source documentation

    Every compact interval has the bounds needed by the discrete Jacobi comparison. No uniformity in the interval is assumed.

    theorem exists_regular (R' : ℝ → NormalMatrix) (hR : Continuous R)
    (hR' : Continuous R') (hdR : ∀ s, HasDerivAt R (R' s) s)
    (hsym : ∀ s, (R s)ᵀ = R s) (t : ℝ) :
    ∃ q : RegularJacobi t, q.R = R ∧ q.J = d.J ∧ q.V = d.V := by
…

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