AcceptedLemma · Statement with omitted proof

A discrete maximum principle on an interval

A sign condition on a finite-difference operator controls grid extrema by endpoint values.

Larsson & Thomée ↗
Lemma 4.1 · printed p. 44

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 sign condition on a finite-difference operator controls grid extrema by endpoint values.

A_hU\le0\quad\Longrightarrow\quad \max_jU_j\le\max\{U_0,U_M,0\}.

Assumptions & context

A uniform mesh on the unit interval, positive diffusion, nonnegative reaction, and the coefficient restrictions $a_j\pm hb_j/2\ge0$ .

Source

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

Lemma 4.1 · printed p. 44

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_1 (a b c : ℝ → ℝ) (M : ℕ) (hM : 1 ≤ M)
    (ha_smooth : ContDiffOn ℝ (⊤ : ℕ∞) a (Set.Icc (0 : ℝ) 1))
    (hb_smooth : ContDiffOn ℝ (⊤ : ℕ∞) b (Set.Icc (0 : ℝ) 1))
    (hc_smooth : ContDiffOn ℝ (⊤ : ℕ∞) 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)
    (hsmall : ∀ j : ℕ, 1 ≤ j → j ≤ M - 1 →
      0 ≤ a (meshPt M j) + (1 / 2) * meshWidth M * b (meshPt M j) ∧
      0 ≤ a (meshPt M j) - (1 / 2) * meshWidth M * b (meshPt M j))
    (U : ℕ → ℝ) :
    ((∀ j : ℕ, 1 ≤ j → j ≤ M - 1 → Ah a b c M U j ≤ 0) →
      ((∀ x ∈ Set.Icc (0 : ℝ) 1, c x = 0) →
          (Finset.range (M + 1)).sup' (range_succ_nonempty M) U = max (U 0) (U M)) ∧
        (Finset.range (M + 1)).sup' (range_succ_nonempty M) U ≤ max (max (U 0) (U M)) 0) ∧
    ((∀ j : ℕ, 1 ≤ j → j ≤ M - 1 → 0 ≤ Ah a b c M U j) →
      ((∀ x ∈ Set.Icc (0 : ℝ) 1, c x = 0) →
          (Finset.range (M + 1)).inf' (range_succ_nonempty M) U = min (U 0) (U M)) ∧
        min (min (U 0) (U M)) 0 ≤ (Finset.range (M + 1)).inf' (range_succ_nonempty M) U) := by
  sorry

Complete Lean file and local definitions

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Lem41

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

/-- Meshpoints `x_j = j h`, `j = 0, …, M`. -/
def meshPt (M : ℕ) (j : ℕ) : ℝ := (j : ℝ) * meshWidth M

/-- Second difference quotient `∂∂̄ U_j = (U_{j+1} - 2U_j + U_{j-1}) / h^2`. -/
def secondDiff (M : ℕ) (U : ℕ → ℝ) (j : ℕ) : ℝ :=
  (U (j + 1) - 2 * U j + U (j - 1)) / (meshWidth M) ^ 2

/-- Centered difference quotient `∂̂ U_j = (U_{j+1} - U_{j-1}) / (2h)`. -/
def centeredDiff (M : ℕ) (U : ℕ → ℝ) (j : ℕ) : ℝ :=
  (U (j + 1) - U (j - 1)) / (2 * meshWidth M)

/-- The finite difference operator of (4.3):
`𝒜_h U_j = -a_j ∂∂̄U_j + b_j ∂̂U_j + c_j U_j`, with `a_j = a(x_j)` etc.
It is used only at interior indices `j = 1, …, M-1`. -/
def Ah (a b c : ℝ → ℝ) (M : ℕ) (U : ℕ → ℝ) (j : ℕ) : ℝ :=
  -(a (meshPt M j)) * secondDiff M U j + b (meshPt M j) * centeredDiff M U j
    + c (meshPt M j) * U j

/-- The index set `{0, …, M}` is nonempty. -/
theorem range_succ_nonempty (M : ℕ) : (Finset.range (M + 1)).Nonempty :=
  ⟨0, Finset.mem_range.mpr (Nat.succ_pos M)⟩

/-- Lemma 4.1 (discrete maximum principle). Standing assumptions of (4.1): `a, b, c` smooth on
`[0,1]`, `a > 0`, `c ≥ 0` there. The mesh `0 = x_0 < ⋯ < x_M = 1` forces `M ≥ 1`.
The grid function `U` is `U_0, …, U_M` (values at other indices are unused).
First conjunct: the version with `𝒜_h U_j ≤ 0` and maxima; second conjunct: the parenthetical
version with `𝒜_h U_j ≥ 0` and minima. -/
theorem lem_4_1 (a b c : ℝ → ℝ) (M : ℕ) (hM : 1 ≤ M)
    (ha_smooth : ContDiffOn ℝ (⊤ : ℕ∞) a (Set.Icc (0 : ℝ) 1))
    (hb_smooth : ContDiffOn ℝ (⊤ : ℕ∞) b (Set.Icc (0 : ℝ) 1))
    (hc_smooth : ContDiffOn ℝ (⊤ : ℕ∞) 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)
    (hsmall : ∀ j : ℕ, 1 ≤ j → j ≤ M - 1 →
      0 ≤ a (meshPt M j) + (1 / 2) * meshWidth M * b (meshPt M j) ∧
      0 ≤ a (meshPt M j) - (1 / 2) * meshWidth M * b (meshPt M j))
    (U : ℕ → ℝ) :
    ((∀ j : ℕ, 1 ≤ j → j ≤ M - 1 → Ah a b c M U j ≤ 0) →
      ((∀ x ∈ Set.Icc (0 : ℝ) 1, c x = 0) →
          (Finset.range (M + 1)).sup' (range_succ_nonempty M) U = max (U 0) (U M)) ∧
        (Finset.range (M + 1)).sup' (range_succ_nonempty M) U ≤ max (max (U 0) (U M)) 0) ∧
    ((∀ j : ℕ, 1 ≤ j → j ≤ M - 1 → 0 ≤ Ah a b c M U j) →
      ((∀ x ∈ Set.Icc (0 : ℝ) 1, c x = 0) →
          (Finset.range (M + 1)).inf' (range_succ_nonempty M) U = min (U 0) (U M)) ∧
        min (min (U 0) (U M)) 0 ≤ (Finset.range (M + 1)).inf' (range_succ_nonempty M) U) := by
  sorry

end PDETextbook.LarssonThomee.Lem41

How to read the formalization

The declaration contains maximum and minimum versions, including sharper endpoint equalities when the reaction term vanishes.

← Back to all statements