AcceptedTheorem · Statement with omitted proof

Von Neumann criterion for discrete L2 stability

For a scalar finite-stencil scheme, the Fourier-symbol condition is equivalent to stability in the discrete square-integrable norm.

Larsson & Thomée ↗
Theorem 9.3 · printed p. 134

Download Lean file ↓

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

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

For a scalar finite-stencil scheme, the Fourier-symbol condition is equivalent to stability in the discrete square-integrable norm.

\text{stability in }\ell_{2,h}\quad\Longleftrightarrow\quad |\widetilde E(\xi)|\le1\ \text{for every }\xi.

Assumptions & context

Finitely supported real stencil coefficients, with the stability and symbol conditions defined in the complete file.

Source

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

Theorem 9.3 · printed p. 134

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_3 (a : ℤ →₀ ℝ) :
    StableL2h a ↔ VonNeumannCondition a := by sorry

Complete Lean file and local definitions

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm93

/-- The explicit finite difference operator (9.8): `(E_k V)_j = ∑_p a_p V_{j-p}`.
The sum is finite: the coefficients `a_p = a_p(λ)`, with `λ = k/h^2` fixed, are given
as a finitely supported family `a : ℤ →₀ ℝ`. -/
def applyE (a : ℤ →₀ ℝ) (V : ℤ → ℝ) : ℤ → ℝ :=
  fun j => ∑ p ∈ a.support, a p * V (j - p)

/-- The symbol `Ẽ(ξ) = ∑_p a_p e^{-i p ξ}` of the operator `E_k`. -/
def symbol (a : ℤ →₀ ℝ) (ξ : ℝ) : ℂ :=
  ∑ p ∈ a.support, (a p : ℂ) * Complex.exp (-(Complex.I * (p : ℂ) * (ξ : ℂ)))

/-- Membership in `l_{2,h}`: a mesh function `V = {V_j}` with finite `l_{2,h}` norm. -/
def InL2h (V : ℤ → ℝ) : Prop :=
  Summable (fun j : ℤ => V j ^ 2)

/-- The discrete norm `‖V‖_{2,h} = (h ∑_j V_j^2)^{1/2}`. -/
def l2hNorm (h : ℝ) (V : ℤ → ℝ) : ℝ :=
  Real.sqrt (h * ∑' j : ℤ, V j ^ 2)

/-- Stability of `E_k^n` in `l_{2,h}`: `‖E_k^n V‖_{2,h} ≤ C ‖V‖_{2,h}` for all `n ≥ 0`
and all `V ∈ l_{2,h}`, with `C` independent of `n`, `V` and the mesh-width `h`
(for the fixed ratio `λ = k/h^2` on which the coefficients depend). -/
def StableL2h (a : ℤ →₀ ℝ) : Prop :=
  ∃ C : ℝ, ∀ h : ℝ, 0 < h → ∀ n : ℕ, ∀ V : ℤ → ℝ, InL2h V →
    l2hNorm h ((applyE a)^[n] V) ≤ C * l2hNorm h V

/-- Von Neumann's condition (9.10): `|Ẽ(ξ)| ≤ 1` for `ξ ∈ ℝ`. -/
def VonNeumannCondition (a : ℤ →₀ ℝ) : Prop :=
  ∀ ξ : ℝ, ‖symbol a ξ‖ ≤ 1

/-- Theorem 9.3: von Neumann's condition (9.10) is necessary and sufficient for
stability of the operator `E_k^n` in `l_{2,h}`. -/
theorem thm_9_3 (a : ℤ →₀ ℝ) :
    StableL2h a ↔ VonNeumannCondition a := by sorry

end PDETextbook.LarssonThomee.Thm93

How to read the formalization

Unlike the neighboring maximum-norm result, this statement supplies both directions of the criterion.

← Back to all statements