LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedprecheck pass

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 summation by parts, Poincaré inequality and inverse bound

Statement

On the grid of Rectangular grid and Dirichlet flux stencil, put $q_{i + 1 / 2, j}^{x} = a_{i + 1 / 2, j} D_{x} v_{i + 1 / 2, j}$ and $q_{i, j + 1 / 2}^{y} = a_{i, j + 1 / 2} D_{y} v_{i, j + 1 / 2}$ . For any grid functions $v, w$ ,

⟨ A_{h}^{a} v, w ⟩_{h} = E_{h}^{a} (v, w) - h_{y} \sum_{j = 1}^{N_{y} - 1} (q_{N_{x} - 1 / 2, j}^{x} w_{N_{x}, j} - q_{1 / 2, j}^{x} w_{0, j}) - h_{x} \sum_{i = 1}^{N_{x} - 1} (q_{i, N_{y} - 1 / 2}^{y} w_{i, N_{y}} - q_{i, 1 / 2}^{y} w_{i, 0}) .

In particular, if $w$ vanishes on the boundary, then $⟨ A_{h}^{a} v, w ⟩_{h} = E_{h}^{a} (v, w)$ . For every $v \in X_{h, 0}$ ,

∥ v ∥_{h}^{2} \leq L_{x}^{2} h_{x} h_{y} \sum_{j = 1}^{N_{y} - 1} \sum_{i = 0}^{N_{x} - 1} ∣ D_{x} v_{i + 1 / 2, j} ∣^{2} .

If all horizontal and vertical face values satisfy $a_{i + 1 / 2, j}, a_{i, j + 1 / 2} \geq a_{0} > 0$ , then the homogeneous Dirichlet matrix $A_{h}^{a}$ is invertible and

∥ (A_{h}^{a})^{- 1} ∥_{ℓ_{h}^{2} \to ℓ_{h}^{2}} \leq \frac{L_{x}^{2}}{a_{0}},

where $ℓ_{h}^{2}$ is the norm $∥ \cdot ∥_{h}$ on interior vectors. The constants are independent of $N_{x}, N_{y}$ .

Facts & Assumptions

Given: $L_{x}, L_{y} > 0$ , integers $N_{x}, N_{y} \geq 2$ , the grid, its real grid functions, the inner product, the flux operator $A_{h}^{a}$ , and edge energy $E_{h}^{a}$ defined in Rectangular grid and Dirichlet flux stencil.

[F1]

Rectangular grid and Dirichlet flux stencil: $A_{h}^{a}$ is the negative horizontal and vertical flux divergence; $E_{h}^{a}$ is the weighted sum of the horizontal and vertical edge-gradient products; $X_{h, 0}$ consists of grid functions vanishing on every boundary node.

Proof

1.1givenF1algebra

Fix an interior row $j$ and write $q_{i} = q_{i + 1 / 2, j}^{x}$ . Telescoping the horizontal contribution gives $h_{x} h_{y} \sum_{i = 1}^{N_{x} - 1} - (q_{i} - q_{i - 1}) w_{i j} / h_{x} = h_{y} \sum_{i = 0}^{N_{x} - 1} q_{i} (w_{i + 1, j} - w_{i j}) - h_{y} (q_{N_{x} - 1 / 2, j}^{x} w_{N_{x}, j} - q_{1 / 2, j}^{x} w_{0, j})$ . Summing this identity over $j$ gives the horizontal energy and its two boundary terms.

1.2givenF1algebra

Let $v \in X_{h, 0}$ . For each interior row, $v_{i j} = \sum_{k = 0}^{i - 1} h_{x} D_{x} v_{k + 1 / 2, j}$ . Cauchy–Schwarz gives $∣ v_{i j} ∣^{2} \leq (i h_{x}) \sum_{k = 0}^{i - 1} h_{x} ∣ D_{x} v_{k + 1 / 2, j} ∣^{2} \leq L_{x} \sum_{k = 0}^{N_{x} - 1} h_{x} ∣ D_{x} v_{k + 1 / 2, j} ∣^{2}$ . Summing with weights $h_{x} h_{y}$ and using $\sum_{i = 1}^{N_{x} - 1} h_{x} < L_{x}$ proves the displayed discrete Poincaré inequality.

2.1F1step 1.1algebra

Applying the same telescoping sum in each column to the vertical flux gives the vertical energy minus the top and bottom boundary terms. Adding it to step 1.1 proves the displayed two-dimensional identity, with all four boundary contributions present.

3.1step 2.1givenalgebra

If $w$ vanishes at every boundary node, both boundary sums in step 2.1 are zero, so $⟨ A_{h}^{a} v, w ⟩_{h} = E_{h}^{a} (v, w)$ .

4.1F1step 3.1step 1.2algebra

Apply step 3.1 with $w = v$ . The face lower bound gives $E_{h}^{a} (v, v) \geq a_{0} h_{x} h_{y} \sum_{j, i} ∣ D_{x} v_{i + 1 / 2, j} ∣^{2} \geq (a_{0} / L_{x}^{2}) ∥ v ∥_{h}^{2}$ by step 1.2.

5.1step 4.1algebra

If $A_{h}^{a} v = 0$ for $v \in X_{h, 0}$ , step 4.1 forces $∥ v ∥_{h} = 0$ , hence every interior value is zero; the boundary values already vanish, so $v = 0$ . Thus the square finite-dimensional matrix is injective and therefore invertible.

6.1step 3.1step 4.1step 5.1algebra∎

For $A_{h}^{a} v = f_{h}$ , steps 3.1 and 4.1 imply $(a_{0} / L_{x}^{2}) ∥ v ∥_{h}^{2} \leq ⟨ f_{h}, v ⟩_{h} \leq ∥ f_{h} ∥_{h} ∥ v ∥_{h}$ . If $v = 0$ the claimed estimate is immediate; otherwise divide by $∥ v ∥_{h}$ to obtain $∥ v ∥_{h} \leq (L_{x}^{2} / a_{0}) ∥ f_{h} ∥_{h}$ , which is the asserted inverse-operator bound.

Remarks

No choice axiom is used: the proof uses finite sums, Cauchy–Schwarz, and finite-dimensional injectivity implying surjectivity.

Depends on

Rectangular grid and Dirichlet flux stencil

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

Endre Süli, Numerical Solution of PDEs, complete lecture notes (standard reference, not scraped)
Benjamin Seibold, MIT 18.336 Lecture 6: General Linear Second Order Equation (standard reference, not scraped)