AcceptedTheorem · Statement with omitted proof

Explicit Dirichlet heat error on an interval

Forward Euler with centered spatial differences gives a second-order maximum-norm error bound under a CFL condition.

Larsson & Thomée ↗
Theorem 9.5 · printed p. 139

Download Lean file ↓

Formal statement. The assumptions and conclusion are explicit; the theorem proof is omitted (sorry).

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

Forward Euler with centered spatial differences gives a second-order maximum-norm error bound under a CFL condition.

\|U^n-u(t_n)\|_{\infty,h}\le Ct_nh^2\sup_{0\le t\le t_n}|u(t)|_{C^4}.

Assumptions & context

A uniform unit-interval grid, positive time step with $k/h^2\le1/2$ , compatible heat initial-boundary data, and a uniform fourth-derivative bound up to the comparison time.

Source

Larsson & Thomée. Partial differential equations with numerical methods.

Theorem 9.5 · printed p. 139

02 / LEAN REPRESENTATION

Formal statement

Statement with omitted proof. Expand the complete file below to read imports, local definitions and surrounding context.

theorem forwardEuler_dirichlet_maxNorm_error :
    ∃ C : ℝ, ∀ (M : ℕ), 0 < M → ∀ (k : ℝ), 0 < k →
      k / (1 / (M : ℝ)) ^ 2 ≤ 1 / 2 →
      ∀ (v : ℝ → ℝ) (u : ℝ → ℝ → ℝ),
        ContinuousOn v (Icc (0:ℝ) 1) →
        IsHeatSolution v u →
        ∀ (n : ℕ) (K : ℝ),
          (∀ t ∈ Icc (0:ℝ) ((n : ℝ) * k), C4SeminormLE (fun x => u x t) K) →
          maxNormH M (fun j =>
              forwardEuler M (k / (1 / (M : ℝ)) ^ 2) v n j
                - u ((j : ℝ) / (M : ℝ)) ((n : ℝ) * k))
            ≤ C * ((n : ℝ) * k) * (1 / (M : ℝ)) ^ 2 * K := by
  sorry

Complete Lean file and local definitions

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm95

open Set

/-- Classical solution of the model problem (9.19):
`u_t = u_xx` in `Ω × (0,∞)` with `Ω = (0,1)`, `u(0,t) = u(1,t) = 0` for `t > 0`,
and `u(·,0) = v` in `Ω`. Here `u x t` is `u(x,t)`. The solution is taken continuous on
`[0,1] × [0,∞)`, which is the classical solution concept. -/
def IsHeatSolution (v : ℝ → ℝ) (u : ℝ → ℝ → ℝ) : Prop :=
  ContinuousOn (fun p : ℝ × ℝ => u p.1 p.2) (Icc (0:ℝ) 1 ×ˢ Ici (0:ℝ)) ∧
  (∀ x ∈ Ioo (0:ℝ) 1, ∀ t : ℝ, 0 < t →
      DifferentiableAt ℝ (fun s => u x s) t ∧
      ContDiffAt ℝ 2 (fun y => u y t) x ∧
      deriv (fun s => u x s) t = iteratedDeriv 2 (fun y => u y t) x) ∧
  (∀ t : ℝ, 0 < t → u 0 t = 0 ∧ u 1 t = 0) ∧
  (∀ x ∈ Ioo (0:ℝ) 1, u x 0 = v x)

/-- The explicit forward Euler scheme (9.20) with `h = 1/M`, `x_j = j h`, mesh ratio `λ`:
`U_j^0 = v(x_j)` for `j = 0,…,M`, and
`U_j^{n+1} = λ(U_{j-1}^n + U_{j+1}^n) + (1-2λ)U_j^n` for `j = 1,…,M-1`,
`U_0^{n+1} = U_M^{n+1} = 0`. Indices `j > M` are irrelevant (set to `0`). -/
def forwardEuler (M : ℕ) (lam : ℝ) (v : ℝ → ℝ) : ℕ → ℕ → ℝ
  | 0, j => v ((j : ℝ) / (M : ℝ))
  | n + 1, j =>
      if j = 0 ∨ M ≤ j then 0
      else lam * (forwardEuler M lam v n (j - 1) + forwardEuler M lam v n (j + 1))
        + (1 - 2 * lam) * forwardEuler M lam v n j

/-- Discrete maximum norm `‖W‖_{∞,h} = max_{j = 0,…,M} |W_j|`. -/
def maxNormH (M : ℕ) (W : ℕ → ℝ) : ℝ :=
  ⨆ j : Fin (M + 1), |W (j : ℕ)|

/-- `|w|_{C^4} ≤ K` on `Ω̄ = [0,1]`: `w` is `C^4` on `[0,1]` and the C⁴ seminorm
`sup_{x ∈ [0,1]} |w⁗(x)|` is at most `K`. -/
def C4SeminormLE (w : ℝ → ℝ) (K : ℝ) : Prop :=
  ContDiffOn ℝ 4 w (Icc (0:ℝ) 1) ∧
  ∀ x ∈ Icc (0:ℝ) 1, |iteratedDerivWithin 4 w (Icc (0:ℝ) 1) x| ≤ K

/-- Theorem 9.5 (Larsson–Thomée). With `h = 1/M`, time step `k > 0`, `λ = k/h² ≤ 1/2`,
`t_n = n k`, `U^n` the forward Euler solution (9.20) and `u` the solution of (9.19),
`‖U^n - u^n‖_{∞,h} ≤ C t_n h² max_{t ≤ t_n} |u(·,t)|_{C^4}` for `t_n ≥ 0`.
The maximum over `t ∈ [0,t_n]` is expressed through an arbitrary bound `K` on
`|u(·,t)|_{C^4}` for all `t ∈ [0,t_n]` (equivalent to using the maximum when it is finite). -/
theorem forwardEuler_dirichlet_maxNorm_error :
    ∃ C : ℝ, ∀ (M : ℕ), 0 < M → ∀ (k : ℝ), 0 < k →
      k / (1 / (M : ℝ)) ^ 2 ≤ 1 / 2 →
      ∀ (v : ℝ → ℝ) (u : ℝ → ℝ → ℝ),
        ContinuousOn v (Icc (0:ℝ) 1) →
        IsHeatSolution v u →
        ∀ (n : ℕ) (K : ℝ),
          (∀ t ∈ Icc (0:ℝ) ((n : ℝ) * k), C4SeminormLE (fun x => u x t) K) →
          maxNormH M (fun j =>
              forwardEuler M (k / (1 / (M : ℝ)) ^ 2) v n j
                - u ((j : ℝ) / (M : ℝ)) ((n : ℝ) * k))
            ≤ C * ((n : ℝ) * k) * (1 / (M : ℝ)) ^ 2 * K := by
  sorry

end PDETextbook.LarssonThomee.Thm95

How to read the formalization

The regularity bound is imposed on the exact solution throughout the elapsed time interval.

← Back to all statements