FARMSAcceptedLemma · Statement with omitted proof
Boundary attainment for the discrete Poisson maximum principle
For the five-point Laplacian on a square grid, the sign of the discrete Laplacian forces a maximum or minimum to occur on the boundary.
Larsson & Thomée ↗
Lemma 4.3 · printed p. 46
Formal statement. The assumptions and conclusion are explicit; the theorem proof is omitted (sorry).
01 / MATHEMATICAL STATEMENT
Meaning & conditions
Mathematical summary
For the five-point Laplacian on a square grid, the sign of the discrete Laplacian forces a maximum or minimum to occur on the boundary.
Assumptions & context
- A uniform unit-square grid and the corresponding discrete subsolution or supersolution inequality.
Source
Larsson & Thomée. Partial differential equations with numerical methods.
Lemma 4.3 · printed p. 46
02 / LEAN REPRESENTATION
Formal statement
Statement with omitted proof. Expand the complete file below to read imports, local definitions and surrounding context.
theorem discrete_maximum_principle (M : ℕ) (hM : 0 < M) (U : ℤ × ℤ → ℝ) :
((∀ j : ℤ × ℤ,
(0 < j.1 ∧ j.1 < (M : ℤ) ∧ 0 < j.2 ∧ j.2 < (M : ℤ)) →
-discreteLaplacian (1 / (M : ℝ)) U j ≤ 0) →
∃ j : ℤ × ℤ,
(0 ≤ j.1 ∧ j.1 ≤ (M : ℤ) ∧ 0 ≤ j.2 ∧ j.2 ≤ (M : ℤ)) ∧
¬ (0 < j.1 ∧ j.1 < (M : ℤ) ∧ 0 < j.2 ∧ j.2 < (M : ℤ)) ∧
∀ k : ℤ × ℤ,
(0 ≤ k.1 ∧ k.1 ≤ (M : ℤ) ∧ 0 ≤ k.2 ∧ k.2 ≤ (M : ℤ)) → U k ≤ U j) ∧
((∀ j : ℤ × ℤ,
(0 < j.1 ∧ j.1 < (M : ℤ) ∧ 0 < j.2 ∧ j.2 < (M : ℤ)) →
0 ≤ -discreteLaplacian (1 / (M : ℝ)) U j) →
∃ j : ℤ × ℤ,
(0 ≤ j.1 ∧ j.1 ≤ (M : ℤ) ∧ 0 ≤ j.2 ∧ j.2 ≤ (M : ℤ)) ∧
¬ (0 < j.1 ∧ j.1 < (M : ℤ) ∧ 0 < j.2 ∧ j.2 < (M : ℤ)) ∧
∀ k : ℤ × ℤ,
(0 ≤ k.1 ∧ k.1 ≤ (M : ℤ) ∧ 0 ≤ k.2 ∧ k.2 ≤ (M : ℤ)) → U j ≤ U k) := by
sorry
Complete Lean file and local definitions
import PDETextbook.Base
open MeasureTheory
open scoped BigOperators ENNReal
noncomputable section
namespace PDETextbook.LarssonThomee.Lem43
/-- The discrete Laplacian (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²`, where `e_1 = (1,0)`, `e_2 = (0,1)`. -/
def discreteLaplacian (h : ℝ) (U : ℤ × ℤ → ℝ) (j : ℤ × ℤ) : ℝ :=
(U (j.1 + 1, j.2) - 2 * U j + U (j.1 - 1, j.2)) / h ^ 2 +
(U (j.1, j.2 + 1) - 2 * U j + U (j.1, j.2 - 1)) / h ^ 2
/-- Lemma 4.3 (discrete maximum principle), Larsson–Thomée §4.2.
Setting (§4.2): `Ω = (0,1)×(0,1)` with boundary `Γ`. The mesh points are `x_j = jh`
with `j = (j₁, j₂) ∈ ℤ²` and mesh-width `h = 1/M`, and `U` is a real mesh function with `U_j = U(x_j)`.
With `h = 1/M` the mesh-index conditions are as follows.
* `x_j ∈ Ω` iff `0 < j_l < M` for `l = 1,2`.
* `x_j ∈ Ω̄` iff `0 ≤ j_l ≤ M`.
* `x_j ∈ Γ` iff `x_j ∈ Ω̄` and `x_j ∉ Ω`.
If `-Δ_h U_j ≤ 0` for `x_j ∈ Ω`, then the maximum of `U` over the mesh points of `Ω̄`
is attained at some `x_j ∈ Γ`. If `-Δ_h U_j ≥ 0` for `x_j ∈ Ω`, then the minimum is
attained at some `x_j ∈ Γ`. -/
theorem discrete_maximum_principle (M : ℕ) (hM : 0 < M) (U : ℤ × ℤ → ℝ) :
((∀ j : ℤ × ℤ,
(0 < j.1 ∧ j.1 < (M : ℤ) ∧ 0 < j.2 ∧ j.2 < (M : ℤ)) →
-discreteLaplacian (1 / (M : ℝ)) U j ≤ 0) →
∃ j : ℤ × ℤ,
(0 ≤ j.1 ∧ j.1 ≤ (M : ℤ) ∧ 0 ≤ j.2 ∧ j.2 ≤ (M : ℤ)) ∧
¬ (0 < j.1 ∧ j.1 < (M : ℤ) ∧ 0 < j.2 ∧ j.2 < (M : ℤ)) ∧
∀ k : ℤ × ℤ,
(0 ≤ k.1 ∧ k.1 ≤ (M : ℤ) ∧ 0 ≤ k.2 ∧ k.2 ≤ (M : ℤ)) → U k ≤ U j) ∧
((∀ j : ℤ × ℤ,
(0 < j.1 ∧ j.1 < (M : ℤ) ∧ 0 < j.2 ∧ j.2 < (M : ℤ)) →
0 ≤ -discreteLaplacian (1 / (M : ℝ)) U j) →
∃ j : ℤ × ℤ,
(0 ≤ j.1 ∧ j.1 ≤ (M : ℤ) ∧ 0 ≤ j.2 ∧ j.2 ≤ (M : ℤ)) ∧
¬ (0 < j.1 ∧ j.1 < (M : ℤ) ∧ 0 < j.2 ∧ j.2 < (M : ℤ)) ∧
∀ k : ℤ × ℤ,
(0 ≤ k.1 ∧ k.1 ≤ (M : ℤ) ∧ 0 ≤ k.2 ∧ k.2 ≤ (M : ℤ)) → U j ≤ U k) := by
sorry
end PDETextbook.LarssonThomee.Lem43
How to read the formalization
- The conclusion gives a boundary node attaining the extremum, beyond a numerical upper bound alone.