Euler method

TheoremUniform quadratic bound on the explicit Euler local error#✓fully proved

Let \(E\) be a real normed space, let \(t_0 < T\) be real numbers, let \(f : \mathbb{R} \times E \to E\) be \(C^2\), and let \(x : \mathbb{R} \to E\) be differentiable at every \(t \in [t_0, T]\) with \(x'(t) = f(t, x(t))\). Then there is a constant \(C \ge 0\) such that \(\|x(t + h) - (x(t) + h f(t, x(t)))\| \le C h^2\) for every \(h \in (0, T - t_0]\) and every \(t \in [t_0, T]\) with \(t + h \le T\).

theorem _root_.ODE.exists_explicitEuler_localTruncationError_le
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (f : ℝ → E → E) (t₀ T : ℝ) (hT : t₀ < T)
    (hf : ContDiff ℝ 2 (Function.uncurry f))
    (x : ℝ → E) (hx : ∀ t ∈ Set.Icc t₀ T, HasDerivAt x (f t (x t)) t) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ h ∈ Set.Ioc 0 (T - t₀),
      ∀ t ∈ Set.Icc t₀ T, t + h ≤ T →
        ‖x (t + h) - (x t + h • f t (x t))‖ ≤ C * h ^ 2

Used by 2

Used byFirst-order convergence of the explicit Euler method · Local truncation error of the explicit Euler method

TheoremFirst-order convergence of the explicit Euler method#✓fully proved

Let \(E\) be a real Banach space, let \(t_0 < T\), let \(x_0 \in E\) and \(L \ge 0\), and let \(f : \mathbb{R} \times E \to E\) be \(C^2\) with \(f(t, \cdot)\) \(L\)-Lipschitz for every \(t \in [t_0, T]\). Then there are a function \(x : \mathbb{R} \to E\) with \(x(t_0) = x_0\) and \(x'(t) = f(t, x(t))\) for every \(t \in [t_0, T]\), and a constant \(C\), such that the following holds for every step size \(h \in (0, T - t_0]\): if \((X_n)_{n \in \mathbb{N}}\) is the explicit Euler sequence \(X_0 = x_0\), \(X_{n+1} = X_n + h f(t_0 + n h, X_n)\), then \(\|X_n - x(t_0 + n h)\| \le C h\) for every \(n \in \mathbb{N}\) with \(n h \le T - t_0\).

Proof: clamp the time variable and use global existence for globally Lipschitz right-hand sides. The local truncation bound and the discrete Grönwall inequality then give the first-order global estimate.

theorem explicit_euler_first_order_convergence
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    (f : ℝ → E → E) (t₀ T : ℝ) (x₀ : E) (L : NNReal)
    (hT : t₀ < T)
    (hf : ContDiff ℝ 2 (Function.uncurry f))
    (hlip : ∀ t ∈ Set.Icc t₀ T, LipschitzWith L (f t)) :
    ∃ x : ℝ → E, x t₀ = x₀ ∧ (∀ t ∈ Set.Icc t₀ T, HasDerivAt x (f t (x t)) t) ∧
      ∃ C : ℝ, ∀ h ∈ Set.Ioc 0 (T - t₀), ∀ X : ℕ → E, X 0 = x₀ →
        (∀ n, X (n + 1) = X n + h • f (t₀ + (n : ℝ) * h) (X n)) →
        ∀ n : ℕ, (n : ℝ) * h ≤ T - t₀ →
          ‖X n - x (t₀ + (n : ℝ) * h)‖ ≤ C * h

Sources

• E. Hairer, S. P. Nørsett and G. Wanner, Solving Ordinary Differential Equations I, 2nd ed., Theorem I.7.3; stable ref https://en.wikipedia.org/wiki/Euler_method.

Uses 2

Proof usesGlobal existence and uniqueness for globally Lipschitz ODEs · Uniform quadratic bound on the explicit Euler local error

TheoremLocal truncation error of the explicit Euler method#✓fully proved

Let \(E\) be a real Banach space, let \(t_0 < T\), let \(f : \mathbb{R} \times E \to E\) be \(C^2\), let \(x_0 \in E\), and let \(x : \mathbb{R} \to E\) satisfy \(x(t_0) = x_0\) and \(x'(t) = f(t, x(t))\) for every \(t \in [t_0, T]\). Then there is a constant \(C\) such that \(\|x(t + h) - (x(t) + h f(t, x(t)))\| \le C h^2\) for every \(h \in (0, T - t_0]\) and every \(t \in [t_0, T]\) with \(t + h \le T\).

Proof: differentiate the velocity by the chain rule, bound that derivative on the compact time interval, and apply the mean value inequality twice.

theorem explicit_euler_local_truncation_error
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    (f : ℝ → E → E) (t₀ T : ℝ) (x₀ : E)
    (hT : t₀ < T)
    (hf : ContDiff ℝ 2 (Function.uncurry f))
    (x : ℝ → E) (hx0 : x t₀ = x₀)
    (hx : ∀ t ∈ Set.Icc t₀ T, HasDerivAt x (f t (x t)) t) :
    ∃ C : ℝ, ∀ h ∈ Set.Ioc 0 (T - t₀), ∀ t ∈ Set.Icc t₀ T, t + h ≤ T →
      ‖x (t + h) - (x t + h • f t (x t))‖ ≤ C * h ^ 2

Sources

• E. Hairer, S. P. Nørsett and G. Wanner, Solving Ordinary Differential Equations I, 2nd ed., Section I.7.

Uses 1

Proof usesUniform quadratic bound on the explicit Euler local error

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.