Derivative and series expansion of real logarithm

In this file we prove that Real.log is infinitely smooth at all nonzero x : ℝ. We also prove that the series ∑' n : ℕ, x ^ (n + 1) / (n + 1) converges to (-Real.log (1 - x)) for all x : ℝ, |x| < 1.

Tags

logarithm, derivative

theorem Real.hasStrictDerivAt_log_of_pos {x : ℝ} (hx : 0 < x) : HasStrictDerivAt Real.log x⁻¹ x

theorem Real.hasStrictDerivAt_log {x : ℝ} (hx : x ≠ 0) : HasStrictDerivAt Real.log x⁻¹ x

theorem Real.hasDerivAt_log {x : ℝ} (hx : x ≠ 0) : HasDerivAt Real.log x⁻¹ x

theorem Real.differentiableAt_log {x : ℝ} (hx : x ≠ 0) : DifferentiableAt ℝ Real.log x

theorem Real.differentiableOn_log : DifferentiableOn ℝ Real.log {0}ᶜ

@[simp]

theorem Real.differentiableAt_log_iff {x : ℝ} : DifferentiableAt ℝ Real.log x ↔ x ≠ 0

theorem Real.deriv_log (x : ℝ) : deriv Real.log x = x⁻¹

@[simp]

theorem Real.deriv_log' : deriv Real.log = Inv.inv

theorem Real.contDiffAt_log {n : WithTop ℕ∞} {x : ℝ} : ContDiffAt ℝ n Real.log x ↔ x ≠ 0

theorem Real.contDiffOn_log {n : WithTop ℕ∞} : ContDiffOn ℝ n Real.log {0}ᶜ

theorem HasDerivWithinAt.log {f : ℝ → ℝ} {x f' : ℝ} {s : Set ℝ} (hf : HasDerivWithinAt f f' s x) (hx : f x ≠ 0) : HasDerivWithinAt (fun (y : ℝ) => Real.log (f y)) (f' / f x) s x

theorem HasDerivAt.log {f : ℝ → ℝ} {x f' : ℝ} (hf : HasDerivAt f f' x) (hx : f x ≠ 0) : HasDerivAt (fun (y : ℝ) => Real.log (f y)) (f' / f x) x

theorem HasStrictDerivAt.log {f : ℝ → ℝ} {x f' : ℝ} (hf : HasStrictDerivAt f f' x) (hx : f x ≠ 0) : HasStrictDerivAt (fun (y : ℝ) => Real.log (f y)) (f' / f x) x

theorem derivWithin.log {f : ℝ → ℝ} {x : ℝ} {s : Set ℝ} (hf : DifferentiableWithinAt ℝ f s x) (hx : f x ≠ 0) (hxs : UniqueDiffWithinAt ℝ s x) : derivWithin (fun (x : ℝ) => Real.log (f x)) s x = derivWithin f s x / f x

@[simp]

theorem deriv.log {f : ℝ → ℝ} {x : ℝ} (hf : DifferentiableAt ℝ f x) (hx : f x ≠ 0) : deriv (fun (x : ℝ) => Real.log (f x)) x = deriv f x / f x

theorem Real.deriv_log_comp_eq_logDeriv {f : ℝ → ℝ} {x : ℝ} (h₁ : DifferentiableAt ℝ f x) (h₂ : f x ≠ 0) : deriv (Real.log ∘ f) x = logDeriv f x

The derivative of log ∘ f is the logarithmic derivative provided f is differentiable and f x ≠ 0.

theorem HasFDerivWithinAt.log {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} {f' : E →L[ℝ] ℝ} {s : Set E} (hf : HasFDerivWithinAt f f' s x) (hx : f x ≠ 0) : HasFDerivWithinAt (fun (x : E) => Real.log (f x)) ((f x)⁻¹ • f') s x

theorem HasFDerivAt.log {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} {f' : E →L[ℝ] ℝ} (hf : HasFDerivAt f f' x) (hx : f x ≠ 0) : HasFDerivAt (fun (x : E) => Real.log (f x)) ((f x)⁻¹ • f') x

theorem HasStrictFDerivAt.log {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} {f' : E →L[ℝ] ℝ} (hf : HasStrictFDerivAt f f' x) (hx : f x ≠ 0) : HasStrictFDerivAt (fun (x : E) => Real.log (f x)) ((f x)⁻¹ • f') x

theorem DifferentiableWithinAt.log {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E} (hf : DifferentiableWithinAt ℝ f s x) (hx : f x ≠ 0) : DifferentiableWithinAt ℝ (fun (x : E) => Real.log (f x)) s x

@[simp]

theorem DifferentiableAt.log {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hf : DifferentiableAt ℝ f x) (hx : f x ≠ 0) : DifferentiableAt ℝ (fun (x : E) => Real.log (f x)) x

theorem ContDiffAt.log {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} {n : WithTop ℕ∞} (hf : ContDiffAt ℝ n f x) (hx : f x ≠ 0) : ContDiffAt ℝ n (fun (x : E) => Real.log (f x)) x

theorem ContDiffWithinAt.log {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E} {n : WithTop ℕ∞} (hf : ContDiffWithinAt ℝ n f s x) (hx : f x ≠ 0) : ContDiffWithinAt ℝ n (fun (x : E) => Real.log (f x)) s x

theorem ContDiffOn.log {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {n : WithTop ℕ∞} (hf : ContDiffOn ℝ n f s) (hs : ∀ x ∈ s, f x ≠ 0) : ContDiffOn ℝ n (fun (x : E) => Real.log (f x)) s

theorem ContDiff.log {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {n : WithTop ℕ∞} (hf : ContDiff ℝ n f) (h : ∀ (x : E), f x ≠ 0) : ContDiff ℝ n fun (x : E) => Real.log (f x)

theorem DifferentiableOn.log {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} (hf : DifferentiableOn ℝ f s) (hx : ∀ x ∈ s, f x ≠ 0) : DifferentiableOn ℝ (fun (x : E) => Real.log (f x)) s

@[simp]

theorem Differentiable.log {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hf : Differentiable ℝ f) (hx : ∀ (x : E), f x ≠ 0) : Differentiable ℝ fun (x : E) => Real.log (f x)

theorem fderivWithin.log {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E} (hf : DifferentiableWithinAt ℝ f s x) (hx : f x ≠ 0) (hxs : UniqueDiffWithinAt ℝ s x) : fderivWithin ℝ (fun (x : E) => Real.log (f x)) s x = (f x)⁻¹ • fderivWithin ℝ f s x

@[simp]

theorem fderiv.log {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hf : DifferentiableAt ℝ f x) (hx : f x ≠ 0) : fderiv ℝ (fun (x : E) => Real.log (f x)) x = (f x)⁻¹ • fderiv ℝ f x

theorem Real.tendsto_mul_log_one_plus_div_atTop (t : ℝ) : Filter.Tendsto (fun (x : ℝ) => x * Real.log (1 + t / x)) Filter.atTop (nhds t)

The function x * log (1 + t / x) tends to t at +∞.

theorem Real.abs_log_sub_add_sum_range_le {x : ℝ} (h : |x| < 1) (n : ℕ) : |∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + Real.log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)

A crude lemma estimating the difference between log (1-x) and its Taylor series at 0, where the main point of the bound is that it tends to 0. The goal is to deduce the series expansion of the logarithm, in hasSum_pow_div_log_of_abs_lt_1.

Porting note (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: use one of generic theorems about Taylor's series to prove this estimate.

theorem Real.hasSum_pow_div_log_of_abs_lt_one {x : ℝ} (h : |x| < 1) : HasSum (fun (n : ℕ) => x ^ (n + 1) / (↑n + 1)) (-Real.log (1 - x))

Power series expansion of the logarithm around 1.

theorem Real.hasSum_log_sub_log_of_abs_lt_one {x : ℝ} (h : |x| < 1) : HasSum (fun (k : ℕ) => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)) (Real.log (1 + x) - Real.log (1 - x))

Power series expansion of log(1 + x) - log(1 - x) for |x| < 1.

theorem Real.hasSum_log_one_add_inv {a : ℝ} (h : 0 < a) : HasSum (fun (k : ℕ) => 2 * (1 / (2 * ↑k + 1)) * (1 / (2 * a + 1)) ^ (2 * k + 1)) (Real.log (1 + a⁻¹))

Expansion of log (1 + a⁻¹) as a series in powers of 1 / (2 * a + 1).