Multiplicative inverse of real logarithm

We prove properties of the function x ↦ (log x)⁻¹.

Main results

• deriv_inv_log gives a formula for the derivative which holds for all values.

theorem Real.not_differentiableAt_inv_log_zero : ¬DifferentiableAt ℝ (fun (x : ℝ) => (log x)⁻¹) 0

theorem Real.not_continuousAt_inv_log_one : ¬ContinuousAt (fun (x : ℝ) => (log x)⁻¹) 1

theorem Real.not_continuousAt_inv_log_neg_one : ¬ContinuousAt (fun (x : ℝ) => (log x)⁻¹) (-1)

theorem Real.deriv_inv_log {x : ℝ} : deriv (fun (x : ℝ) => (log x)⁻¹) x = -x⁻¹ / log x ^ 2