LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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 improper integral of a power at zero

Statement

For every real $γ > - 1$ , the improper Riemann integral of $x^{γ}$ on $(0, 1]$ converges and $\int_{0}^{1} x^{γ} d x = \frac{1}{γ + 1} .$

Facts & Assumptions

Given: A real exponent $γ > - 1$ .

[F1]

Real powers for positive bases, with the zero-base positive-exponent convention and The natural logarithm as the inverse of the exponential function: for $x > 0$ , $x^{γ} = \exp (γ \log x)$ and $\exp (\log x) = x$ .

[F2]

Continuity and derivatives of positive-base real powers: on $(0, \infty)$ , $x \mapsto x^{q}$ is continuous and differentiable with derivative $q x^{q - 1}$ for every real $q$ .

[F3]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: the natural logarithm is strictly increasing on $(0, \infty)$ .

[F4]

The exponential tends to $+ \infty$ at $+ \infty$ and to $0$ at $- \infty$ : $\exp (u) \to 0$ as $u \to - \infty$ .

[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 every closed interval $[ε, 1]$ with $ε > 0$ , the integral of a continuous derivative equals the endpoint increment of its primitive.

Proof

1.1givenF2F5algebra

Put $q = γ + 1 > 0$ . For $0 < ε < 1$ , the function $x \mapsto x^{q} / q$ is differentiable on $[ε, 1]$ with derivative $x^{q - 1} = x^{γ}$ by [F2]. Applying [F5] gives $\int_{ε}^{1} x^{γ} d x = (1 - ε^{q}) / q$ .

1.2givenF1F3F4algebra

As $ε ↓ 0$ , $\log ε \to - \infty$ : for any real $M$ , $0 < ε < \exp (M)$ implies $\log ε < M$ by [F1] and [F3]. Hence $q \log ε \to - \infty$ and $ε^{q} = \exp (q \log ε) \to 0$ by [F1] and [F4].

2.1givenstep 1.1step 1.2algebra∎

Taking $ε ↓ 0$ in step 1.1 using step 1.2 proves convergence of the improper integral and gives its value $1 / q = 1 / (γ + 1)$ .

Depends on

Used by

Dependency tree · two levels

32 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

J. Lebl, Basic Analysis I, §5.4.1–5.4.2, The logarithm and the exponential (standard reference, not scraped)