AcceptedLemma · Statement with omitted proof

Maximum-norm stability of a one-dimensional difference operator

A grid function is bounded by its endpoint values and discrete residual.

Larsson & Thomée ↗
Lemma 4.2 · printed p. 45

Download Lean file ↓

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

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

A grid function is bounded by its endpoint values and discrete residual.

|U|_h\le\max\{|U_0|,|U_M|\}+C|A_hU|_{h,\mathrm{int}}.

Assumptions & context

The uniform interval grid and the elliptic difference operator with no first-order term, positive diffusion, and nonnegative reaction.

Source

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

Lemma 4.2 · printed p. 45

02 / LEAN REPRESENTATION

Formal statement

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

theorem lem_4_2 (a b c : ℝ → ℝ)
    (ha_smooth : ∀ n : ℕ, ContDiffOn ℝ n a (Set.Icc (0 : ℝ) 1))
    (hb_smooth : ∀ n : ℕ, ContDiffOn ℝ n b (Set.Icc (0 : ℝ) 1))
    (hc_smooth : ∀ n : ℕ, ContDiffOn ℝ n c (Set.Icc (0 : ℝ) 1))
    (ha_pos : ∀ x ∈ Set.Icc (0 : ℝ) 1, 0 < a x)
    (hc_nonneg : ∀ x ∈ Set.Icc (0 : ℝ) 1, 0 ≤ c x)
    (hb : b = 0) :
    ∃ C : ℝ, ∀ M : ℕ, 1 ≤ M → ∀ U : ℕ → ℝ,
      meshMaxNorm (closedIdx M) U ≤
        max |U 0| |U M| + C * meshMaxNorm (openIdx M) (discreteOp a b c M U) := by
  sorry

Complete Lean file and local definitions

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Lem42

/-- Uniform mesh on Ω̄ = [0,1] with step h = 1/M: x_j = j h, j = 0,…,M. -/
def meshStep (M : ℕ) : ℝ := 1 / (M : ℝ)

def meshPoint (M j : ℕ) : ℝ := (j : ℝ) * meshStep M

/-- The finite difference operator 𝒜_h of (4.3) at an interior index j (1 ≤ j ≤ M-1):
`𝒜_h U_j = -a_j ∂∂̄U_j + b_j ∂̂U_j + c_j U_j`, with the difference quotients written out
so that multiplying by h² gives exactly (4.4). -/
def discreteOp (a b c : ℝ → ℝ) (M : ℕ) (U : ℕ → ℝ) (j : ℕ) : ℝ :=
  c (meshPoint M j) * U j
    - a (meshPoint M j) * ((U (j + 1) - 2 * U j + U (j - 1)) / meshStep M ^ 2)
    + b (meshPoint M j) * ((U (j + 1) - U (j - 1)) / (2 * meshStep M))

/-- Discrete maximum norm (4.7): `|U|_S = max_{x_j ∈ S} |U_j|`, S given by its index set
(the maximum over an empty index set is taken to be 0). -/
def meshMaxNorm (S : Finset ℕ) (U : ℕ → ℝ) : ℝ :=
  ((S.sup fun j => ‖U j‖₊ : NNReal) : ℝ)

/-- Indices j with x_j ∈ Ω̄ = [0,1]: j = 0,…,M. -/
def closedIdx (M : ℕ) : Finset ℕ := Finset.range (M + 1)

/-- Indices j with x_j ∈ Ω = (0,1): j = 1,…,M-1. -/
def openIdx (M : ℕ) : Finset ℕ := Finset.Ioo 0 M

/-- Lemma 4.2 (Larsson–Thomée). Let 𝒜_h be as in (4.3) with b = 0, where a, b, c are smooth on
Ω̄ = [0,1] with a > 0 and c ≥ 0 there (setting of (4.1)). Then there is a constant C, depending
on the coefficients but not on h or U, such that for every mesh h = 1/M and every mesh-function U,
`|U|_{Ω̄} ≤ max{|U_0|, |U_M|} + C |𝒜_h U|_Ω`. -/
theorem lem_4_2 (a b c : ℝ → ℝ)
    (ha_smooth : ∀ n : ℕ, ContDiffOn ℝ n a (Set.Icc (0 : ℝ) 1))
    (hb_smooth : ∀ n : ℕ, ContDiffOn ℝ n b (Set.Icc (0 : ℝ) 1))
    (hc_smooth : ∀ n : ℕ, ContDiffOn ℝ n c (Set.Icc (0 : ℝ) 1))
    (ha_pos : ∀ x ∈ Set.Icc (0 : ℝ) 1, 0 < a x)
    (hc_nonneg : ∀ x ∈ Set.Icc (0 : ℝ) 1, 0 ≤ c x)
    (hb : b = 0) :
    ∃ C : ℝ, ∀ M : ℕ, 1 ≤ M → ∀ U : ℕ → ℝ,
      meshMaxNorm (closedIdx M) U ≤
        max |U 0| |U M| + C * meshMaxNorm (openIdx M) (discreteOp a b c M U) := by
  sorry

end PDETextbook.LarssonThomee.Lem42

How to read the formalization

The residual is measured on interior nodes while the left-hand norm includes the endpoints.

← Back to all statements