ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-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.

Two-node Gauss is exact through degree three but not for x to the fourth

Example

Assume Countable Choice. For Lebesgue measure on $[- 1, 1]$ , the two-node Gaussian rule has nodes $\pm 1 / \sqrt{3}$ and weights $1$ . The supplier theorem gives exactness through degree three, but the error on $x^{4}$ is $8 / 45$ .

Facts & Assumptions

Given: Countable Choice, $a = - 1$ , $b = 1$ , $m = 2$ , $r = 3 = 2 m - 1$ , and Lebesgue measure $μ$ on $[- 1, 1]$ .

[F1]

Positive-measure Gaussian quadrature moment data: a moment datum is a finite positive measure whose relative support contains at least $m + 1$ points and whose moments through degree $2 m - 1$ are finite.

[F2]

Monic orthogonal polynomials exist uniquely through the quadrature order: the monic degree-two polynomial $p_{2}$ is orthogonal to every polynomial of degree below two.

[F3]

The m-node Gaussian quadrature rule for a positive measure: the nodes are the roots of $p_{2}$ and the weights are the integrals of their Lagrange cardinal polynomials.

[F4]

Gaussian quadrature is exact through degree 2m−1 and has positive weights: the rule integrates every polynomial of degree at most $2 m - 1$ exactly.

[F5]

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)$ : the integral of a continuous derivative on $[- 1, 1]$ is the primitive's endpoint difference.

[F6]

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: $(x^{k})^{'} = k x^{k - 1}$ for positive integer $k$ .

[F7]

Under Countable Choice, $λ_{1} ([- 1, 1]) = 2$ and every nondegenerate subinterval has its length as Lebesgue measure (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}_{ω}$ )).

[F8]

Under Countable Choice, a bounded Riemann-integrable function on a closed interval is Lebesgue integrable and the two integrals agree (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}_{ω}$ )).

Verification

1.1F1F7F8given

By [F7], $μ ([- 1, 1]) = 2$ . Every relative neighborhood of a point in $[- 1, 1]$ contains a nondegenerate relative interval, so it has positive measure by [F7]; hence the relative support is all of $[- 1, 1]$ and contains at least three points. Each $∣ x ∣^{k}$ , $0 \leq k \leq 3$ , is continuous and bounded on $[- 1, 1]$ , hence Riemann integrable and Lebesgue integrable by [F8]. Thus the moment datum conditions [F1] hold.

1.2F1F2F3F5F6F8algebra

Write $p_{2} (x) = x^{2} + b x + c$ . Orthogonality [F2] to $1$ and $x$ , using [F8] to read the Lebesgue moments as Riemann integrals, and [F5, F6] to evaluate $\int_{- 1}^{1} 1 = 2$ , $\int x = 0$ , $\int x^{2} = 2 / 3$ , and $\int x^{3} = 0$ , gives $2 / 3 + 2 c = 0$ and $2 b / 3 = 0$ . Hence $p_{2} = x^{2} - 1 / 3$ , and [F3] gives nodes $\pm 1 / \sqrt{3}$ .

2.1F3F5F6F8step 1.2algebra

Using the nodes from step 1.2, the corresponding cardinal polynomials are $ℓ_{+} (x) = (x + 1 / \sqrt{3}) / (2 / \sqrt{3}) = (1 + \sqrt{3} x) / 2$ and $ℓ_{-} (x) = (1 / \sqrt{3} - x) / (2 / \sqrt{3}) = (1 - \sqrt{3} x) / 2$ . By [F8], [F5], and [F6], their odd terms integrate to zero and their constant terms integrate to one, so [F3] gives both weights equal to $1$ .

3.1F4F5F6F8step 1.2step 2.1algebra∎

By [F4], this rule is exact for every polynomial of degree at most three. Using the nodes and weights from steps 1.2 and 2.1, its value on $x^{4}$ is $(1 / \sqrt{3})^{4} + (- 1 / \sqrt{3})^{4} = 2 / 9$ , whereas [F8], [F5], and [F6] give $\int_{- 1}^{1} x^{4} d μ = 2 / 5$ . The absolute error is $2 / 5 - 2 / 9 = 8 / 45$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

73 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

MATH 373 Lecture Notes, Lecture 14, Gaussian Quadrature (standard reference, not scraped)