LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Discrete maximum principle and uniform inverse bound for the Dirichlet stencil

Statement

Let $N \geq 1$ , $h = 1 / (N + 1)$ , $x_{j} = j h$ , and $A_{h} = h^{- 2} tridiag (- 1, 2, - 1)$ on the $N$ interior values, with $w_{0} = w_{N + 1} = 0$ , as in Centered finite differences for the zero-Dirichlet boundary-value problem. For $v \in R^{N}$ , define $∥ v ∥_{\infty} : = \max_{1 \leq j \leq N} ∣ v_{j} ∣$ . The Thomas recurrence in that definition has pivots $p_{j} = (j + 1) / j > 0$ and returns the unique solution of $A_{h} U = g_{h}$ for every admissible exact input; neither linear-solve-failure branch is reached. Also, $A_{h}$ is invertible; if $r_{j} \geq 0$ for every $j$ , then $(A_{h}^{- 1} r)_{j} \geq 0$ for every $j$ ; and for every $r \in R^{N}$ ,

∥ A_{h}^{- 1} r ∥_{\infty} \leq \frac{1}{8} ∥ r ∥_{\infty} .

In particular the inverse bound is uniform over all $N \geq 1$ .

Facts & Assumptions

Given: An integer $N \geq 1$ , its mesh $h = 1 / (N + 1)$ , and $r \in R^{N}$ . The endpoints for a vector are fixed at $w_{0} = w_{N + 1} = 0$ .

[F1]

Centered finite differences for the zero-Dirichlet boundary-value problem defines the nodes, matrix, and exact Thomas recurrence: “Set $h = 1 / (N + 1)$ , $x_{j} = j h$ for $0 \leq j \leq N + 1$ ”; “The finite-difference equations are $\frac{- U_{j - 1} + 2 U_{j} - U_{j + 1}}{h^{2}} = g_{j}, 1 \leq j \leq N$ ”; and the forward pivots satisfy $p_{1} = 2$ , $p_{j} = 2 - 1 / p_{j - 1}$ .

Proof

1.1F1inductionalgebra

Let $p_{1} = 2$ and $p_{j} = 2 - 1 / p_{j - 1}$ for $2 \leq j \leq N$ , as in [F1]. Induction gives $p_{j} = (j + 1) / j$ : it holds at $j = 1$ , and if $p_{j - 1} = j / (j - 1)$ then $p_{j} = 2 - (j - 1) / j = (j + 1) / j > 0$ . Thus every Thomas pivot is nonzero.

1.2F1algebra

Define $q_{j} = x_{j} (1 - x_{j}) / 2$ and $q_{0} = q_{N + 1} = 0$ . Direct expansion of this quadratic gives $q_{j - 1} - 2 q_{j} + q_{j + 1} = - h^{2}$ , so $A_{h} q = 1$ . Also $0 \leq q_{j} \leq 1 / 8$ , since $x (1 - x) = 1 / 4 - (x - 1 / 2)^{2}$ on $0 \leq x \leq 1$ .

2.1F1step 1.1algebra

For the equation $A_{h} w = r$ , put $b_{j} = h^{2} r_{j}$ and $s_{1} = b_{1}$ . The first row is $p_{1} w_{1} - w_{2} = s_{1}$ . If elimination has produced $p_{j - 1} w_{j - 1} - w_{j} = s_{j - 1}$ , then $w_{j - 1} = (s_{j - 1} + w_{j}) / p_{j - 1}$ ; substituting this into $- w_{j - 1} + 2 w_{j} - w_{j + 1} = b_{j}$ gives $p_{j} w_{j} - w_{j + 1} = b_{j} + s_{j - 1} / p_{j - 1} = s_{j}$ , exactly the recurrence in [F1].

3.1F1step 1.1step 2.1algebra

Since $w_{N + 1} = 0$ , backward substitution gives $w_{N} = s_{N} / p_{N}$ and then $w_{j} = (s_{j} + w_{j + 1}) / p_{j}$ for $j = N - 1, \dots, 1$ . Each pivot is positive by step 1.1, so each value is uniquely determined; substitution into the transformed rows proves it solves the original rows. Hence for every $r$ there is exactly one $w$ with $A_{h} w = r$ , and $A_{h}^{- 1}$ exists.

4.1givenstep 3.1choosealgebra

Suppose $r_{j} \geq 0$ and let $w = A_{h}^{- 1} r$ . If the finite list $w_{0}, \dots, w_{N + 1}$ had a negative minimum $m$ at an interior index $j$ , then $w_{j - 1}, w_{j + 1} \geq m$ and $h^{2} r_{j} = 2 m - w_{j - 1} - w_{j + 1} \leq 0$ . Since $r_{j} \geq 0$ and $h > 0$ , equality must hold, forcing both neighbors to equal $m$ . Repeating this equality to the left reaches $w_{0} = m < 0$ , contradicting $w_{0} = 0$ . Thus $w_{j} \geq 0$ at every interior index.

5.1givenstep 4.1step 1.2algebra

Put $R = ∥ r ∥_{\infty}$ . The coordinate bounds $- R 1 \leq r \leq R 1$ and step 4.1 show that $A_{h}^{- 1} (R 1 - r) = R q - A_{h}^{- 1} r \geq 0$ and $A_{h}^{- 1} (R 1 + r) = R q + A_{h}^{- 1} r \geq 0$ . Hence $- R q \leq A_{h}^{- 1} r \leq R q$ coordinatewise.

6.1step 1.2step 5.1algebra∎

Step 5.1 and $q_{j} \leq 1 / 8$ from step 1.2 give $∣ (A_{h}^{- 1} r)_{j} ∣ \leq R / 8$ for every $j$ , so $∥ A_{h}^{- 1} r ∥_{\infty} \leq ∥ r ∥_{\infty} / 8$ for every mesh.

Depends on

Centered finite differences for the zero-Dirichlet boundary-value problem

Used by

Dependency tree · one level

1 result within one dependency step of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Tobin A. Driscoll and Richard J. Braun, Fundamentals of Numerical Computation, author-source revision 2025.01.27, Chapter 10, linear.md (standard reference, not scraped)
Benjamin Seibold, MIT OpenCourseWare 18.336, Lecture 5: Finite Difference Approximation, Spring 2009 (standard reference, not scraped)
Benjamin Seibold, MIT OpenCourseWare 18.336, Lecture 6: General Linear Second Order Equation, Spring 2009 (standard reference, not scraped)