Alphabeta MathThe Integral Logarithm and the Equivalence of Its Characterisations
About this page
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.
✓ 16 results · all verified · 0 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 16 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.
1 · Prerequisites
Abstract Algebra
Linear Algebra
Real Analysis
- Absolute and Conditional Convergence; Rearrangement; Products
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Countability and Uncountability
- Equivalent Forms of Completeness
- Foundations of the Real Numbers for Analysis
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Power Series and Real-Analytic Functions
- Properties of the Integral and the Working FTC
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Suprema and Infima
- The Derivative and the Mean Value Theorems
- The Exponential Function
- The Logarithm and General Powers
- The Riemann Integral: Definition and Integrability
- Topology of ℝ
Set Theory
2 · Logical flowchart
3 · Items
Definition
The integral logarithm L(x):=∫₁ˣdt/t for x>0
Theorem
The integral logarithm satisfies L'(x)=1/x for x>0 and L(1)=0
Corollary
The integral logarithm is continuous and strictly increasing on (0,∞)
Theorem
The integral logarithm satisfies L(xy)=L(x)+L(y) for all positive x and y
Corollary
L(1/x)=-L(x), L(xⁿ)=nL(x), and in particular L(2ⁿ)=nL(2)
Theorem
The integral logarithm is unbounded above and below
Theorem
L:(0,∞)→ℝ is a continuous strictly increasing bijection
Definition
The integral exponential E:ℝ→(0,∞) as the inverse of L
Corollary
The inverse E satisfies E(a+b)=E(a)E(b)
Theorem
The inverse E is differentiable, E'=E, and E(0)=1
Theorem
The integral exponential E is the published exponential function
Corollary
The integral logarithm L is the published natural logarithm
Corollary
The number e is the unique x>0 satisfying ∫₁ˣdt/t=1
Theorem
log is the unique continuous f:(0,∞)→ℝ with f(xy)=f(x)+f(y) and f(e)=1
Theorem
log is the unique f with f(xy)=f(x)+f(y) that is differentiable at 1 with f'(1)=1
Corollary
Every continuous f with f(xy)=f(x)+f(y) is f(x)=c log x for a unique c, including c=0
Lemma
The Mercator series, its value at 1 and the product law determine log on all positive reals, while the series alone is only local
Theorem
Five characterisations of the natural logarithm are equivalent: inverse exponential, integral, continued Mercator series, Landau root limit and the normalised functional equation
Remark