LemmaStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11

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.

Truncated integrals of rational powers

Statement

For rational $p\ne1$ and $0<A<B$ , $\int_A^B x^{-p}\,dx=\frac{B^{1-p}-A^{1-p}}{1-p}.$ For $p=1$ and every positive integer $N$ , $\int_1^{2^N}\frac{dx}{x}\ge\frac N2,\qquad \int_{2^{-N}}^1\frac{dx}{x}\ge\frac N2.$

Facts & Assumptions

Given: Positive endpoints $A<B$ and the stated rational exponent.

[L1]

Positive rational powers satisfy the exponent, product, and monotonicity laws (Rational powers $a^r$ of a positive base, Laws of rational exponents, Monotonicity of $r \mapsto a^{r}$ and of $a \mapsto a^{r}$ ).

[L2]

Proper substitution and the FTC evaluate integrals from verified primitives (Substitution: if $\varphi$ is differentiable on $[c,d]$ with $\varphi'$ integrable and $f$ is continuous on an interval containing $\varphi([c,d])$ , then $\int_{\varphi(c)}^{\varphi(d)} f = \int_c^d (f\circ\varphi)\,\varphi'$ , 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)$ ).

[L3]

Integer-power differentiation, the product rule, and the reciprocal rule follow from the derivative algebra (Integer powers $a^m$ , Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$ , $(\alpha f)'(c) = \alpha f'(c)$ , $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$ , and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$ ).

Proof

technique · computation

1.1

Write $p=m/q$ with an integer $m$ and a positive integer $q$ . Substituting $x=t^q$ on the positive interval and using [L1]–[L3] reduces the integrand to $qt^{q-m-1}$ . The integer-power rule gives primitive $qt^{q-m}/(q-m)$ when $m\ne q$ . Substituting $t=x^{1/q}$ back gives $x^{1-p}/(1-p)$ . The FTC proves the displayed formula.

L1L2L3

2.1

On $[2^k,2^{k+1}]$ , $1/x\ge2^{-(k+1)}$ , so its integral is at least $1/2$ . Adding the first $N$ dyadic blocks proves the first lower bound. The intervals $[2^{-(k+1)},2^{-k}]$ give the second in the same way.

given∎

Depends on

Used by

1/x² has no finite Cauchy principal value at zero Counterexample
|x-c|^-1/2 has a convergent improper integral across an interior singularity Example
∫₀¹ x^-1/2 dx=2 Example
The rational p-threshold reverses between zero and infinity Example
The improper p-test for rational exponents Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 136 results over 33 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

William F. Trench, Introduction to Real Analysis, Examples 3.4.1–3 (standard reference, not scraped)