Multiplicative inverse and iteration of real logarithm

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

Main results

• deriv_inv_log gives a formula for the derivative of x ↦ (log x)⁻¹ which holds for all values.
• deriv_log_log gives a formula for the derivative of x ↦ log (log x) 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_apply {x : ℝ} : deriv (fun (x : ℝ) => (log x)⁻¹) x = -x⁻¹ / log x ^ 2

@[simp]

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

theorem Real.differentiableAt_inv_log {x : ℝ} (hx₀ : x ≠ 0) (hx₁ : x ≠ 1) (hx₂ : x ≠ -1) : DifferentiableAt ℝ (fun (x : ℝ) => (log x)⁻¹) x

theorem Real.hasDerivAt_inv_log {x : ℝ} (hx₀ : x ≠ 0) (hx₁ : x ≠ 1) (hx₂ : x ≠ -1) : HasDerivAt (fun (x : ℝ) => (log x)⁻¹) (-x⁻¹ / log x ^ 2) x

theorem Real.differentiableOn_inv_log' : DifferentiableOn ℝ (fun (x : ℝ) => (log x)⁻¹) {-1, 0, 1}ᶜ

theorem Real.differentiableOn_inv_log : DifferentiableOn ℝ (fun (x : ℝ) => (log x)⁻¹) (Set.Ioi 1)

theorem Real.inv_log_isLittleO_one : (fun (x : ℝ) => (log x)⁻¹) =o[Filter.atTop] fun (x : ℝ) => 1

theorem Real.not_continuousAt_log_log_zero : ¬ContinuousAt (fun (x : ℝ) => log (log x)) 0

theorem Real.not_continuousAt_log_log_one : ¬ContinuousAt (fun (x : ℝ) => log (log x)) 1

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

theorem Real.deriv_log_log_apply {x : ℝ} : deriv (fun (x : ℝ) => log (log x)) x = x⁻¹ / log x

@[simp]

theorem Real.deriv_log_log : (deriv fun (x : ℝ) => log (log x)) = fun (x : ℝ) => x⁻¹ / log x

theorem Real.differentiableAt_log_log {x : ℝ} (hx₀ : x ≠ 0) (hx₁ : x ≠ 1) (hx₂ : x ≠ -1) : DifferentiableAt ℝ (fun (x : ℝ) => log (log x)) x

theorem Real.hasDerivAt_log_log {x : ℝ} (hx₀ : x ≠ 0) (hx₁ : x ≠ 1) (hx₂ : x ≠ -1) : HasDerivAt (fun (x : ℝ) => log (log x)) (x⁻¹ / log x) x

theorem Real.differentiableOn_log_log' : DifferentiableOn ℝ (fun (x : ℝ) => log (log x)) {-1, 0, 1}ᶜ

theorem Real.differentiableOn_log_log : DifferentiableOn ℝ (fun (x : ℝ) => log (log x)) (Set.Ioi 1)

theorem Real.one_isLittleO_log_log : (fun (x : ℝ) => 1) =o[Filter.atTop] fun (x : ℝ) => log (log x)