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.
The natural logarithm as the inverse of the exponential function
Definition
For , define to be the unique real such that . This is well-defined because The exponential is a continuous bijection from onto states that is a bijection.
Thus is the inverse function of . In particular, for every and for every .
Definition references
Remarks
The domain is exactly . This definition assigns no real logarithm to or to a negative number.
Depends on
Used by
- Finite endpoint power substitution followed by Gauss–Jacobi quadrature Algorithm
- Finite-candidate information design Algorithm
- Finite-horizon upper-confidence-bound bandit algorithm Algorithm
- LinUCB with a self-normalized confidence radius Algorithm
- Validation temperature scaling Algorithm
- Variance-aware quantum Monte Carlo Algorithm
- A PAC-Bayes bound for a finite tuning grid Corollary
- A sample-size consequence for compression schemes Corollary
- Compatible extensions from the finite simple core Corollary
- ERM excess risk from Rademacher uniform deviation Corollary
- LinUCB has expected pseudo-regret of order d√n log(nL) Corollary
- One-sample natural error in the Gaussian model Corollary
- Polynomial and exponential minimax estimation rates Corollary
- The integral logarithm L is the published natural logarithm Corollary
- The principal logarithm is the normalised holomorphic branch on the slit plane Corollary
- The winding number is the increment of a continuous argument divided by 2π Corollary
- A data-dependent prior can invalidate the PAC-Bayes bound Counterexample
- Assuming choice, a Hamel-basis additive map transported through exp gives a discontinuous logarithmic function that is not c log Counterexample
- Disconnected comparison support does not identify Gibbs policy mass Counterexample
- Equal posterior means do not control the full posterior Counterexample
- Fidelity and trace-distance inequalities do not imply QRE data processing Counterexample
- Knapp rules out extension below the Tomas exponent Counterexample
- Point evaluation is unbounded below the Sobolev continuity threshold Counterexample
- Subcritical W^1,p is not closed under multiplication Counterexample
- The claimed univariate clean-quantile count exponent is too strong Counterexample
- The critical Riesz potential can diverge and be essentially unbounded Counterexample
- The logarithm is not uniformly continuous on the positive half-line Counterexample
- Zero reference support makes the DPO reward ratio undefined Counterexample
- Average-cost fixed-length codes and operational DMC capacity Definition
- Causal feedback codes for a finite cost-constrained DMC Definition
- Causal feedback codes for a finite-dimensional Gaussian channel Definition
- Chebyshev's theta function Definition
- Complex logarithms, the principal logarithm, and principal and multivalued complex powers Definition
- Density-defined Jensen–Shannon divergence Definition
- Dirichlet series Definition
- Finite DMC information density Definition
- Finite DMC with a nonnegative input cost and feasible budget Definition
- Finite KL-regularized policy improvement Definition
- Finite Kullback–Leibler divergence Definition
- Finite Rényi divergence Definition
…and 262 more results.
Dependency tree · two levels
5 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
- J. Lebl, Basic Analysis, Logarithm and Exponential (standard reference, not scraped)
- MIT OpenCourseWare 18.100B Real Analysis, Spring 2025 full lecture notes (standard reference, not scraped)