Pipeline-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.

✓ 4 results · all verified · 3 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Singular and infinite interval quadrature — Examples

1 · Prerequisites

2 · Summary

The examples compute the logarithmic endpoint integral, an interior-pole principal value, and a weakly singular reference-triangle integral. The Gaussian example gives the sinh–sinh transformed identity and a rigorous finite-sum tail bound. Its transformed complex extension fails the uniform strip-decay hypothesis, so no total quadrature error bound is asserted for that example; this records the exact boundary of the analytic-strip theorem.

3 · Logical flowchart

4 · Definitions, theorems and proofs

ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

The Gaussian integral on the line with a certified sinh-sinh truncation tail

Statement

For $f (x) = e^{- x^{2}}$ on $R$ , use the sinh–sinh mode of Finite truncated tanh–sinh, exp–sinh, and sinh–sinh trapezoid rules. Its transformed function is $Φ (t) = \frac{π}{2} \cosh t \cosh u (t) e^{- \sinh^{2} u (t)}, u (t) = \frac{π}{2} \sinh t .$ Then the absolutely convergent improper Riemann integral satisfies $\int_{R} Φ (t) d t = \sqrt{π}$ . There is $T > 0$ such that $∣ Φ (t) ∣ \leq e^{- e^{∣ t ∣}}$ for $∣ t ∣ \geq T$ , so if $N_{\pm} h \geq T$ , the omitted finite-sum tail is at most $e^{- e^{N_{-} h}} + e^{- e^{N_{+} h}} .$ However, the complex extension of this transformed Gaussian does not satisfy the uniform exponential-decay hypothesis of An analytic-strip error bound for the infinite trapezoid sum on any nonzero horizontal substrip. Thus this example certifies its truncation tail but does not claim a full discretization-plus-tail error bound.

Facts & Assumptions

Given: The real sinh–sinh transformation and finite truncation with $h > 0$ and nonnegative integers $N_{-}, N_{+}$ .

[F1]

Finite truncated tanh–sinh, exp–sinh, and sinh–sinh trapezoid rules: $x (t) = \sinh ((π / 2) \sinh t)$ and $Φ (t) = x^{'} (t) e^{- x (t)^{2}}$ .

[F2]

The double-exponential maps and their change-of-variable identities: if the transformed function is absolutely integrable as an improper Riemann integral, its integral equals the whole-line target integral.

[F3]

A double-exponential envelope bounds the omitted trapezoid tails: an envelope $A e^{- B e^{κ ∣ t ∣}}$ bounds each continuous tail and the corresponding omitted trapezoid samples by $A (κ B)^{- 1} e^{- B e^{κ N h}}$ .

[F4]

The Gaussian integral $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ : $\int_{R} e^{- x^{2}} d x = \sqrt{π}$ .

[F5]

A finite double-exponential trapezoid has separate strip and tail errors: a total finite-rule error estimate requires both the separate analytic-strip and sampled-tail hypotheses.

[F6]

An analytic-strip error bound for the infinite trapezoid sum: its analytic-strip hypothesis requires uniform exponential decay on each horizontal edge of some nonzero closed substrip.

[F7]

Complex sine, cosine, hyperbolic sine, and hyperbolic cosine from the complex exponential defines $\sinh z = (e^{z} - e^{- z}) / 2$ and $\cosh z = (e^{z} + e^{- z}) / 2$ . The addition formulas for complex trigonometric and hyperbolic functions, $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , and $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential give $\sinh (U + i V) = \sinh U \cos V + i \cosh U \sin V$ and $\cosh (U + i V) = \cosh U \cos V + i \sinh U \sin V$ for real $U, V$ , by substituting the exponential definitions.

[F8]

The exponential tends to $+ \infty$ at $+ \infty$ and to $0$ at $- \infty$ : the real exponential tends to $+ \infty$ at $+ \infty$ and to zero at $- \infty$ . The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ and The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ give $e^{v + w} = e^{v} e^{w}$ and $e^{- v} = 1 / e^{v} > 0$ . The real definitions The six hyperbolic functions and their natural domains and Addition formulas, identities, parity, and derivatives of the hyperbolic functions give $(\sinh t)^{'} = \cosh t$ , $(\cosh t)^{'} = \sinh t$ , parity, positivity of $\cosh$ , and unbounded growth of both hyperbolic functions at $+ \infty$ .

[F9]

The exponential dominates every fixed nonnegative integer power at $+ \infty$ : $v / e^{c v} \to 0$ as $v \to + \infty$ for every fixed $c > 0$ .

[F10]

Complex sine, cosine, hyperbolic sine, and hyperbolic cosine are entire with their standard derivatives gives entire $\sinh, \cosh$ with derivatives $\cosh, \sinh$ . Together with The complex exponential is entire and its complex derivative is itself, The chain rule for complex derivatives, and Linearity, product, reciprocal, and quotient rules for complex derivatives, this makes the displayed complex extension of $Φ$ entire.

[F11]

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 and The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : a continuous function takes intermediate values, and a positive derivative makes it strictly increasing.

[F12]

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

[F13]

The zero sets of sine and cosine and the least positive common period 2 pi and Quarter-turn values and shifts by pi/2 and pi: $\cos 0 = 1$ , $\sin (π / 2) = 1$ , and neither function has a zero in $(0, π / 2)$ ; continuity and [F11] therefore give $\sin y, \cos y > 0$ there.

Proof

1.1F1F8F9algebra

On the real axis, $x^{'} (t) = (π / 2) \cosh t \cosh u (t) > 0$ . As $t \to \pm \infty$ , $x (t) \to \pm \infty$ . We show the tail envelope for $t \to + \infty$ ; evenness gives the left tail. For $t \geq 1$ , $\sinh t \geq c e^{t}$ with $c = (1 - e^{- 2}) / 2 > 0$ , so $u (t) \geq c_{1} e^{t}$ for $c_{1} = π c / 2$ . For $u \geq 1$ , $\sinh u \geq c e^{u}$ , hence $x (t)^{2} \geq c^{2} e^{2 u (t)} \geq c^{2} e^{2 c_{1} e^{t}}$ . Also $u (t) \leq (π / 4) e^{t}$ and $\cosh t \leq e^{t}$ , $\cosh u \leq e^{u}$ , so for a fixed constant $C^{'} > 0$ and all sufficiently large $t$ , $(π / 2) \cosh t \cosh u (t) \leq e^{C^{'} e^{t}}$ . Put $v = e^{t}$ . By [F8], $v \to \infty$ , and [F9] implies $c^{2} e^{2 c_{1} v} / v \to \infty$ . Thus $x (t)^{2}$ eventually exceeds both $2 C^{'} e^{t}$ and $2 e^{t}$ . It follows that $Φ (t) \leq e^{C^{'} e^{t} - x (t)^{2}} \leq e^{- x (t)^{2} / 2} \leq e^{- e^{t}}$ for all sufficiently large $t$ .

1.2F6F7F8F10F11F13algebraconstruct

For any proposed substrip halfwidth $a > 0$ , fix $0 < y < \min (a, π / 2)$ ; then [F13] gives $\sin y, \cos y > 0$ . Extend $u (z) = (π / 2) \sinh z$ holomorphically; this extension is entire by [F10]. For $z = x + i y$ , write $u = U + i V$ with $U = (π / 2) \sinh x \cos y$ and $V = (π / 2) \cosh x \sin y$ . The continuous function $V (x)$ has positive derivative for $x > 0$ and tends to infinity. For every sufficiently large integer $j$ , its value $(j + 1 / 2) π$ lies strictly between $V (0)$ and some $V (R)$ ; [F11] gives a solution $x_{j} \in (0, R)$ , and strict increase makes it unique. Defining $x_{j}$ as that unique solution avoids any choice of a sequence. Then $x_{j} \to \infty$ . At those points, [F7] gives $Re (\sinh^{2} u) = - \cosh^{2} U$ and $∣ \cosh u ∣ = \sinh U$ . Since $U (x_{j}) \to \infty$ , also $∣ \cosh (x_{j} + i y) ∣^{2} = \sinh^{2} x_{j} + \cos^{2} y \geq \sinh^{2} x_{j}$ by [F7] and $\cosh^{2} x_{j} - \sinh^{2} x_{j} = 1$ from [F8]. Thus it follows that $∣ Φ (x_{j} + i y) ∣ = \frac{π}{2} ∣ \cosh (x_{j} + i y) ∣ \sinh U (x_{j}) e^{\cosh^{2} U (x_{j})} ⟶ \infty .$ Thus no bound $C e^{- η ∣ x ∣}$ can hold on that horizontal line; this disproves the uniform strip hypothesis in [F6] for every proposed positive halfwidth.

2.1F2F3F4F12step 1.1

The envelope in step 1.1 makes $Φ$ absolutely integrable on both tails. On every compact interval, $∣ Φ ∣$ is continuous and Riemann integrable by [F12], so $Φ$ is absolutely integrable on $R$ as an improper Riemann integral. Apply [F2] and then [F4] to obtain $\int Φ = \sqrt{π}$ . Applying [F3] with $A = B = κ = 1$ gives the asserted omitted-sample bound when $N_{\pm} h \geq T$ .

3.1F5step 2.1step 1.2∎

By [F5], the bound of the full-error theorem requires the strip premise as well as the tail premise. The real integral and truncation tail are justified in step 2.1, while step 1.2 disproves that strip premise. Thus no total quadrature error bound is asserted.

ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

An interior Cauchy principal value reduces to a regular integral

Statement

For $f (x) = x$ on $[0, 1]$ and $c = 1 / 3$ , the symmetric Cauchy principal value is $1 + \frac{1}{3} \log 2$ .

Facts & Assumptions

Given: $f (x) = x$ , $a = 0$ , $c = 1 / 3$ , $b = 1$ .

[F1]

The Cauchy principal-value subtraction identity: for $f \in C^{1} ([a, b])$ , the principal value is the ordinary integral of $(f (x) - f (c)) / (x - c)$ plus $f (c) \log ((b - c) / (c - a))$ .

[F2]

The natural logarithm as the inverse of the exponential function and The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t: $\log$ is the natural logarithm and $\log 2$ is defined for the positive number $2$ .

[F3]

Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ : the linear function is $C^{1}$ on $[0, 1]$ .

Proof

1.1givenF3algebra

The function $f (x) = x$ is $C^{1}$ by [F3] and $f (c) = 1 / 3$ . For every $x \neq c$ , $(f (x) - f (c)) / (x - c) = 1$ , and its continuous extension at $c$ is also $1$ .

2.1F1F2step 1.1algebra∎

Apply [F1]. The ordinary integral of this quotient is $\int_{0}^{1} 1 d x = 1$ , and $(b - c) / (c - a) = (2 / 3) / (1 / 3) = 2$ . Thus the principal value equals $1 + (1 / 3) \log 2$ .

ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passOpen item page →

A 1 over r singularity on the reference triangle

Statement

On $T = {(x, y) : 0 \leq y \leq x \leq 1}$ , the weakly singular integral $\int_{T} \frac{d x d y}{\sqrt{x^{2} + y^{2}}} = \log (1 + \sqrt{2}) .$ Under The reference-triangle Duffy map from a vertex, its transformed amplitude is $G (r, s) = (1 + s^{2})^{- 1 / 2}$ with radial weight $r^{0}$ . For every $n \geq 1$ , Weighted product Gauss quadrature after the Duffy transform applies with $α = 1$ , and The Duffy weighted product rule has an explicit bound using pure coordinate derivatives bounds its error by $K_{0} ∥ \partial_{r}^{2 n} G ∥_{\infty} + K_{0} ∥ \partial_{s}^{2 n} G ∥_{\infty}$ with the constants specified there; here $\partial_{r}^{2 n} G = 0$ .

Facts & Assumptions

Given: The reference triangle $T$ and integrand $(x^{2} + y^{2})^{- 1 / 2}$ away from its vertex.

[F1]

The Duffy map turns a vertex singularity into an integrable radial weight: for exponent $α = 1$ and amplitude $q = 1$ , the transformed radial weight is $r^{0}$ and $G (r, s) = (1 + s^{2})^{- 1 / 2}$ .

[F2]

The Duffy weighted product rule has an explicit bound using pure coordinate derivatives: the weighted product rule error is bounded by the two pure derivative norms with its stated constants.

[F3]

The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t and The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ : differentiating gives $\frac{d}{d s} \log (s + \sqrt{1 + s^{2}}) = (1 + s^{2})^{- 1 / 2}$ for $s \in [0, 1]$ . 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)$ evaluates the integral of this continuous derivative by its endpoint increment.

[F4]

The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ and Continuity and derivatives of positive-base real powers: the displayed amplitude is smooth in $s$ because $1 + s^{2}$ is strictly positive.

[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: continuous derivatives on the compact square are bounded.

Proof

1.1F1F3algebra

For $G (r, s) = (1 + s^{2})^{- 1 / 2}$ , the transformed integral in [F1] is $\int_{0}^{1} \int_{0}^{1} G (r, s) d s d r$ . An antiderivative in $s$ is the logarithm in [F3], so the integral equals $\log (1 + \sqrt{2}) - \log 1 = \log (1 + \sqrt{2})$ .

2.1F2F4F5givenalgebra∎

The function $G$ is smooth on the compact square by [F4], and its derivatives are bounded there by [F5]. The Duffy weighted product rule therefore has the error bound [F2]; since $G$ is independent of $r$ , its positive-order $r$ derivative vanishes.

ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Gauss–Jacobi regularization for x to the minus one half times log x

Statement

The improper integral is $\int_{0}^{1} x^{- 1 / 2} \log x d x = - 4.$ For example, Finite endpoint power substitution followed by Gauss–Jacobi quadrature applies with $n = 1$ , $α = - 1 / 2$ , $β = 0$ , $m_{a} = 1$ , $m_{b} = 0$ , $h (x) = 1$ , $q_{a} = 7$ , and $q_{b} = 4$ . The transformed functions are $C^{2}$ and Error bound after endpoint power regularization gives an explicit error bound $C_{1} (∥ F_{L}^{''} ∥_{\infty} + ∥ F_{R}^{''} ∥_{\infty})$ for the returned two-node sum.

Facts & Assumptions

Given: The integrand $f (x) = x^{- 1 / 2} \log x$ on $(0, 1]$ and the specified endpoint-regularization inputs.

[F1]

The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t: $\log$ is differentiable on $(0, \infty)$ with derivative $1 / x$ .

[F2]

A sufficiently high power regularizes finite logarithmic endpoint factors: $t^{δ} P (\log t)$ extends to $C^{r} ([0, 1])$ when $δ > r$ and $P$ is a polynomial.

[F3]

Finite endpoint power substitution followed by Gauss–Jacobi quadrature: the left and right substitution orders $q_{a}, q_{b}$ and the shifted Gauss–Jacobi sums define the stated finite output.

[F4]

Error bound after endpoint power regularization: when the substituted functions are $C^{2 n}$ , the improper integral exists and the error is bounded by the displayed derivative constant.

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

[F6]

Continuity and derivatives of positive-base real powers, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , and The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ : real powers, products, and compositions have the derivatives used for the primitive below.

Proof

1.1F1F2F5F6algebra

A primitive on $(0, 1]$ is $P (x) = 2 \sqrt{x} \log x - 4 \sqrt{x}$ by [F1] and [F6]. The endpoint term $\sqrt{x} \log x$ tends to zero by the power-regularity lemma [F2] with $r = 0$ , $δ = 1 / 2$ , and polynomial $z$ . Hence $P (x) \to 0$ as $x ↓ 0$ . Applying [F5] on $[ε, 1]$ and taking $ε ↓ 0$ gives the improper integral $P (1) - 0 = - 4$ .

1.2F2F3givenalgebra

For the left substitution, $δ_{L} = q_{a} (α + 1) - 1 = 7 / 2 - 1 = 5 / 2 > 2$ ; its transformed function is a constant times $t^{5 / 2}$ times a polynomial of degree one in $\log t$ and a smooth factor bounded with two continuous derivatives. For the right substitution, $δ_{R} = q_{b} (β + 1) - 1 = 3 > 2$ and the remaining factors are smooth on $[0, 1]$ . Therefore both transformed functions are $C^{2}$ by [F2], and [F3] applies.

2.1F3F4step 1.1step 1.2∎

Apply [F4] with $n = 1$ to the functions in step 1.2. Its error constant is $C_{1}$ and the output is the stated sum, so the claimed error bound follows. The value $- 4$ from step 1.1 is the integral being approximated.

5 · Examples, counterexamples and false statements

None yet.

Singular and infinite interval quadrature — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

The Gaussian integral on the line with a certified sinh-sinh truncation tail

Statement

Facts & Assumptions

Proof

An interior Cauchy principal value reduces to a regular integral

Statement

Facts & Assumptions

Proof

A 1 over r singularity on the reference triangle

Statement

Facts & Assumptions

Proof

Gauss–Jacobi regularization for x to the minus one half times log x

Statement

Facts & Assumptions

Proof

5 · Examples, counterexamples and false statements

Sources