LemmaStatement: Literature-sourcedProof: 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.

Midpoint quadrature defect for one-dimensional P1 stiffness

Statement

Assume Countable Choice. Let $0 = x_{0} < \dots < x_{N} = 1$ be a finite partition with cells $K = [x_{j - 1}, x_{j}]$ , cell lengths $h_{K}$ , and maximum $h$ . Let $A \in C^{2} ([0, 1])$ , and let $v_{h}, w_{h}$ be continuous piecewise-linear functions. Write $v_{K}^{'}, w_{K}^{'}$ for their constant cell slopes and take their a.e. derivatives as $L^{2}$ representatives. Define the exact and midpoint stiffness forms by

$a (v_{h}, w_{h}) : = \int_{(0, 1)} A (x) v_{h}^{'} (x) w_{h}^{'} (x) d λ_{1} (x), a_{h} (v_{h}, w_{h}) : = \sum_{K} h_{K} A (m_{K}) v_{K}^{'} w_{K}^{'},$

where $m_{K}$ is the cell midpoint and the cell derivatives are constant. Then

$∣ a (v_{h}, w_{h}) - a_{h} (v_{h}, w_{h}) ∣ \leq \frac{h^{2}}{24} ∥ A^{''} ∥_{L^{\infty} (0, 1)} ∥ v_{h}^{'} ∥_{L^{2} (0, 1)} ∥ w_{h}^{'} ∥_{L^{2} (0, 1)} .$

Moreover, $∥ v_{h}^{'} ∥_{L^{2} (0, 1)}^{2} = \sum_{K} h_{K} ∣ v_{K}^{'} ∣^{2}$ , and likewise for $w_{h}^{'}$ .

The midpoint rule is exact for this stiffness integrand when $A$ is affine; for a general $C^{2}$ coefficient the displayed defect is retained. The bound is exact-arithmetic quadrature error, separate from roundoff.

Facts & Assumptions

Given: Countable Choice, the finite partition, $A \in C^{2} ([0, 1])$ , and continuous piecewise-linear $v_{h}, w_{h}$ .

[F1]

Composite midpoint rule on a uniform grid: on one cell $K$ , the midpoint value times $h_{K}$ is the one-panel midpoint quadrature rule.

[F2]

Composite midpoint error bound for a twice continuously differentiable function: for $g \in C^{2} (K)$ , the one-panel error is at most $h_{K}^{3} ∥ g^{''} ∥_{L^{\infty} (K)} / 24$ .

[F3]

For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ : the integral over $[0, 1]$ is the sum of cell integrals.

[F4]

Triangle inequality for finite sums: the absolute value of the sum of cell errors is bounded by their absolute values' sum.

[F5]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: the sum of products of two finite real lists is bounded by the product of their Euclidean norms.

[F6]

Extreme value theorem: a continuous real function on a nonempty compact subset of $R$ attains a greatest and a least value: the continuous function $∣ A^{''} ∣$ attains a finite maximum on $[0, 1]$ . Because every relative interval has positive Lebesgue measure by [F8], this maximum is its essential supremum (The essential supremum of a measurable function with respect to a measure, The space $L^{\infty} (μ)$ of essentially bounded measurable functions).

[F7]

The $L^{2}$ norm is the square root of the integral of the square (The function space $L^{p} (μ)$ for $0 < p < \infty$ , The space $L^{p} (μ)$ as the quotient by null functions). A finite-valued measurable function has simple integral $\sum_{j} c_{j} λ_{1} (E_{j})$ (Nonnegative simple measurable functions, The integral of a nonnegative simple function), and its nonnegative Lebesgue integral agrees with that value (The nonnegative integral agrees with the simple integral on simple functions).

[F8]

Under Countable Choice, every interval in $[0, 1]$ has Lebesgue measure equal to its length; in particular each open cell $K^{\circ} = (x_{j - 1}, x_{j})$ has measure $h_{K}$ and each mesh node is null (A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F9]

Under Countable Choice, a bounded Riemann-integrable function on $[0, 1]$ has the same Riemann and Lebesgue integrals (A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F10]

A continuous function on a closed interval is Riemann integrable, and changing its values at finitely many points preserves its integral (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, Changing an integrable function at finitely many points changes neither its integrability nor its integral).

Proof

1.1givenF7F8construct

For each cell, define $g_{v} = v_{K}^{'}$ and $g_{w} = w_{K}^{'}$ on $K^{\circ}$ , and set both representatives to $0$ at the finitely many mesh nodes. Their squares are nonnegative simple functions. By [F7] and [F8], $∥ v_{h}^{'} ∥_{2}^{2} = \sum_{K} ∣ v_{K}^{'} ∣^{2} λ_{1} (K^{\circ}) = \sum_{K} h_{K} ∣ v_{K}^{'} ∣^{2}$ , and the same identity holds for $w_{h}^{'}$ and for the cell-restricted norms.

1.2givenF1F2construct

On a cell $K$ , $v_{K}^{'}$ and $w_{K}^{'}$ are constants, so $g_{K} (x) : = A (x) v_{K}^{'} w_{K}^{'}$ is $C^{2}$ ; the discrete sample is the one-panel midpoint rule [F1]. Also $∥ g_{K}^{''} ∥_{\infty} \leq ∥ A^{''} ∥_{\infty} ∣ v_{K}^{'} ∣ ∣ w_{K}^{'} ∣$ . Applying [F2] with $n = 1$ bounds the cell error by $h_{K}^{3} ∥ A^{''} ∥_{\infty} ∣ v_{K}^{'} ∣ ∣ w_{K}^{'} ∣ / 24$ .

2.1step 1.1step 1.2algebra

By step 1.1, the cell error in step 1.2 is at most $h_{K}^{2} ∥ A^{''} ∥_{\infty} ∥ v_{h}^{'} ∥_{L^{2} (K)} ∥ w_{h}^{'} ∥_{L^{2} (K)} / 24$ .

3.1F3F4F5F6F8F9F10step 1.1step 2.1algebra∎

The global integrand $A v_{h}^{'} w_{h}^{'}$ is bounded. On each cell its representative differs at most at the endpoints from the continuous function $g_{K} (x) = A (x) v_{K}^{'} w_{K}^{'}$ , so [F10] makes each cell restriction Riemann integrable with the same cell integral as $g_{K}$ . Repeated application of [F3] then makes the global integrand Riemann integrable and expresses its integral as the sum of the cell integrals. By [F9], its Lebesgue integral on $[0, 1]$ equals this Riemann integral; the endpoints are null by [F8], so this is also $a (v_{h}, w_{h})$ . Thus $a (v_{h}, w_{h}) - a_{h} (v_{h}, w_{h})$ is the sum of the cell errors. The finite-sum triangle inequality [F4] and step 2.1 bound its absolute value by $h^{2} ∥ A^{''} ∥_{\infty} / 24$ times $\sum_{K} ∥ v_{h}^{'} ∥_{L^{2} (K)} ∥ w_{h}^{'} ∥_{L^{2} (K)}$ . Cauchy–Schwarz [F5] and the norm decompositions in step 1.1 give the displayed global estimate.

Depends on

Used by

A midpoint-quadrature P1 solve has an explicit Strang error budget Corollary

Dependency tree · two levels

100 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

Art B. Owen, Monte Carlo Theory, Methods and Examples, Chapter 7, Theorem 7.1 (standard reference, not scraped)
Tobin A. Driscoll and Richard J. Braun, Fundamentals of Numerical Computation, §5.6 Numerical Integration (standard reference, not scraped)