ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generated

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.

One midpoint sample destroys a quadratic stiffness coercivity bound

Example

On the single interval $[0, 1]$ , let $ϕ (x) = x (1 - x)$ and let $V = V_{h} = {span}_{R} {ϕ}$ with inner product $(c ϕ, d ϕ)_{V} : = c d$ and induced norm $∥ c ϕ ∥_{V} = ∣ c ∣$ . Define $a (v, w) = \int_{0}^{1} v^{'} w^{'} d x$ and let $a_{h} (v, w)$ replace that integral by the one-panel midpoint rule. Exact integration gives $a (ϕ, ϕ) = 1 / 3$ , while the midpoint form gives zero. Thus $a$ is bounded and coercive in this one-dimensional Hilbert norm, but $a_{h}$ is not coercive and the first Strang theorem's discrete stability hypothesis fails.

Facts & Assumptions

Given: The interval $[0, 1]$ , the nonzero trial function $ϕ (x) = x (1 - x)$ , the real one-dimensional spaces $V = V_{h} = span {ϕ}$ with $(c ϕ, d ϕ)_{V} = c d$ and $∥ c ϕ ∥_{V} = ∣ c ∣$ , the exact stiffness $a (v, w) = \int_{0}^{1} v^{'} w^{'} d x$ , and its one-panel midpoint approximation $a_{h}$ .

[F1]

Composite midpoint rule on a uniform grid: on one panel of width $1$ , $Q_{M} (g) = g (1 / 2)$ .

[F2]

First Strang estimate for conforming perturbed Galerkin problems: the first Strang estimate assumes a positive discrete coercivity constant $α_{h}$ .

[F3]

The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ and For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term: a polynomial integral is the endpoint difference of an explicit antiderivative.

[F4]

Every finite-dimensional normed space is Banach and Hilbert space: a finite-dimensional real inner-product space is complete and hence Hilbert.

Verification

1.1F3F4givenalgebra

The space $V$ has finite dimension, so [F4] makes it Banach and hence Hilbert for the stated inner product. By the power rule, $ϕ^{'} (x) = 1 - 2 x$ ; the displayed polynomial is an antiderivative of $(1 - 2 x)^{2}$ by the same rule, so [F3] gives $a (ϕ, ϕ) = \int_{0}^{1} (1 - 2 x)^{2} d x = [x - 2 x^{2} + \frac{4}{3} x^{3}]_{0}^{1} = 1 / 3$ . Bilinearity then gives $a (c ϕ, d ϕ) = c d / 3 = \frac{1}{3} (c ϕ, d ϕ)_{V}$ , verifying boundedness and coercivity with constant $1 / 3$ .

2.1F1step 1.1algebra

The midpoint is $1 / 2$ , where $ϕ^{'} (1 / 2) = 0$ . Thus [F1] gives $a_{h} (ϕ, ϕ) = Q_{M} ((ϕ^{'})^{2}) = 0$ , although $ϕ \neq 0$ .

3.1F2givenstep 2.1algebra∎

The stated norm gives $∥ ϕ ∥_{V} = 1$ , so a coercivity constant $α_{h} > 0$ would require $0 = a_{h} (ϕ, ϕ) \geq α_{h}$ , contradicting step 2.1. Therefore the first-Strang stability hypothesis [F2] is absent; the calculation asserts no error rate for the unstable discrete problem.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

42 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

Jean-Luc Guermond, MATH 661 Fall 2025, Part VI, Chapter 27, Error analysis with variational crimes (standard reference, not scraped)
Joachim Schöberl, Numerical Methods for Partial Differential Equations, Chapter 25, Non-conforming Finite Element Methods (standard reference, not scraped)