Real logarithm #
In this file we define
Real.log to be the logarithm of a real number. As usual, we extend it from
(0, +∞) to a globally defined function. We choose to do it so that
log 0 = 0 and
log (-x) = log x.
We prove some basic properties of this function and show that it is continuous.
The real logarithm function, equal to the inverse of the exponential for
x > 0,
log |x| for
x < 0, and to
0. We use this unconventional extension to
(-∞, 0] as it gives the formula
log (x * y) = log x + log y for all nonzero
the derivative of
1/x away from