JacobiMeshError.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Error bounds at all nodes, including normalization through time zero.

theorem OAI.PositiveEinsteinFour.Jacobi.relative_discrete_error line 15

theorem OAI.PositiveEinsteinFour.Jacobi.next_discrete_velocity_error line 43

Source documentation

The velocity used in a pivot is the next backward velocity. Its distance from the velocity at the current node also tends to zero.

theorem next_discrete_velocity_error {R : ℕ → NormalMatrix} {V : ℝ → NormalMatrix}
    {h t C K L : ℝ} {N : ℕ} (hh : 0 < h) (hC : 0 ≤ C) (hK : 0 ≤ K)
    (_hL : 0 ≤ L) (hNt : ((N + 1 : ℕ) : ℝ) * h ≤ t)
    (herr : ∀ i : ℕ, i ≤ N + 1 →
      ‖discreteVelocity R h i - V (i * h)‖ ≤ C * i * h ^ 2 * Real.exp (K * i * h))
    (hLip : ∀ s ∈ Set.Icc 0 t, ∀ r ∈ Set.Icc 0 t, ‖V s - V r‖ ≤ L * |s - r|) :
    ∀ i : ℕ, i ≤ N →
      ‖discreteVelocity R h (i + 1) - V (i * h)‖ ≤
        (C * t * Real.exp (K * t) + L) * h := by
…

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