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 log x⁻¹ x

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

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

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

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

@[simp]

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

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

@[simp]

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

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

theorem Real.contDiffOn_log {n : WithTop ℕ∞} : ContDiffOn ℝ n 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 (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' : StrongDual ℝ E} {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' : StrongDual ℝ E} (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' : StrongDual ℝ E} (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.abs_log_sub_add_sum_range_le {x : ℝ} (h : |x| < 1) (n : ℕ) : |∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + 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.

TODO: use one of generic theorems about Taylor's series to prove this estimate.

theorem Real.hasDerivAt_half_log_one_add_div_one_sub_sub_sum_range {y : ℝ} (n : ℕ) (hy₁ : -1 < y) (hy₂ : y < 1) : HasDerivAt (fun (x : ℝ) => 1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1)) ((y ^ 2) ^ n / (1 - y ^ 2)) y

Compute the derivative of the difference between $\frac{1}{2} * \log(\frac{1+x}{1-x})$ and its Taylor series at 0 up to order n. This is an auxiliary lemma for sum_range_sub_log_div_le and sum_range_le_log_div. Note that thanks to the geometric series, the derivative has a particularly simple form, and means that it is more convenient to avoid Taylor's theorem.

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

A lemma estimating the difference between $\frac{1}{2} * \log(\frac{1+x}{1-x})$ and its Taylor series at 0, where the bound tends to 0. This bound is particularly useful for explicit estimates of logarithms.

Note that thanks to the geometric series, the derivative has a particularly simple form, and means that it is more convenient to avoid Taylor's theorem for this proof.

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

For 0 ≤ x < 1, the partial sums of the series expansion of $\frac{1}{2} * \log(\frac{1+x}{1-x})$ at 0 form a lower bound for it. This shows that the absolute value in sum_range_sub_log_div_le can be dropped, and gives explicit lower bounds for logarithms.

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

theorem Real.hasSum_pow_div_log_of_abs_lt_one {x : ℝ} (h : |x| < 1) : HasSum (fun (n : ℕ) => x ^ (n + 1) / (↑n + 1)) (-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)) (log (1 + x) - 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)) (log (1 + a⁻¹))

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

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

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

theorem Real.le_log_one_add_of_nonneg {x : ℝ} (hx : 0 ≤ x) : 2 * x / (x + 2) ≤ log (1 + x)

theorem Real.lt_log_one_add_of_pos {x : ℝ} (hx : 0 < x) : 2 * x / (x + 2) < log (1 + x)