AcceptedLemma · Statement with omitted proof

Maximum-norm stability of the five-point Laplacian

The maximum size of a square-grid function is controlled by its boundary values and discrete Laplacian.

Larsson & Thomée ↗
Lemma 4.4 · printed p. 47

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 maximum size of a square-grid function is controlled by its boundary values and discrete Laplacian.

|U|_h\le |U|_{\partial h}+C|\Delta_hU|_{\mathrm{int}}.

Assumptions & context

The uniform unit-square grid and the standard five-point difference operator.

Source

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

Lemma 4.4 · printed p. 47

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_4 :
    ∃ C : ℝ, ∀ M : ℕ, 0 < M → ∀ U : ℤ × ℤ → ℝ,
      meshMaxNorm (closedMesh M) U ≤
        meshMaxNorm (boundaryMesh M) U +
          C * meshMaxNorm (interiorMesh M) (discreteLaplacian M U) := by
  sorry

Complete Lean file and local definitions

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Lem44

/-- Mesh-width `h = 1/M` (Section 4.2). -/
def meshWidth (M : ℕ) : ℝ := 1 / (M : ℝ)

/-- Indices `j = (j₁, j₂)` with mesh-point `x_j = j h` in the closed unit square `Ω̄ = [0,1]²`,
i.e. `0 ≤ j_l ≤ M`. -/
def closedMesh (M : ℕ) : Finset (ℤ × ℤ) :=
  Finset.Icc (0 : ℤ) M ×ˢ Finset.Icc (0 : ℤ) M

/-- Indices with `x_j ∈ Ω = (0,1)²`, i.e. `0 < j_l < M` (interior mesh-points). -/
def interiorMesh (M : ℕ) : Finset (ℤ × ℤ) :=
  Finset.Ioo (0 : ℤ) M ×ˢ Finset.Ioo (0 : ℤ) M

/-- Indices with `x_j ∈ Γ = ∂Ω`, i.e. mesh-points of `Ω̄` not in `Ω`. -/
def boundaryMesh (M : ℕ) : Finset (ℤ × ℤ) :=
  closedMesh M \ interiorMesh M

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

/-- The 5-point discrete Laplacian of (4.10)–(4.11):
`Δ_h U_j = ∂₁∂̄₁ U_j + ∂₂∂̄₂ U_j`, with
`∂_l∂̄_l U_j = (U_{j+e_l} - 2U_j + U_{j-e_l}) / h²`. -/
def discreteLaplacian (M : ℕ) (U : ℤ × ℤ → ℝ) (j : ℤ × ℤ) : ℝ :=
  (U (j + (1, 0)) - 2 * U j + U (j - (1, 0))) / (meshWidth M) ^ 2 +
  (U (j + (0, 1)) - 2 * U j + U (j - (0, 1))) / (meshWidth M) ^ 2

/-- Lemma 4.4 (Larsson–Thomée). With `Δ_h` defined in (4.11), for any mesh-function `U`,
`|U|_{Ω̄} ≤ |U|_Γ + C |Δ_h U|_Ω`, where `Ω = (0,1)²`, `h = 1/M`, and the constant `C`
is independent of the mesh-function `U` and of the mesh-width `h`. -/
theorem lem_4_4 :
    ∃ C : ℝ, ∀ M : ℕ, 0 < M → ∀ U : ℤ × ℤ → ℝ,
      meshMaxNorm (closedMesh M) U ≤
        meshMaxNorm (boundaryMesh M) U +
          C * meshMaxNorm (interiorMesh M) (discreteLaplacian M U) := by
  sorry

end PDETextbook.LarssonThomee.Lem44

How to read the formalization

The stability constant is independent of the mesh width and of the grid function.

← Back to all statements