OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/RoundedEuler.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Grid rounding after every Euler step controls the size of rational intermediates. The rounding error is accumulated in the actual trajectory estimate, separately from the field sampling and time discretization.

  1. def OAI.ContinuumCoulomb.EulerApproximation.roundedIterate line 14
  2. theorem OAI.ContinuumCoulomb.EulerApproximation.rounded_sequence_error line 20
  3. theorem OAI.ContinuumCoulomb.EulerApproximation.rounded_iterate_error line 40
  4. theorem OAI.ContinuumCoulomb.EulerApproximation.uniform_flow_local_defect line 53
  5. theorem OAI.ContinuumCoulomb.EulerApproximation.projected_sequence_error line 73

    Source documentation

    Projection onto a fixed box may move an inaccurate Euler proposal a long way, but it only improves its distance to a trajectory inside that box. This form of the recurrence handles such projections directly.

    theorem projected_sequence_error (v evaluate : ℕ → E → E) (z y : ℕ → E)
    (N : ℕ) {h L δ D R : ℝ} (hh : 0 ≤ h) (hL : 0 ≤ L)
    (hδ : 0 ≤ δ) (hD : 0 ≤ D) (hR : 0 ≤ R)
    (hLip : ∀ n < N, ∀ x, ‖v n x-v n (z n)‖ ≤ L*‖x-z n‖)
    (heval : ∀ n < N, ‖evaluate n (y n)-v n (y n)‖ ≤ δ)
    (hdefect : ∀ n < N, ‖z n+h • v n (z n)-z (n+1)‖ ≤ D)
    (hproject : ∀ n < N, ‖y (n+1)-z (n+1)‖ ≤
      ‖y n+h • evaluate n (y n)-z (n+1)‖+R) :
    ‖y N-z N‖ ≤
      (‖y 0-z 0‖+(N:ℝ)*(h*δ+D+R))*Real.exp ((N:ℝ)*(h*L)) := by
…
  6. theorem OAI.ContinuumCoulomb.EulerApproximation.sampled_unit_error line 92