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.

A signed Simpson-Smolyak weight makes a nonnegative chaos coefficient estimate negative

Example

For $k = 1, \dots, 8$ , put $ϕ (x) = \prod_{k = 1}^{8} (1 - 8 x / k)^{2}$ on $[0, 1]$ and $u (x, y) = ϕ (x) ϕ (y)$ . This is a nonnegative polynomial. Under the uniform law on $[0, 1]^{2}$ , the constant polynomial-chaos coefficient is $c_{00} = \int_{[0, 1]^{2}} u > 0$ . Yet the level-two composite-Simpson Smolyak rule on $Λ_{2} = {(i, j) : i + j \leq 2}$ returns $- 1 / 144$ . This shows why signed Smolyak weights matter when integrating chaos coefficients. Any tensor product of Gaussian rules with positive coordinate weights returns a nonnegative value on $u$ ; no Gaussian exactness for this high-degree polynomial is asserted.

Facts & Assumptions

Given: The uniform probability law on $[0, 1]^{2}$ , $ϕ (x) = \prod_{k = 1}^{8} (1 - 8 x / k)^{2}$ , $u (x, y) = ϕ (x) ϕ (y)$ , the constant chaos basis $Ψ_{00} = 1$ , and the Simpson hierarchy of Nested one-dimensional quadrature levels and differences.

[F1]

Nested one-dimensional quadrature levels and differences: $Q_{ℓ} = Q_{S} (\cdot; 0, 1, 2^{ℓ + 1})$ , $Δ_{0} = Q_{0}$ , and $Δ_{ℓ} = Q_{ℓ} - Q_{ℓ - 1}$ .

[F2]

Composite Simpson rule on an even uniform grid: the endpoint weight at level $ℓ$ is $1 / (3 \cdot 2^{ℓ + 1})$ , and the other weights are nonnegative.

[F3]

Smolyak cubature on a finite downward-closed index set: for $Λ_{2} = {(i, j) : i + j \leq 2}$ , the Smolyak functional is the sum of its six tensor details.

[F4]

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: one-variable polynomials and their finite products and sums are continuous.

[F5]

A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion: a continuous function on a nondegenerate closed interval is Riemann integrable.

[F6]

If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ : pointwise order between integrable functions implies the same order between their integrals.

[F7]

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 integrals over $[0, δ]$ and $[δ, 1]$ when $0 < δ < 1$ .

[F8]

The integral of a product function on a product rectangle is the product of the two integrals: the integral of a product function on a product rectangle factors into the coordinate integrals.

[F9]

The m-node Gaussian quadrature rule for a positive measure: a Gaussian rule returns a finite weighted sum of samples.

[F10]

Gaussian quadrature is exact through degree 2m−1 and has positive weights: for valid positive-measure moment data, every Gaussian weight is strictly positive.

[F11]

Tensor-product Gaussian quadrature: tensor weights are products of coordinate weights.

[F12]

Finite sums and finite products, by recursion and Laws of finite sums and finite products: finite sums distribute; finite sums and finite products of nonnegative terms are nonnegative.

[F13]

By trichotomy, every real $z$ is zero, positive, or negative. Its square is $0$ in the zero case, positive by Sign rules for products and monotonicity of multiplication in the positive case, and positive in the negative case because $(- z) > 0$ and $(- z)^{2} = z^{2}$ by Sign rules for products: $(- a) b = - (a b)$ and $(- a) (- b) = a b$ . Thus every real square is nonnegative; Multiplication by zero: $0 \cdot a = 0$ supplies the zero case.

Verification

1.1givenF4F5F6F7F8F12F13choose

Every real square is nonnegative by [F13], so each factor in $ϕ$ is nonnegative and [F12] gives $ϕ (x) \geq 0$ on $[0, 1]$ . The polynomial $ϕ$ is continuous by [F4] and satisfies $ϕ (0) = 1$ . Continuity at zero gives $η > 0$ such that $ϕ (x) > 1 / 2$ for $0 \leq x < η$ ; choose $δ = \min (η / 2, 1 / 2)$ , so $0 < δ < η$ and $δ < 1$ . By [F5]–[F6], $\int_{0}^{δ} ϕ \geq δ / 2$ and $\int_{δ}^{1} ϕ \geq 0$ ; [F7] then gives $\int_{0}^{1} ϕ \geq δ / 2 > 0$ . Applying [F8] to the continuous coordinate factors establishes integrability of $u$ and gives $c_{00} = (\int_{0}^{1} ϕ)^{2} > 0$ .

2.1givenF1F3F12F13step 1.1algebra

For each $m = 0, \dots, 8$ , $ϕ (m / 8) = 0$ when $m > 0$ , because the factor indexed by $k = m$ vanishes; $ϕ (0) = 1$ . The nested Simpson grids through level two are $X_{0} = {0, 1 / 2, 1}$ , $X_{1} = {m / 4 : 0 \leq m \leq 4}$ , and $X_{2} = {m / 8 : 0 \leq m \leq 8}$ . Thus every sampled value of $u$ on any tensor rule in $Λ_{2}$ vanishes except at $(0, 0)$ , where it is one; all sampled values are nonnegative by [F13] and [F12].

3.1givenF1F2F3F12step 2.1algebra

Let $w_{ℓ}$ be the level- $ℓ$ endpoint weight. By [F2], $w_{0} = 1 / 6$ , $w_{1} = 1 / 12$ , and $w_{2} = 1 / 24$ . Expanding the six details from [F3] and using finite distributivity [F12] gives $Q_{Λ_{2}} = Q_{2} \otimes Q_{0} + Q_{0} \otimes Q_{2} - Q_{1} \otimes Q_{0} - Q_{0} \otimes Q_{1} + Q_{1} \otimes Q_{1}$ . By step 2.1, its value on $u$ is the combined coefficient at $(0, 0)$ : $2 w_{2} w_{0} - 2 w_{1} w_{0} + w_{1}^{2} = 2 / (24 \cdot 6) - 2 / (12 \cdot 6) + 1 / 12^{2} = - 1 / 144 < 0$ . This differs in sign from $c_{00} > 0$ in step 1.1.

4.1givenF9F10F11F12F13step 3.1algebra∎

For tensor products of Gaussian rules with valid positive-measure moment data, [F10] makes every coordinate weight positive and [F11] makes each tensor weight a product of positive numbers. Since all samples of $u$ are nonnegative by [F12]–[F13], [F9] and [F12] make the resulting finite sum nonnegative. Together with the negative Simpson estimate in step 3.1, this is a sign comparison; it does not claim that such a Gaussian rule exactly integrates $u$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

80 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

T. Gerstner and M. Griebel, Sparse Grids, Encyclopedia of Quantitative Finance, §Numerical integration (standard reference, not scraped)
John A. Gubner, Gaussian Quadrature and the Eigenvalue Problem, §§2–5 (standard reference, not scraped)
Tobin A. Driscoll and Richard J. Braun, Fundamentals of Numerical Computation, §5.6 (standard reference, not scraped)