AcceptedTheorem · Statement with omitted proof

First-order error of the upwind transport scheme

The upwind approximation to constant-speed transport has a first-order spatial error bound.

Larsson & Thomée ↗
Theorem 12.1 · printed p. 186

Download Lean file ↓

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

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

The upwind approximation to constant-speed transport has a first-order spatial error bound.

\|U^n-u(t_n)\|_\infty\le Ct_nh|v|_{C^2},\qquad t_n=n\lambda h.

Assumptions & context

A positive time-to-space ratio, $0<a\lambda\le1$ , and twice continuously differentiable initial data with a bounded second derivative.

Source

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

Theorem 12.1 · printed p. 186

02 / LEAN REPRESENTATION

Formal statement

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

theorem thm_12_1 (a lam : ℝ) (hlam : 0 < lam) (hpos : 0 < a * lam) (hle : a * lam ≤ 1) :
    ∃ C : ℝ, ∀ h : ℝ, 0 < h → ∀ v : ℝ → ℝ, ContDiff ℝ 2 v →
      ∀ M : ℝ, (∀ x, |iteratedDeriv 2 v x| ≤ M) →
      ∀ n : ℕ, ∀ x : ℝ,
        |upwindApprox a lam h v n x - exactSolution a v ((n : ℝ) * (lam * h)) x|
          ≤ C * ((n : ℝ) * (lam * h)) * h * M := by
  sorry

Complete Lean file and local definitions

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Ch12

/-- Exact solution operator of (12.1)-(12.2): `(E(t) v)(x) = v(x + a t)`. -/
def exactSolution (a : ℝ) (v : ℝ → ℝ) (t : ℝ) : ℝ → ℝ :=
  fun x => v (x + a * t)

/-- One step of the upwind scheme (12.6), for `U` defined on all of `ℝ`:
`(E_k U)(x) = a λ U(x+h) + (1 - a λ) U(x)`. -/
def upwindStep (a lam h : ℝ) (U : ℝ → ℝ) : ℝ → ℝ :=
  fun x => a * lam * U (x + h) + (1 - a * lam) * U x

/-- Approximate solution `U^n = E_k^n v` from (12.6). -/
def upwindApprox (a lam h : ℝ) (v : ℝ → ℝ) (n : ℕ) : ℝ → ℝ :=
  (upwindStep a lam h)^[n] v

/-- Theorem 12.1 (Larsson–Thomée). The mesh ratio `λ = k/h > 0` is fixed and
`k = λ h`, `t_n = n k`, `n ≥ 0`. The constant `C` is chosen after `a, λ` and before
`h`, `v`, `n`. The maximum norm `‖U^n - u^n‖_C = sup_x |U^n(x) - u^n(x)|` is
expressed pointwise for all `x`, and `|v|_{C^2} = sup_x |v''(x)|` enters through
an arbitrary bound `M` on `|v''|`. This is equivalent to the sup formulation, and
the claim is vacuous when the seminorm is infinite. -/
theorem thm_12_1 (a lam : ℝ) (hlam : 0 < lam) (hpos : 0 < a * lam) (hle : a * lam ≤ 1) :
    ∃ C : ℝ, ∀ h : ℝ, 0 < h → ∀ v : ℝ → ℝ, ContDiff ℝ 2 v →
      ∀ M : ℝ, (∀ x, |iteratedDeriv 2 v x| ≤ M) →
      ∀ n : ℕ, ∀ x : ℝ,
        |upwindApprox a lam h v n x - exactSolution a v ((n : ℝ) * (lam * h)) x|
          ≤ C * ((n : ℝ) * (lam * h)) * h * M := by
  sorry

end PDETextbook.LarssonThomee.Ch12

How to read the formalization

The formal estimate is pointwise in space and uniform through the supplied derivative bound.

← Back to all statements