Alphabeta MathHow 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.
Frullani's formula with its proper integral factor
Statement
Let , and let be continuous with finite limit . Then the mixed improper integral converges and where the factor on the right is a proper oriented Riemann integral.
Facts & Assumptions
Given: Positive and a continuous with finite limit at infinity.
Proper substitution applies on every compact interval away from zero (Substitution: if is differentiable on with integrable and is continuous on an interval containing , then ).
A continuous function approaches its value at zero uniformly after the arguments are restricted to the fixed compact interval between and (Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point).
The limit at infinity is uniform for when stays in that same positive compact interval (Limits at and , and infinite limits at a point).
Proper integral errors are bounded by interval length times a uniform bound (If on and both are integrable then ; and ).
Proof
Assume first . Substitution on and cancellation give the identity below. [L1]
By [L2] and [L4], the first proper integral tends to as . By [L3] and [L4], the second tends to as . The two limits exist independently, so the mixed improper integral converges and has the displayed value.
The case is zero on both sides. If , interchange in step 2.1; both the numerator and the oriented proper factor change sign.
Depends on
- Improper integrals over unbounded intervals
- Improper integrals at a finite singular endpoint
- Improper integrals with several singular ends
- 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'$
- Integrable functions on $[a,b]$ form a set closed under sums and scalar multiples, and $\int_a^b(\lambda f+\mu g) = \lambda\int_a^b f + \mu\int_a^b g$
- If $f \le g$ on $[a,b]$ and both are integrable then $\int_a^b f \le \int_a^b g$; and $m(b-a) \le \int_a^b f \le M(b-a)$
- Continuity of $f : A \to \mathbb{R}$ at a point of $A$ and on $A$: the $\varepsilon$-$\delta$ condition, its agreement with $\lim_{x \to c} f(x) = f(c)$ at a limit point, and continuity at an isolated point
- Limits at $+\infty$ and $-\infty$, and infinite limits at a point
- The integral with oriented limits: $\int_a^a f := 0$ and $\int_b^a f := -\int_a^b f$
- If $f,g$ are integrable on $[a,b]$ then so are $\lvert f\rvert$, $f^{2}$, $fg$, $\max(f,g)$ and $\min(f,g)$, and $\bigl\lvert\int_a^b f\bigr\rvert \le \int_a^b\lvert f\rvert$
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 105 results over 20 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, Frullani integral exercise (standard reference, not scraped)