AcceptedTheorem · Statement with omitted proof

Second-order error for an elliptic difference scheme

The one-dimensional finite-difference solution approximates a smooth elliptic solution with second-order accuracy in the grid maximum norm.

Larsson & Thomée ↗
Theorem 4.1 · 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

The one-dimensional finite-difference solution approximates a smooth elliptic solution with second-order accuracy in the grid maximum norm.

\max_j|U_j-u(x_j)|\le Ch^2\|u\|_{C^4([0,1])}.

Assumptions & context

No first-order term, smooth positive diffusion and nonnegative reaction, a four-times continuously differentiable solution, and matching discrete boundary data.

Source

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

Theorem 4.1 · 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 thm_4_1 (a c : ℝ → ℝ)
    (ha : SmoothOnClosure a) (hc : SmoothOnClosure c)
    (ha_pos : ∀ x ∈ Set.Icc (0 : ℝ) 1, 0 < a x)
    (hc_nonneg : ∀ x ∈ Set.Icc (0 : ℝ) 1, 0 ≤ c x) :
    ∃ C : ℝ, ∀ M : ℕ, 0 < M →
      ∀ (f : ℝ → ℝ) (u0 u1 : ℝ) (u : ℝ → ℝ) (U : ℕ → ℝ),
        ContDiffOn ℝ 4 u (Set.Icc (0 : ℝ) 1) →
        IsBVPSolution a c f u0 u1 u →
        IsFDSolution a c f u0 u1 M U →
        meshMaxNormOmega M (fun j => U j - u (meshPoint M j))
          ≤ C * (meshWidth M) ^ 2 * c4Norm u := by
  sorry

Complete Lean file and local definitions

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm41

/-- Smoothness of a coefficient on the closed interval `Ω̄ = [0,1]`, meaning `C^n` for every `n`. -/
def SmoothOnClosure (g : ℝ → ℝ) : Prop :=
  ∀ n : ℕ, ContDiffOn ℝ n g (Set.Icc (0 : ℝ) 1)

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

/-- Mesh points `x_j = j h = j / M`, `j = 0, …, M`. -/
def meshPoint (M j : ℕ) : ℝ := (j : ℝ) / (M : ℝ)

/-- Classical solution of (4.1) with `b = 0`:
`-a u'' + c u = f` in `Ω = (0,1)`, `u(0) = u₀`, `u(1) = u₁`. -/
def IsBVPSolution (a c f : ℝ → ℝ) (u0 u1 : ℝ) (u : ℝ → ℝ) : Prop :=
  (∀ x ∈ Set.Ioo (0 : ℝ) 1, -(a x * deriv (deriv u) x) + c x * u x = f x) ∧
  u 0 = u0 ∧ u 1 = u1

/-- Forward difference quotient `∂U_j = (U_{j+1} - U_j)/h`. -/
def fwdDiff (h : ℝ) (U : ℕ → ℝ) (j : ℕ) : ℝ := (U (j + 1) - U j) / h

/-- Backward difference quotient `∂̄U_j = (U_j - U_{j-1})/h`. It is used only for `j ≥ 1`. -/
def bwdDiff (h : ℝ) (U : ℕ → ℝ) (j : ℕ) : ℝ := (U j - U (j - 1)) / h

/-- Finite difference scheme (4.3) with `b = 0`:
`-a_j ∂∂̄U_j + c_j U_j = f_j` for `j = 1, …, M-1`, with `U_0 = u₀` and `U_M = u₁`.
The coefficients are `a_j = a(x_j)`, `c_j = c(x_j)` and `f_j = f(x_j)`. -/
def IsFDSolution (a c f : ℝ → ℝ) (u0 u1 : ℝ) (M : ℕ) (U : ℕ → ℝ) : Prop :=
  (∀ j : ℕ, 1 ≤ j → j ≤ M - 1 →
    -(a (meshPoint M j) * fwdDiff (meshWidth M) (bwdDiff (meshWidth M) U) j)
      + c (meshPoint M j) * U j = f (meshPoint M j)) ∧
  U 0 = u0 ∧ U M = u1

/-- Discrete maximum norm (4.7) over `S = Ω = (0,1)`:
`|V|_Ω = max_{x_j ∈ Ω} |V_j|`. Here `x_j ∈ (0,1)` holds iff `0 < j < M`. -/
def meshMaxNormOmega (M : ℕ) (V : ℕ → ℝ) : ℝ :=
  NNReal.toReal ((Finset.Ioo 0 M).sup fun j => ‖V j‖₊)

/-- `‖u‖_{C⁴}` on `Ω̄ = [0,1]`: the maximum over orders `k ≤ 4` of `sup_{x ∈ [0,1]} |u^{(k)}(x)|`. -/
def c4Norm (u : ℝ → ℝ) : ℝ :=
  ⨆ k : Fin 5, ⨆ x : Set.Icc (0 : ℝ) 1,
    |iteratedDerivWithin (k : ℕ) u (Set.Icc (0 : ℝ) 1) x|

/-- Theorem 4.1 (Larsson–Thomée). Let `b = 0`, and let `U` and `u` be the solutions of (4.3) and (4.1).
Then `|U - u|_Ω ≤ C h² ‖u‖_{C⁴}`. The constant `C` depends only on the data `a` and `c`.
It is uniform in the mesh `M` (`h = 1/M`), in `f`, in `u₀, u₁` and in the solutions. -/
theorem thm_4_1 (a c : ℝ → ℝ)
    (ha : SmoothOnClosure a) (hc : SmoothOnClosure c)
    (ha_pos : ∀ x ∈ Set.Icc (0 : ℝ) 1, 0 < a x)
    (hc_nonneg : ∀ x ∈ Set.Icc (0 : ℝ) 1, 0 ≤ c x) :
    ∃ C : ℝ, ∀ M : ℕ, 0 < M →
      ∀ (f : ℝ → ℝ) (u0 u1 : ℝ) (u : ℝ → ℝ) (U : ℕ → ℝ),
        ContDiffOn ℝ 4 u (Set.Icc (0 : ℝ) 1) →
        IsBVPSolution a c f u0 u1 u →
        IsFDSolution a c f u0 u1 M U →
        meshMaxNormOmega M (fun j => U j - u (meshPoint M j))
          ≤ C * (meshWidth M) ^ 2 * c4Norm u := by
  sorry

end PDETextbook.LarssonThomee.Thm41

How to read the formalization

The mesh-independent constant is quantified before the mesh and problem data.

← Back to all statements