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.
Change of variable in an improper integral
Statement
Let and be intervals, possibly open at finite or infinite singular ends, and let be a monotone differentiable surjection. Assume is locally Riemann integrable and the proper change-of-variable hypotheses hold on every compact truncation. If is locally Riemann integrable on , then converge simultaneously and, when convergent, are equal. At several singular ends this assertion is applied separately to the corresponding ends; orientation is retained for decreasing parametrizations.
Facts & Assumptions
Given: The intervals, monotone surjection , and locally integrable in the statement.
The proper change-of-variable theorem gives equality on corresponding compact truncations (Monotone change of variable for Riemann-integrable functions).
Monotonicity and surjectivity send truncations tending to an endpoint of to truncations tending to the corresponding endpoint of .
Improper convergence at one end is the existence of a finite limit of the corresponding compact-truncation values (Improper integrals over unbounded intervals, Improper integrals at a finite singular endpoint).
Mixed improper integrals require separate convergence at every singular end (Improper integrals with several singular ends).
Proof
On each compact source truncation , [L1] gives [L1] with the endpoint order adjusted when decreases.
By [L2], the two sides form the same family of values as the corresponding truncation approaches a singular end. Since they are equal term by term by step 1.1, the epsilon condition in [L3] holds for one family exactly when it holds for the other, with the same limit.
For multiple ends, apply step 2.1 separately at each matched end and add only after all pieces converge, as [L4] requires. The oriented convention supplies the sign for a decreasing parametrization.
Depends on
- Monotone change of variable for Riemann-integrable functions
- Improper integrals over unbounded intervals
- Improper integrals at a finite singular endpoint
- Improper integrals with several singular ends
- Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $\mathbb{R}$, with the dictionary to monotone sequences
- The derivative $f'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c}$ of $f : A \to \mathbb{R}$ at a point $c \in A$ that is a limit point of $A$, and differentiability on a set
- The integral with oriented limits: $\int_a^a f := 0$ and $\int_b^a f := -\int_a^b f$
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 83 results over 17 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, Theorem 3.4.13 (standard reference, not scraped)