CorollaryStatement: Literature-sourcedProof: AI-generatedPipeline-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.

The Duffy weighted product rule has an explicit bound using pure coordinate derivatives

Statement

Assume Countable Choice, let $α < 2$ , $ρ = 1 - α$ , $n \geq 1$ , and let $G \in C^{2 n}$ in each coordinate on $[0, 1]^{2}$ . Let ${\tilde{p}}_{n, ρ}$ and ${\tilde{p}}_{n, 0}$ be the monic node polynomials of the pushed-forward Gauss–Jacobi rules for $r^{ρ} d r$ and $d s$ , respectively. Define $M_{ρ} = \int_{0}^{1} r^{ρ} d r = \frac{1}{ρ + 1}, K_{ρ} = \frac{1}{(2 n)!_{R}} \int_{0}^{1} {\tilde{p}}_{n, ρ} (r)^{2} r^{ρ} d r, K_{0} = \frac{1}{(2 n)!_{R}} \int_{0}^{1} {\tilde{p}}_{n, 0} (s)^{2} d s .$ Then the rule of Weighted product Gauss quadrature after the Duffy transform satisfies $∣ \int_{T} ∥ (x, y) ∥_{2}^{- α} q (x, y) d x d y - Q_{n, α}^{D} (G) ∣ \leq K_{ρ} ∥ \partial_{r}^{2 n} G ∥_{\infty} + M_{ρ} K_{0} ∥ \partial_{s}^{2 n} G ∥_{\infty},$ where $G$ is the transformed amplitude from The Duffy map turns a vertex singularity into an integrable radial weight.

Facts & Assumptions

Given: Countable Choice, $α < 2$ , $n \geq 1$ , continuous $q$ on the reference triangle, the Duffy rule, and the stated coordinate smoothness of its transformed amplitude $G$ .

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): Countable Choice is used to supply the Lebesgue-density positive measures underlying the two Gaussian rules.

[F1]

The Duffy map turns a vertex singularity into an integrable radial weight: the singular triangle integral equals $\int_{0}^{1} \int_{0}^{1} r^{ρ} G (r, s) d s d r$ .

[F2]

Weighted product Gauss quadrature after the Duffy transform: its finite sum is the tensor product of the $n$ -node rules for $r^{ρ} d r$ and $d s$ .

[F3]

Gauss–Jacobi exactness and the derivative remainder: each pushed-forward one-dimensional rule has error constant $(2 n)!^{- 1} \int {\tilde{p}}_{n}^{2} d μ$ and integrates the measure mass exactly.

[F4]

A tensor product of two positive Gaussian rules has a derivative error bound: the tensor error is bounded by the first coordinate constant times the second mass and the first mass times the second coordinate constant.

[F5]

The Jacobi weight defines a finite positive measure with full support: the weights $(1 + t)^{ρ}$ for $ρ > - 1$ and $1$ define finite positive full-support measures with moments of every finite order.

[F6]

The improper integral of a power at zero: $\int_{0}^{1} r^{ρ} d r = 1 / (ρ + 1)$ for $ρ > - 1$ .

[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$ .

Proof

1.1A1F2F5givenalgebra

The exponent $ρ = 1 - α$ satisfies $ρ > - 1$ . By [F5] and [A1], the Jacobi weights $(1 + t)^{ρ}$ and $1$ define finite positive measures with full support; the affine node/weight scalings in [F2] give their Gaussian rules for $r^{ρ} d r$ and $d s$ .

1.2F2F3F6F7algebra

The first measure has mass $M_{ρ} = 1 / (ρ + 1)$ by [F6], and the second has mass $1$ . For the first affine pushforward, $r = (1 + t) / 2$ gives $r^{ρ} d r = 2^{- (ρ + 1)} (1 + t)^{ρ} d t$ and its monic node polynomial is ${\tilde{p}}_{n, ρ} (r) = 2^{- n} p_{n, ρ} (2 r - 1)$ . Hence its squared-node-polynomial integral is $2^{- (ρ + 1 + 2 n)} \int_{- 1}^{1} p_{n, ρ} (t)^{2} (1 + t)^{ρ} d t$ . The derivative of $H ((1 + t) / 2)$ contributes $2^{- 2 n}$ , so [F3] gives exactly $K_{ρ}$ as defined. The same calculation with $ρ = 0$ gives $K_{0}$ . Positivity of the factorial denominator follows from [F7].

2.1F1F2F4step 1.2∎

Apply [F4] to the transformed integral and tensor rule identified by [F1]–[F2]. Substituting the masses and constants from step 1.2 yields the displayed error bound.

Depends on

Used by

Cited to discharge well-definedness by Weighted product Gauss quadrature after the Duffy transform.

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

Imperial College London, Numerical quadrature, Finite Element course notes, §1.6 (standard reference, not scraped)
Christopher J. Bishop, The Riemann Mapping Theorem, Chapter 3 §3, Gauss-Jacobi quadrature lecture notes (standard reference, not scraped)