JacobiApproximation.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Stability and consistency for the kick-drift approximation of the matrix Jacobi equation. The estimates use operator bounds, so no two curvature matrices are required to commute.

def OAI.PositiveEinsteinFour.Jacobi.kick line 21
def OAI.PositiveEinsteinFour.Jacobi.drift line 23

theorem OAI.PositiveEinsteinFour.Jacobi.first_order_remainder line 27

Source documentation

A first-order Taylor remainder with the uniform quadratic bound needed for convergence. The slightly larger constant avoids unnecessary sharpness.

theorem first_order_remainder {f d : ℝ → E} {a h L : ℝ}
    (hh : 0 ≤ h) (hL : 0 ≤ L)
    (hd : ∀ s ∈ Set.Icc a (a + h), HasDerivAt f (d s) s)
    (hlip : ∀ s ∈ Set.Icc a (a + h), ‖d s - d a‖ ≤ L * (s - a)) :
    ‖f (a + h) - f a - h • d a‖ ≤ L * h ^ 2 := by
…

theorem OAI.PositiveEinsteinFour.Jacobi.kick_stability line 44
theorem OAI.PositiveEinsteinFour.Jacobi.kick_drift_stability line 59

theorem OAI.PositiveEinsteinFour.Jacobi.kick_drift_local_error line 79

Source documentation

Local error of the actual update, from the two Taylor remainders.

theorem kick_drift_local_error {R : E →L[ℝ] E} {h Cx Cv F : ℝ}
    {x v x' v' : E} (hh : 0 ≤ h)
    (hx : ‖x' - x - h • v‖ ≤ Cx * h ^ 2)
    (hv : ‖v' - v + h • R x‖ ≤ Cv * h ^ 2)
    (hforce : ‖R x‖ ≤ F) :
    ‖x' - drift R h x v‖ + ‖v' - kick R h x v‖ ≤
      (Cx + Cv + F) * h ^ 2 := by
…

Mentions: OAI.PositiveEinsteinFour.Jacobi.drift, OAI.PositiveEinsteinFour.Jacobi.kick

theorem OAI.PositiveEinsteinFour.Jacobi.kick_drift_consistency line 103

Source documentation

The local error hypotheses follow from the differential equation and Lipschitz bounds for its velocity and acceleration on the current interval.

theorem kick_drift_consistency {R : ℝ → E →L[ℝ] E} {X V : ℝ → E}
    {a h Lx Lv F : ℝ} (hh : 0 ≤ h) (hLx : 0 ≤ Lx) (hLv : 0 ≤ Lv)
    (hX : ∀ s ∈ Set.Icc a (a + h), HasDerivAt X (V s) s)
    (hV : ∀ s ∈ Set.Icc a (a + h), HasDerivAt V (-(R s) (X s)) s)
    (hvelocity : ∀ s ∈ Set.Icc a (a + h), ‖V s - V a‖ ≤ Lx * (s - a))
    (hacceleration : ∀ s ∈ Set.Icc a (a + h),
      ‖-(R s) (X s) - -(R a) (X a)‖ ≤ Lv * (s - a))
    (hforce : ‖(R a) (X a)‖ ≤ F) :
    ‖X (a + h) - drift (R a) h (X a) (V a)‖ +
      ‖V (a + h) - kick (R a) h (X a) (V a)‖ ≤ (Lx + Lv + F) * h ^ 2 := by
…

Mentions: OAI.PositiveEinsteinFour.Jacobi.drift, OAI.PositiveEinsteinFour.Jacobi.kick

theorem OAI.PositiveEinsteinFour.Jacobi.finite_error_bound line 120

Source documentation

Discrete Grönwall on precisely the finite interval used by the Jacobi approximation. It also handles zero step size and zero local error.

theorem finite_error_bound {u : ℕ → ℝ} {N : ℕ} {h K C : ℝ}
    (hh : 0 ≤ h) (hK : 0 ≤ K) (hC : 0 ≤ C)
    (hu0 : u 0 = 0) (hu : ∀ i ≤ N, 0 ≤ u i)
    (hstep : ∀ i < N, u (i + 1) ≤ (1 + K * h) * u i + C * h ^ 2) :
    u N ≤ C * N * h ^ 2 * Real.exp (K * N * h) := by
…

theorem OAI.PositiveEinsteinFour.Jacobi.finite_error_bound_scaled line 143

theorem OAI.PositiveEinsteinFour.Jacobi.kick_drift_global_error line 156

Source documentation

Propagation of local Jacobi errors, with the curvature operator allowed to vary arbitrarily from one mesh point to the next.

theorem kick_drift_global_error
    {R : ℕ → E →L[ℝ] E} {x v X V : ℕ → E} {N : ℕ} {h K C : ℝ}
    (hh : 0 ≤ h) (hh1 : h ≤ 1) (hK : 0 ≤ K) (hC : 0 ≤ C)
    (hR : ∀ i < N, ‖R i‖ ≤ K)
    (hx0 : x 0 = X 0) (hv0 : v 0 = V 0)
    (hxstep : ∀ i < N, x (i + 1) = drift (R i) h (x i) (v i))
    (hvstep : ∀ i < N, v (i + 1) = kick (R i) h (x i) (v i))
    (hlocal : ∀ i < N,
      ‖X (i + 1) - drift (R i) h (X i) (V i)‖ +
      ‖V (i + 1) - kick (R i) h (X i) (V i)‖ ≤ C * h ^ 2) :
    ‖x N - X N‖ + ‖v N - V N‖ ≤
      C * N * h ^ 2 * Real.exp ((1 + 2 * K) * N * h) := by
…

Mentions: OAI.PositiveEinsteinFour.Jacobi.drift, OAI.PositiveEinsteinFour.Jacobi.kick

theorem OAI.PositiveEinsteinFour.Jacobi.kick_drift_global_error_scaled line 186

Source documentation

The global estimate on a mesh of fixed total length has order 1/N.

theorem kick_drift_global_error_scaled
    {R : ℕ → E →L[ℝ] E} {x v X V : ℕ → E} {N : ℕ} {t K C : ℝ}
    (hN : 0 < N) (ht : 0 ≤ t) (hmesh : t / N ≤ 1)
    (hK : 0 ≤ K) (hC : 0 ≤ C) (hR : ∀ i < N, ‖R i‖ ≤ K)
    (hx0 : x 0 = X 0) (hv0 : v 0 = V 0)
    (hxstep : ∀ i < N, x (i + 1) = drift (R i) (t / N) (x i) (v i))
    (hvstep : ∀ i < N, v (i + 1) = kick (R i) (t / N) (x i) (v i))
    (hlocal : ∀ i < N,
      ‖X (i + 1) - drift (R i) (t / N) (X i) (V i)‖ +
      ‖V (i + 1) - kick (R i) (t / N) (X i) (V i)‖ ≤ C * (t / N) ^ 2) :
    ‖x N - X N‖ + ‖v N - V N‖ ≤
      (C * t ^ 2 * Real.exp ((1 + 2 * K) * t)) / N := by
…

Mentions: OAI.PositiveEinsteinFour.Jacobi.drift, OAI.PositiveEinsteinFour.Jacobi.kick

theorem OAI.PositiveEinsteinFour.Jacobi.converges_of_inverse_mesh_error line 211
Source documentation
Position and backward velocity both converge once the uniform mesh estimate is available. This applies to matrices as a finite-dimensional normed space, without any commutation assumption.
```
theorem converges_of_inverse_mesh_error
    {x v : ℕ → E} {X V : E} {C : ℝ}
    (herror : ∀ᶠ N in atTop,
      ‖x N - X‖ + ‖v N - V‖ ≤ C / N) :
    Tendsto x atTop (nhds X) ∧ Tendsto v atTop (nhds V) := by
…
```