JacobiNearZero.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform relative errors at the initial endpoint. These estimates let the Jacobi approximation be used on intervals reaching zero, where the inverse of the exact Jacobi matrix itself is unbounded.

theorem OAI.PositiveEinsteinFour.Jacobi.relative_position_error line 20

Source documentation

Dividing the position error by time leaves an error of order one mesh step, uniformly over every positive mesh index.

theorem relative_position_error {x X : E} {i : ℕ} {h C K : ℝ}
    (hi : 0 < i) (hh : 0 < h)
    (herr : ‖x - X‖ ≤ C * i * h ^ 2 * Real.exp (K * i * h)) :
    ‖((1 : ℝ) / (i * h)) • x - ((1 : ℝ) / (i * h)) • X‖ ≤
      C * h * Real.exp (K * i * h) := by
…

theorem OAI.PositiveEinsteinFour.Jacobi.relative_position_near_initial line 36

Source documentation

The relative approximation is close to its initial derivative even at the first mesh point; no lower cutoff for time is needed.

theorem relative_position_near_initial {x X e : E} {i : ℕ} {h C K L : ℝ}
    (hi : 0 < i) (hh : 0 < h)
    (herr : ‖x - X‖ ≤ C * i * h ^ 2 * Real.exp (K * i * h))
    (hexact : ‖((1 : ℝ) / (i * h)) • X - e‖ ≤ L * (i * h)) :
    ‖((1 : ℝ) / (i * h)) • x - e‖ ≤
      C * h * Real.exp (K * i * h) + L * (i * h) := by
…

theorem OAI.PositiveEinsteinFour.Jacobi.exact_relative_position_near_initial line 47

Source documentation

The exact solution divided by time approaches its initial derivative with a quantitative bound, directly from the differential equation.

theorem exact_relative_position_near_initial {X V : ℝ → E} {e : E} {t L : ℝ}
    (ht : 0 < t) (hL : 0 ≤ L) (hX0 : X 0 = 0) (hV0 : V 0 = e)
    (hX : ∀ s ∈ Set.Icc 0 t, HasDerivAt X (V s) s)
    (hV : ∀ s ∈ Set.Icc 0 t, ‖V s - e‖ ≤ L * s) :
    ‖((1 : ℝ) / t) • X t - e‖ ≤ L * t := by
…

theorem OAI.PositiveEinsteinFour.Jacobi.quadratic_lower_of_norm_error line 68

Source documentation

The operator-norm neighborhood used to keep the symmetric Schur pivots positive. This lower bound also records the size of the positive margin.

theorem quadratic_lower_of_norm_error
    {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
    (A : F →L[ℝ] F) (c : ℝ) (x : F) :
    (c - ‖A - c • ContinuousLinearMap.id ℝ F‖) * ‖x‖ ^ 2 ≤ inner ℝ (A x) x := by
…

theorem OAI.PositiveEinsteinFour.Jacobi.quadratic_pos_of_norm_error line 88

Source documentation

Strict positivity follows without taking an inverse of a limiting matrix. Symmetry can then be supplied separately by the Schur recurrence.

theorem quadratic_pos_of_norm_error
    {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
    {A : F →L[ℝ] F} {c : ℝ}
    (hA : ‖A - c • ContinuousLinearMap.id ℝ F‖ < c) {x : F} (hx : x ≠ 0) :
    0 < inner ℝ (A x) x := by
…