ThmDex – An index of mathematical definitions, results, and conjectures.
Set of symbols
Alphabet
Deduction system
Theory
Zermelo-Fraenkel set theory
Set
Binary cartesian set product
Binary relation
Binary endorelation
Preordering relation
Partial ordering relation
Partially ordered set
Closed interval
Implicit interval partition
Implicit basic real interval partition
Closed real interval tagged partition
Stieltjes sum
Riemann sum
Riemann integrable real function
Real Riemann integral
Standard natural real logarithm function
Definition D866
Standard real logarithm function
Formulation 0
Let $x \mapsto \log(x)$ be the D865: Standard natural real logarithm function.
The standard real logarithm function in base $a \in (0, \infty) \setminus \{ 1 \}$ is the D5482: Positive real function \begin{equation} \log_a : (0, \infty) \to \mathbb{R}, \quad \log_a(x) = \frac{\log x}{\log a} \end{equation}
Formulation 1
Let $x \mapsto \log_e(x)$ be the D865: Standard natural real logarithm function.
The standard real logarithm function in base $a \in (0, \infty) \setminus \{ 1 \}$ is the D5482: Positive real function \begin{equation} \log_a : (0, \infty) \to \mathbb{R}, \quad \log_a(x) = \frac{\log_e x}{\log_e a} \end{equation}
Children
D5706: Real entropy function
Results
R4830: Change of base formula for logarithm function
R4831: Homomorphism property of standard logarithm function
R4832: Homomorphism property of standard logarithm function in the binary case
R4826: Logarithm of a ratio
R4855: Reflection property of standard logarithm function
R5662: Reflection property of standard logarithm function for a single positive real number
R4857: Standard logarithm of a positive real number raised to an integer power
R3232: Value of standard logarithm function at its parameter value