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

Direct midpoint quadrature loses order on a half-order singularity

Example

At $x = 0$ , take the weakly singular kernel $s (0, y) = y^{- 1 / 2}$ and smooth factor $a \equiv 1$ , $u \equiv 1$ . The exact integral is $2$ . The composite midpoint rule on panels of width $h = 1 / N$ underestimates it by at least $(2 - \sqrt{2}) \sqrt{h},$ so direct midpoint sampling of this singular integrand is not second order. The product-integration rule of Piecewise-linear product integration for a half-order diagonal singularity is exact for this constant smooth factor, because its interpolant is identically $1$ .

Facts & Assumptions

Given: $N \geq 1$ , $h = 1 / N$ , the function $g (y) = y^{- 1 / 2}$ on $(0, 1]$ , its improper integral, and the product-integration rule from the A page. For the midpoint algorithm, use the extension $\tilde{g} : [0, 1] \to R$ given by $\tilde{g} (0) = 0$ and $\tilde{g} (y) = g (y)$ for $y > 0$ .

[F1]

The half-order diagonal singularity defines a bounded improper integral: $\int_{0}^{1} y^{- 1 / 2} d y = 2$ and the product weights integrate the constant function with their total weight $S_{0} (1) = 2$ .

[F2]

Piecewise-linear product integration for a half-order diagonal singularity: $K_{n} u (0) = S_{0} (I_{n} g_{0})$ and the hats form the piecewise-linear interpolant.

[F3]

Composite midpoint rule on a uniform grid applies to the everywhere evaluable function $\tilde{g}$ and uses $\tilde{g} ((j + \frac{1}{2}) h) = g ((j + \frac{1}{2}) h)$ on each panel with weight $h$ . No endpoint is sampled, and the assigned value at zero does not enter the improper integral.

[F4]

On $(0, \infty)$ , $g (y) = y^{- 1 / 2}$ is $C^{2}$ with $g^{'} (y) = - \frac{1}{2} y^{- 3 / 2}$ and $g^{''} (y) = \frac{3}{4} y^{- 5 / 2} > 0$ ; positive-base powers are exponentials and the exponential is positive (Continuity and derivatives of positive-base real powers, Real powers for positive bases, with the zero-base positive-exponent convention, The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ ).

[F5]

The mean value theorem on a closed interval gives a point where the derivative equals the secant slope (Mean value theorem on a closed real interval).

[F6]

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

[F7]

Integrals add when a closed interval is split at an interior point (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$ ).

[F8]

A nonnegative integrable function has nonnegative integral (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)$ ).

[F9]

Differentiating compositions, sums, and scalar multiples uses the chain rule and algebra of derivatives (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)$ , 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$ ).

Verification

Given: The data in the Example, $m_{j} : = (j + \frac{1}{2}) h$ , $g (y) = y^{- 1 / 2}$ for $y > 0$ , and the extension $\tilde{g}$ above.

1.1givenF1F3algebra

Since every $m_{j} > 0$ , the admissible call $Q_{M} (\tilde{g}; 0, 1, N)$ equals $h \sum_{j = 0}^{N - 1} g (m_{j})$ by [F3]. On the first panel, the substitution $y = h t$ gives $\int_{0}^{h} y^{- 1 / 2} d y = \sqrt{h} \int_{0}^{1} t^{- 1 / 2} d t = 2 \sqrt{h}$ by [F1]; this substitution follows by scaling tagged sums on each truncated interval and then taking the improper limit. The midpoint contribution is $h g (h / 2) = \sqrt{2} \sqrt{h}$ . Their difference is $(2 - \sqrt{2}) \sqrt{h}$ .

2.1givenF3F4F5F6F7F8F9step 1.1algebra

For every later panel $[j h, (j + 1) h]$ , $j \geq 1$ , the function $g$ is $C^{2}$ by [F4]. Its second derivative is positive because $y^{- 5 / 2} = \exp ((- 5 / 2) \log y) > 0$ for $y > 0$ , using [F4]. The mean value theorem [F5] applied to $g^{'}$ shows that $g^{'}$ is increasing there. For $0 \leq s \leq h / 2$ , put $D (s) : = g (m_{j} - s) + g (m_{j} + s) - 2 g (m_{j})$ . By [F9], $D^{'} (s) = - g^{'} (m_{j} - s) + g^{'} (m_{j} + s) \geq 0$ in the interior; another application of [F5] on $[0, s]$ gives $D (s) \geq D (0) = 0$ . Splitting at $m_{j}$ and substituting $y = m_{j} - s$ and $y = m_{j} + s$ gives $\int_{j h}^{(j + 1) h} g (y) d y - h g (m_{j}) = \int_{0}^{h / 2} D (s) d s$ : the left substitution reverses the limits, while the right preserves them, and each has Jacobian magnitude $1$ . Thus the integral identity follows directly from the tagged Riemann sums under these affine maps. The integrals exist by [F6], the split at $m_{j}$ is additive by [F7], and the nonnegative difference integrates to at least zero by [F8]. Thus no later panel cancels the positive first-panel error, and the total midpoint error is at least $(2 - \sqrt{2}) \sqrt{h}$ .

3.1F1F2step 1.1∎

For the product rule, $a \equiv 1$ and $u \equiv 1$ give $g_{0} \equiv 1$ . On each panel the two adjacent hat formulas in [F2] sum to $1$ , so $I_{n} g_{0} = 1$ . By [F1] and [F2], $K_{n} u (0) = S_{0} (1) = 2 = K u (0)$ . Hence this case is exact under product integration although direct midpoint sampling has only the lower-bound rate above.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

70 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

Jiri Lebl, Basic Analysis I, §5.5 Improper Integrals (standard reference, not scraped)
Andreas Neubauer and Ronny Ramlau, Lecture Notes: Integral Equations and Boundary Value Problems, §3.3 (standard reference, not scraped)