The logarithm as a limit of powers

This file shows that the logarithm can be expressed as a limit of powers, namely that p⁻¹ * (x ^ p - 1) tends to log x as p tends to zero for positive x.

Main declarations

• Real.tendstoLocallyUniformlyOn_rpow_sub_one_log: p⁻¹ * (x ^ p - 1) tends uniformly to log x on compact subsets of Ioi 0 as p tends to zero
• tendsto_rpow_sub_one_log: p⁻¹ * (x ^ p - 1): the analogous statement for pointwise convergence.

theorem Real.norm_inv_mul_rpow_sub_one_sub_log_le {p x : ℝ} (p_pos : 0 < p) (x_pos : 0 < x) (hx : ‖p * log x‖ ≤ 1) : ‖p⁻¹ * (x ^ p - 1) - log x‖ ≤ p * ‖log x‖ ^ 2

theorem Real.tendstoLocallyUniformlyOn_rpow_sub_one_log : TendstoLocallyUniformlyOn (fun (p x : ℝ) => p⁻¹ * (x ^ p - 1)) log (nhdsWithin 0 (Set.Ioi 0)) (Set.Ioi 0)

theorem tendsto_rpow_sub_one_log {x : ℝ} (hx : 0 < x) : Filter.Tendsto (fun (p : ℝ) => p⁻¹ * (x ^ p - 1)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (Real.log x))