AcceptedTheorem · Statement with omitted proof

Maximum-norm error of explicit heat differences

The explicit whole-line heat scheme has second-order spatial accuracy when the time step satisfies the stability restriction.

Larsson & Thomée ↗
Theorem 9.1 · printed p. 132

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 explicit whole-line heat scheme has second-order spatial accuracy when the time step satisfies the stability restriction.

\|U^n-u(t_n)\|_{\infty,h}\le Ct_nh^2|v|_{C^4},\qquad 0<k/h^2\le\tfrac12.

Assumptions & context

A fixed positive ratio $\lambda=k/h^2\le1/2$ , smooth bounded initial data, and the explicit difference recurrence.

Source

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

Theorem 9.1 · printed p. 132

02 / LEAN REPRESENTATION

Formal statement

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

theorem thm_9_1 (lam : ℝ) (hlam_pos : 0 < lam) (hlam : lam ≤ 1 / 2) :
    ∃ C : ℝ, ∀ (h k : ℝ), 0 < h → 0 < k → k / h ^ 2 = lam →
      ∀ v : ℝ → ℝ, ContDiff ℝ (⊤ : ℕ∞) v → (∃ M : ℝ, ∀ x, |v x| ≤ M) →
      ∀ U : ℕ → ℤ → ℝ, SolvesExplicitScheme lam h v U →
      ∀ n : ℕ,
        gridSupNorm (fun j : ℤ => U n j - heatSolution v ((j : ℝ) * h) ((n : ℝ) * k))
          ≤ ENNReal.ofReal (C * ((n : ℝ) * k) * h ^ 2) * c4Seminorm v := by
  sorry

Complete Lean file and local definitions

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm91

/-- Solution of the pure initial value problem (9.1), given by the representation (9.2):
`u(x,t) = (4πt)^{-1/2} ∫ e^{-y²/4t} v(x-y) dy` for `t > 0`, and `u(·,0) = v`. -/
def heatSolution (v : ℝ → ℝ) (x t : ℝ) : ℝ :=
  if t ≤ 0 then v x
  else (1 / Real.sqrt (4 * Real.pi * t)) *
    ∫ y : ℝ, Real.exp (-y ^ 2 / (4 * t)) * v (x - y)

/-- Discrete maximum norm (9.5): `‖w‖_{∞,h} = sup_{j ∈ ℤ} |w_j|`, valued in `[0,∞]`. -/
def gridSupNorm (w : ℤ → ℝ) : ℝ≥0∞ :=
  ⨆ j : ℤ, ENNReal.ofReal |w j|

/-- The seminorm `|v|_{C^4} = sup_{x ∈ ℝ} |v''''(x)|`, valued in `[0,∞]`. -/
def c4Seminorm (v : ℝ → ℝ) : ℝ≥0∞ :=
  ⨆ x : ℝ, ENNReal.ofReal |iteratedDeriv 4 v x|

/-- `U` is the solution of the explicit scheme (9.4) with `λ = lam`, mesh width `h`,
and initial values `U_j^0 = v(x_j)`, `x_j = j h`. -/
def SolvesExplicitScheme (lam h : ℝ) (v : ℝ → ℝ) (U : ℕ → ℤ → ℝ) : Prop :=
  (∀ j : ℤ, U 0 j = v ((j : ℝ) * h)) ∧
  ∀ (n : ℕ) (j : ℤ),
    U (n + 1) j = lam * U n (j - 1) + (1 - 2 * lam) * U n j + lam * U n (j + 1)

/-- Theorem 9.1 (Larsson–Thomée). Let `U^n` solve (9.4) and `u` solve (9.1), with
`k/h² = λ ≤ 1/2`. Then there is a constant `C` such that
`‖U^n - u^n‖_{∞,h} ≤ C t_n h² |v|_{C^4}` for `t_n = n k ≥ 0`, where `u^n_j = u(x_j, t_n)`. -/
theorem thm_9_1 (lam : ℝ) (hlam_pos : 0 < lam) (hlam : lam ≤ 1 / 2) :
    ∃ C : ℝ, ∀ (h k : ℝ), 0 < h → 0 < k → k / h ^ 2 = lam →
      ∀ v : ℝ → ℝ, ContDiff ℝ (⊤ : ℕ∞) v → (∃ M : ℝ, ∀ x, |v x| ≤ M) →
      ∀ U : ℕ → ℤ → ℝ, SolvesExplicitScheme lam h v U →
      ∀ n : ℕ,
        gridSupNorm (fun j : ℤ => U n j - heatSolution v ((j : ℝ) * h) ((n : ℝ) * k))
          ≤ ENNReal.ofReal (C * ((n : ℝ) * k) * h ^ 2) * c4Seminorm v := by
  sorry

end PDETextbook.LarssonThomee.Thm91

How to read the formalization

The estimate grows linearly with elapsed time. Holding the ratio fixed ties the time step to the squared mesh width.

← Back to all statements