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.

A finite-grid Poincare inequality for zero endpoint values

Statement

Let $N \geq 2$ , $h > 0$ , $L = N h$ , and let $w = (w_{0}, \dots, w_{N})$ be a complex grid function with $w_{0} = w_{N} = 0$ . Then $∥ w ∥_{h} \leq L ∥ D_{+} w ∥_{e, h} .$

Facts & Assumptions

Given: A complex grid function $w$ on $j = 0, \dots, N$ with zero endpoint values.

[F1]

The weighted interior and edge norms are those of Uniform periodic, infinite, and Dirichlet grid conventions.

Proof

1.1givenF1algebra

For each $1 \leq j \leq N - 1$ , put $d_{i} = w_{i + 1} - w_{i}$ for $i = 0, \dots, j - 1$ . Expanding both expressions shows $j \sum_{i = 0}^{j - 1} ∣ d_{i} ∣^{2} - {∣ \sum_{i = 0}^{j - 1} d_{i} ∣}^{2} = \sum_{0 \leq i < r < j} ∣ d_{i} - d_{r} ∣^{2},$ since each side equals $(j - 1) \sum_{i} ∣ d_{i} ∣^{2} - \sum_{i < r} (d_{i} \overline{d_{r}} + d_{r} \overline{d_{i}})$ . The right side is nonnegative. Since $w_{0} = 0$ , $w_{j} = \sum_{i = 0}^{j - 1} d_{i}$ , so $∣ w_{j} ∣^{2} \leq j \sum_{i = 0}^{j - 1} ∣ w_{i + 1} - w_{i} ∣^{2} \leq N \sum_{i = 0}^{N - 1} ∣ w_{i + 1} - w_{i} ∣^{2} .$

2.1step 1.1F1algebra∎

Sum the step 1.1 bound over $j = 1, \dots, N - 1$ and multiply by $h$ . Since $(N - 1) N h \leq N^{2} h$ and $∥ D_{+} w ∥_{e, h}^{2} = h^{- 1} \sum_{i = 0}^{N - 1} ∣ w_{i + 1} - w_{i} ∣^{2}$ , we obtain $∥ w ∥_{h}^{2} \leq N^{2} h^{2} ∥ D_{+} w ∥_{e, h}^{2} = L^{2} ∥ D_{+} w ∥_{e, h}^{2}$ . Taking nonnegative square roots proves the claim.

Depends on

Uniform periodic, infinite, and Dirichlet grid conventions

Used by

Coercive discrete energy for the Dirichlet leapfrog wave scheme Theorem

Dependency tree · two levels

5 results within two dependency steps 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, B6.1 Numerical Solution of Partial Differential Equations (standard reference, not scraped)