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