TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Gaussian quadrature has the Hermite mean-value remainder

Statement

Let $(a, b, m, 2 m, μ)$ be moment data as in Positive-measure Gaussian quadrature moment data, let $Q_{m}$ be its Gaussian rule, and let $f \in C^{2 m} ([a, b], R)$ . Then there is $ξ \in (a, b)$ such that $\int_{[a, b]} f (x) d μ (x) - Q_{m} (f) = \frac{f^{(2 m)} (ξ)}{(2 m)!_{R}} \int_{[a, b]} p_{m} (x)^{2} d μ (x),$ where $p_{m} (X) = \prod_{i = 1}^{m} (X - x_{i})$ is the monic node polynomial and $(2 m)!_{R} : = \prod_{j = 1}^{2 m} j$ .

Facts & Assumptions

Given: Moment data of order $2 m$ , its Gaussian rule, and a real function $f \in C^{2 m} ([a, b])$ .

[F1]

Positive-measure Gaussian quadrature moment data: $μ$ is finite and positive, its support contains at least $m + 1$ points, and moments through degree $2 m$ are finite.

[F2]

The m-node Gaussian quadrature rule for a positive measure and Gaussian quadrature is exact through degree 2m−1 and has positive weights: $Q_{m}$ is the finite Gaussian rule, is exact through degree $2 m - 1$ , and its nodes are the roots of $p_{m}$ .

[F3]

Double-node Hermite interpolation has the stated pointwise remainder: for the nodes $x_{i}$ , the explicit polynomial $H$ has degree at most $2 m - 1$ , matches $f, f^{'}$ at the nodes, and for every non-node $x$ the pointwise remainder is $f (x) - H (x) = p_{m} (x)^{2} f^{(2 m)} (ξ_{x}) / (2 m)!_{R}$ for some $ξ_{x} \in (a, b)$ .

[F4]

The polynomial moment pairing is a real inner product: since $r = 2 m$ , $\int p_{m}^{2} d μ$ is finite and strictly positive.

[F5]

Extreme value theorem: a continuous real function on a nonempty compact subset of $R$ attains a greatest and a least value and The image of an interval under a continuous real function is order-convex, hence an interval, and the image of a closed bounded interval is a closed bounded interval: a continuous real function on $[a, b]$ has a minimum and maximum and takes every value between them.

[F6]

Monotonicity and nonnegative homogeneity of the nonnegative integral, The nonnegative integral agrees with the simple integral on simple functions, and The integral of a nonnegative simple function: nonnegative integrals are monotone and homogeneous, and $\int 1_{U} d μ = μ (U)$ .

[F7]

The Lebesgue integral is linear on $L^{1} (μ)$ : integrable functions may be added and integrated linearly.

[F8]

The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ , Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ , and The reals form a totally ordered field: $(2 m)!_{R} = \prod_{j = 1}^{2 m} j > 0$ .

[F9]

Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point and The Borel sigma-algebra of a topological space: a continuous function on $[a, b]$ is Borel measurable, since preimages of relative open sets are relative open and those sets generate $B ([a, b])$ .

[F10]

Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function: absolute values, polynomial functions, sums and products of the continuous functions used below are continuous.

Proof

1.1F1F3F4F5F6F9F10algebra

The function $f$ and the polynomial $H$ from [F3] are continuous, hence Borel measurable by [F9]–[F10]. They are bounded on the compact interval by [F5]. Since $μ ([a, b]) < \infty$ by [F1], monotonicity and homogeneity in [F6] give $\int ∣ f ∣ d μ < \infty$ and $\int ∣ H ∣ d μ < \infty$ . Also $p_{m}^{2}$ is integrable by [F4]. Thus all integrals below are finite.

1.2F3F5F8algebra

Let $A = \min_{[a, b]} f^{(2 m)}$ and $B = \max_{[a, b]} f^{(2 m)}$ , which exist by [F5]. The pointwise remainder [F3], and the zero error at nodes, imply for every $x \in [a, b]$ that $\frac{A}{(2 m)!_{R}} p_{m} (x)^{2} \leq f (x) - H (x) \leq \frac{B}{(2 m)!_{R}} p_{m} (x)^{2} .$ The multiplier $p_{m} (x)^{2}$ is nonnegative.

2.1F2F3step 1.1algebra

By [F3], $H (x_{i}) = f (x_{i})$ and $\deg H \leq 2 m - 1$ . Exactness [F2] gives $\int H d μ = Q_{m} (H) = Q_{m} (f)$ , so the quadrature error is $\int (f - H) d μ$ .

2.2F4F6F7F8step 1.2algebra

Integrating the nonnegative differences in step 1.2 and using [F6]–[F7] gives $\frac{A}{(2 m)!_{R}} \int p_{m}^{2} d μ \leq \int (f - H) d μ \leq \frac{B}{(2 m)!_{R}} \int p_{m}^{2} d μ .$ By [F4], $h_{m} : = \int p_{m}^{2} d μ > 0$ . Define $γ : = (2 m)!_{R} \int (f - H) d μ / h_{m}$ ; the displayed bounds give $A \leq γ \leq B$ .

3.1F5step 2.2caseschoose

If $A = B$ , $f^{(2 m)}$ is constant and any point of $(a, b)$ has value $γ$ . If $A < γ < B$ , choose points attaining $A$ and $B$ by [F5]. They are distinct; the intermediate value property on the segment between them gives a point strictly between the extrema where $f^{(2 m)} = γ$ , and that point lies in $(a, b)$ .

3.2F1F3F6F8step 2.2casesalgebra

Suppose $γ = A < B$ and $f^{(2 m)}$ has no interior point with value $A$ . Then $f^{(2 m)} (t) > A$ for every $t \in (a, b)$ . For every non-node $x$ , [F3] uses some $ξ_{x} \in (a, b)$ , and so $d (x) : = f (x) - H (x) - A p_{m} (x)^{2} / (2 m)!_{R} > 0$ because $p_{m} (x) \neq 0$ . At nodes, $d = 0$ . There is a support point $y$ not among the $m$ nodes by [F1]; continuity makes $d \geq c > 0$ on a relative open neighborhood $U$ of $y$ , and $μ (U) > 0$ . Thus [F6] gives $\int d d μ > 0$ . But $γ = A$ and step 2.2 imply $\int d d μ = 0$ , a contradiction. Hence some interior point has derivative value $γ$ .

3.3F1F3F6F8step 2.2casesalgebra

The case $γ = B > A$ is analogous: if $f^{(2 m)} (t) < B$ throughout $(a, b)$ , the nonnegative continuous function $e (x) : = B p_{m} (x)^{2} / (2 m)!_{R} - (f (x) - H (x))$ is strictly positive at every non-node, hence on a positive-measure neighborhood of a support point outside the nodes. This contradicts $γ = B$ in step 2.2. Therefore there is an interior point with derivative value $γ$ .

4.1step 2.1step 2.2step 3.1step 3.2step 3.3algebra∎

In every case there is $ξ \in (a, b)$ with $f^{(2 m)} (ξ) = γ$ . Substitute the definition of $γ$ , use step 2.1, and rearrange to obtain the stated remainder formula.

Depends on

Used by

Dependency tree · two levels

108 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

John A. Gubner, Gaussian Quadrature and the Eigenvalue Problem, §§2–5, 2020 (standard reference, not scraped)
MATH 373 Lecture Notes, Lecture 14: Gaussian Quadrature, §§10.2–10.5 (standard reference, not scraped)
Walter Gautschi, The Interplay Between Classical Analysis and (Numerical) Linear Algebra, §2.1 (standard reference, not scraped)