OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/EulerApproximation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Quantitative inexact Euler estimates. All error assumptions concern the vector field and the actual local differential equation; no endpoint approximation is assumed.

  1. def OAI.ContinuumCoulomb.EulerApproximation.iterate line 16
  2. theorem OAI.ContinuumCoulomb.EulerApproximation.step_error line 20
  3. theorem OAI.ContinuumCoulomb.EulerApproximation.finite_recurrence_bound line 46
  4. theorem OAI.ContinuumCoulomb.EulerApproximation.iterate_error line 76
  5. theorem OAI.ContinuumCoulomb.EulerApproximation.local_defect line 92

    Source documentation

    The actual solution has a quadratic one-step error whenever its velocity is bounded and the field is jointly Lipschitz in time and space.

    theorem local_defect (v : ℝ → E → E) (z : ℝ → E)
    {t h L M : ℝ} (hh : 0 ≤ h) (hL : 0 ≤ L) (hM : 0 ≤ M)
    (hz : ∀ s ∈ Set.Icc t (t+h),
      HasDerivWithinAt z (v s (z s)) (Set.Icc t (t+h)) s)
    (hbound : ∀ s ∈ Set.Icc t (t+h), ‖v s (z s)‖ ≤ M)
    (hLip : ∀ s ∈ Set.Icc t (t+h),
      ‖v s (z s)-v t (z t)‖ ≤ L*(|s-t|+‖z s-z t‖)) :
    ‖z t+h • v t (z t)-z (t+h)‖ ≤ L*(1+M)*h^2 := by
…