ExampleConstruction: Literature-sourcedVerification: Literature-sourcedSession-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.

Fubini computes $\int_0^1\int_{-1}^1 x\exp(xy)\,dx\,dy$ by reversing the order

Example

The continuous integrand $x\exp(xy)$ satisfies $\int_0^1\int_{-1}^1x\exp(xy)\,dx\,dy=e-e^{-1}-2.$ Reversing the order avoids an awkward antiderivative in $x$ .

Facts & Assumptions

Given: The displayed integral over $[-1,1]\times[0,1]$ .

[L1]

A continuous function on a rectangle may be integrated in either repeated order (A continuous function on a closed rectangle has repeated Riemann integrals in every coordinate order, all equal to its multiple integral).

[L2]

The derivative of the exponential is the exponential (The exponential function is smooth and $(\exp)'=\exp$ ), and the second fundamental theorem evaluates integrals of derivatives (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]

Exponential values are positive and $\exp(-1)=\exp(1)^{-1}$ (The exponential is positive and satisfies $\exp(-x)=1/\exp(x)$ ).

Verification

technique · computation

1.1

By continuity and [L1], reverse the order and integrate in $y$ first. Since $\partial_y\exp(xy)=x\exp(xy)$ , [L2] gives $\int_0^1x\exp(xy)\,dy=e^x-1$ , including $x=0$ .

L1L2

2.1

A second application of [L2] gives $\int_{-1}^1(e^x-1)\,dx=(e-e^{-1})-2.$

L2step 1.1

3.1

Using [L3] for the negative endpoint yields the stated value $e-e^{-1}-2$ .

L3step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 112 results over 19 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

J. Lebl, Basic Analysis II, Exercise 10.2.1 (standard reference, not scraped)

Fubini computes ∫01∫−11xexp⁡(xy) dx dy\int_0^1\int_{-1}^1 x\exp(xy)\,dx\,dy∫01​∫−11​xexp(xy)dxdy by reversing the order