TheoremStatement: 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.

Second-order grid L2 error for rectangular Dirichlet flux differences

Statement

Let $Ω = (0, L_{x}) \times (0, L_{y})$ , let $a \in C^{3} (\overline{Ω})$ satisfy $a \geq a_{0} > 0$ , and let $u \in C^{4} (\overline{Ω})$ solve $- \partial_{x} (a \partial_{x} u) - \partial_{y} (a \partial_{y} u) = f$ . On each grid from Rectangular grid and Dirichlet flux stencil, impose the exact sampled boundary values $u_{i j}^{*} = u (x_{i}, y_{j})$ and solve $(A_{h}^{a} U_{h})_{i j} = f (x_{i}, y_{j})$ at every interior node. Let $C_{x}, C_{y}$ be the derivative constants of Second-order consistency of the variable-coefficient flux stencil. Then the discrete solution exists uniquely and, with $e_{h} = U_{h} - u^{*}$ ,

∥ e_{h} ∥_{h} \leq \frac{L_{x}^{2}}{a_{0}} \sqrt{L_{x} L_{y}} (2 C_{x} h_{x}^{2} + 2 C_{y} h_{y}^{2}) .

Thus the weighted grid $L^{2}$ error is $O (h_{x}^{2} + h_{y}^{2})$ as both mesh widths tend to zero. This is a pointwise-smooth-solution result; it asserts no error rate for a nonsmooth weak solution.

Facts & Assumptions

Given: $L_{x}, L_{y} > 0$ , $a \in C^{3} (\overline{Ω})$ with $a \geq a_{0} > 0$ , $u \in C^{4} (\overline{Ω})$ satisfying $- \partial_{x} (a \partial_{x} u) - \partial_{y} (a \partial_{y} u) = f$ , and the exact sampled Dirichlet boundary values on every rectangular grid.

[F1]

Rectangular grid and Dirichlet flux stencil: $A_{h}^{a}$ is the negative-divergence operator formed from exact midpoint face coefficients and acts on the interior nodes; $∥ \cdot ∥_{h}$ is the weighted interior grid $L^{2}$ norm.

[F2]

Discrete summation by parts, Poincaré inequality and inverse bound: if every face value is at least $a_{0} > 0$ , the homogeneous Dirichlet matrix is invertible and its inverse has weighted grid $L^{2}$ norm at most $L_{x}^{2} / a_{0}$ .

[F3]

Second-order consistency of the variable-coefficient flux stencil: the sampled exact solution has interior residual bounded pointwise by $2 C_{x} h_{x}^{2} + 2 C_{y} h_{y}^{2}$ .

Proof

1.1givenF1F2algebra

Write $u_{h}^{*} = (u (x_{i}, y_{j}))$ and seek $U_{h} = u_{h}^{*} + e_{h}$ with $e_{h} \in X_{h, 0}$ . The discrete equations are equivalent to $A_{h}^{a} e_{h} = f_{h} - A_{h}^{a} u_{h}^{*}$ on the finite-dimensional zero-boundary space. By [F2], $A_{h}^{a}$ is invertible, so this equation has exactly one solution; hence the Dirichlet scheme has exactly one solution $U_{h}$ .

2.1F1F3step 1.1algebra

Define $τ_{h} = A_{h}^{a} u_{h}^{*} - f_{h}$ . Then the equation for $e_{h}$ is $A_{h}^{a} e_{h} = - τ_{h}$ , and $e_{h} = 0$ at every boundary node because the scheme uses the exact sampled Dirichlet data. By [F3], each interior entry satisfies $∣ τ_{h, i j} ∣ \leq 2 C_{x} h_{x}^{2} + 2 C_{y} h_{y}^{2}$ .

3.1givenF3step 2.1algebra

The weighted sum defining $∥ τ_{h} ∥_{h}^{2}$ has $(N_{x} - 1) (N_{y} - 1)$ terms, so $h_{x} h_{y} (N_{x} - 1) (N_{y} - 1) \leq L_{x} L_{y}$ . Therefore $∥ τ_{h} ∥_{h} \leq \sqrt{L_{x} L_{y}} (2 C_{x} h_{x}^{2} + 2 C_{y} h_{y}^{2})$ .

4.1F2step 2.1step 3.1algebra∎

Apply the inverse estimate [F2] to $A_{h}^{a} e_{h} = - τ_{h}$ and then use step 3.1. This gives the displayed error bound; the derivative constants do not depend on $N_{x}$ or $N_{y}$ , so the error is $O (h_{x}^{2} + h_{y}^{2})$ .

Remarks

No choice axiom is used. The estimates use finite-dimensional coercivity, finite sums, and pointwise Taylor remainders. The published Lax–Milgram and Sobolev–Poincaré pages are continuous-theory context; no continuous weak-solvability theorem is used as a discrete stability result.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · one level

3 results 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 5: Finite Difference Approximation (standard reference, not scraped)
Benjamin Seibold, MIT 18.336 Lecture 6: General Linear Second Order Equation (standard reference, not scraped)