Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21
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 ex2 over R is finite and positive

Statement

The integral I=ex2dx exists as a finite positive real number.

Facts & Assumptions

Given: The real exponential function and the mixed-improper convention on the real line.

[L2]

The improper integral 1xpdx converges exactly when the rational p>1 (The improper p-test for rational exponents).

[L3]

For every real u, exp(u)>0 and exp(u)=1/exp(u) (The exponential is positive and satisfies exp(x)=1/exp(x)).

[L4]

Improper integrals at and + must converge separately before they are added (Improper integrals with several singular ends).

[L5]

If 0uv toward a singular end and the improper integral of v converges there, then the improper integral of u converges there (Comparison tests for improper integrals).

[L6]

The exponential function is strictly increasing on R (The exponential function is strictly increasing).

[L8]

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

[L9]

A valid C1 substitution carries a convergent improper integral to the corresponding transformed improper integral (Change of variable in an improper integral).

Proof

technique · direct
1.1

If x1, then [L1] and [L3] give 0<ex21/(1+x2)x2. The p-test [L2] and comparison [L5] make the positive tail converge, and the substitution u=x in [L9] gives the identical negative-tail estimate.

L1L2L3L5L9
1.2

On [1,1], the integrand is continuous and hence integrable by [L8]; [L6] gives ex2e1>0, so [L7] gives 11ex2dx2e1>0.

L3L6L7L8
2.1

By [L4], the two finite tails and the proper middle integral combine to a finite mixed improper integral, and step 1.2 makes the total strictly positive.

step 1.1step 1.2L4

Depends on

Used by

Dependency tree · two levels

61 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