EulerTrajectory.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The actual clipped-register iteration obeys the proved Euler error estimate. All numerical values here are the rational register values; the hypotheses concern the usual velocity error, speed and Lipschitz bounds.

def OAI.ContinuumCoulomb.EulerRegisters.initial line 15
def OAI.ContinuumCoulomb.EulerRegisters.trajectory line 18
theorem OAI.ContinuumCoulomb.EulerRegisters.trajectory_zero line 22
theorem OAI.ContinuumCoulomb.EulerRegisters.trajectory_succ line 25

theorem OAI.ContinuumCoulomb.EulerRegisters.trajectory_error line 36

Source documentation

Final error for the exact rational register recurrence. The box condition is only imposed on the true solution, not on numerical proposals.

theorem trajectory_error (evaluate : E → ℚ → Triple → Triple) (e : E)
    {N D : ℕ} (hN : 0 < N) (hD : 0 < D) (B : ℕ) (r : Registers)
    (v : ℝ → Position → Position) (z : ℝ → Position)
    {L M δ : ℝ} (hL : 0 ≤ L) (hM : 0 ≤ M) (hδ : 0 ≤ δ)
    (hz : ∀ t ∈ Set.Icc (0:ℝ) 1,
      HasDerivWithinAt z (v t (z t)) (Set.Icc (0:ℝ) 1) t)
    (hbound : ∀ t ∈ Set.Icc (0:ℝ) 1, ‖v t (z t)‖ ≤ M)
    (hLip : ∀ s ∈ Set.Icc (0:ℝ) 1, ∀ t ∈ Set.Icc (0:ℝ) 1, ∀ x w,
      ‖v s x-v t w‖ ≤ L*(|s-t|+‖x-w‖))
    (hbox : ∀ t ∈ Set.Icc (0:ℝ) 1, ∀ a, |z t a| ≤ (B:ℝ)/(D:ℝ))
    (heval : ∀ n < N,
      ‖position (evaluate e ((n:ℚ)*(N:ℚ)⁻¹) (trajectory evaluate e N D B r n))-
…

Mentions: OAI.ContinuumCoulomb.EulerRegisters.Registers, OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.EulerRegisters.trajectory