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.
The integral logarithm is the published natural logarithm
Statement
For every ,
Facts & Assumptions
Given: .
The natural logarithm is the inverse of the bijection (The natural logarithm as the inverse of the exponential function).
Proof
By [F1] and [L1], is an inverse of .
Inverse functions are unique, so [F2] and step 1.1 give for every .
Depends on
Used by
- Every continuous f with f(xy)=f(x)+f(y) is f(x)=c log x for a unique c, including c=0 Corollary
- Kullback–Leibler divergence Definition
- A sparse Gaussian sequence lower bound by Fano’s method Example
- Finite evidence and finite expected logs do not replace admissibility Example
- A sparse Hamming packing for every 1≤ k≤ d/2 Lemma
- A weighted total-variation bound from relative entropy Lemma
- Coherent spectral minimum and a frozen Gibbs energy shift Lemma
- Finite KL nonnegativity for subprobability references Lemma
- Additive spectral-estimation accuracy and cost Theorem
- Extremal length of the rectangle and of the round annulus Theorem
- Fano’s packing bound with a reference-distribution KL bound Theorem
- Five characterisations of the natural logarithm are equivalent: inverse exponential, integral, continued Mercator series, Landau root limit and the normalised functional equation Theorem
- Gaussian sparse-sequence minimax lower bound Theorem
- Kullback–Leibler divergence is nonnegative 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 Theorem
- Pinsker’s inequality with event-supremum total variation Theorem
- The conformal parameter of a round annulus is a complete invariant Theorem
Dependency tree · two levels
8 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
- OpenStax, Calculus Volume 1, Section 6.7 (standard reference, not scraped)