TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Gauss–Jacobi exactness and the derivative remainder

Statement

Assume Countable Choice. Let $n \geq 1$ , $α, β > - 1$ , and let $Q_{n}^{α, β}$ be the rule of The Gauss–Jacobi quadrature rule for $d μ_{α, β} = (1 - t)^{α} (1 + t)^{β} d t$ on $[- 1, 1]$ . It integrates every polynomial of degree at most $2 n - 1$ exactly and has positive weights. If $g \in C^{2 n} ([- 1, 1])$ , and $p_{n}$ is the monic node polynomial, then some $ξ \in (- 1, 1)$ satisfies $\int_{[- 1, 1]} g d μ_{α, β} - Q_{n}^{α, β} (g) = \frac{g^{(2 n)} (ξ)}{(2 n)!_{R}} \int_{[- 1, 1]} p_{n} (t)^{2} d μ_{α, β} (t) .$ In particular, with $K_{n, α, β} : = (2 n)!_{R}^{- 1} \int p_{n}^{2} d μ_{α, β} > 0$ , $∣ \int g d μ_{α, β} - Q_{n}^{α, β} (g) ∣ \leq K_{n, α, β} ∥ g^{(2 n)} ∥_{\infty} .$

Facts & Assumptions

Given: Countable Choice, $n \geq 1$ , $α, β > - 1$ , the Gauss–Jacobi rule, and $g \in C^{2 n} ([- 1, 1])$ .

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): Countable Choice is the only axiom used to construct the Jacobi density measure.

[F1]

The Jacobi weight defines a finite positive measure with full support and Gauss–Jacobi nodes and weights are well-defined: $μ_{α, β}$ is finite positive, has at least $n + 1$ support points, has every finite moment, and the $n$ nodes and weights are defined.

[F2]

The Gauss–Jacobi quadrature rule: $Q_{n}^{α, β}$ is the Gaussian rule for $μ_{α, β}$ , with node polynomial $p_{n}$ and weights defined by integrating the Lagrange cardinal polynomials.

[F3]

Gaussian quadrature is exact through degree 2m−1 and has positive weights: an $n$ -node Gaussian rule for finite positive order- $2 n - 1$ moment data is exact through degree $2 n - 1$ , has positive weights, and its weights sum to the total mass.

[F4]

Gaussian quadrature has the Hermite mean-value remainder: for order- $2 n$ moment data and $g \in C^{2 n}$ , the Gaussian error equals $g^{(2 n)} (ξ) / (2 n)!_{R}$ times the squared norm of the monic node polynomial.

[F5]

For a nonempty subset of $R^{n}$ with $n \geq 1$ , compactness, closedness and boundedness, pseudocompactness, and attainment of extrema by every continuous real-valued function are equivalent: every continuous real function on $[- 1, 1]$ attains a finite maximum and minimum.

[F6]

The polynomial moment pairing is a real inner product: a nonzero polynomial of degree at most $n$ has strictly positive squared integral under this full-support positive measure.

[F7]

The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ and Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ : $(2 n)!_{R}$ is the positive real image of $\prod_{j = 1}^{2 n} j$ .

[F8]

Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ : $C^{2 n}$ means the derivatives through order $2 n$ exist and are continuous.

Proof

1.1A1F1F3F4given

By [F1], $μ_{α, β}$ is a finite positive measure with all moments finite and support containing at least $n + 1$ points. Thus its moment datum satisfies both the order- $2 n - 1$ and order- $2 n$ hypotheses in [F3] and [F4].

2.1F2F3step 1.1

Applying [F3] to the rule [F2] proves polynomial exactness through degree $2 n - 1$ and positivity of the weights.

2.2F1F2F4givenstep 1.1

Apply the Hermite remainder [F4] to $g$ and the order- $2 n$ datum from step 1.1. It gives the stated $ξ$ and error identity with the same monic node polynomial $p_{n}$ .

3.1F1F5F6F7F8step 2.2algebra∎

The integral of $p_{n}^{2}$ is finite by [F1] and strictly positive by [F6], since $p_{n}$ is monic and hence nonzero. Thus $K_{n, α, β} > 0$ by [F7]. The derivative $g^{(2 n)}$ is continuous by [F8] on a compact interval, so [F5] gives $∥ g^{(2 n)} ∥_{\infty} < \infty$ ; taking absolute values in step 2.2 yields the claimed error bound.

Depends on

Used by

Dependency tree · two levels

91 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

Christopher J. Bishop, The Riemann Mapping Theorem, Chapter 3 §3, Gauss-Jacobi quadrature lecture notes (standard reference, not scraped)