Derivative and series expansion of real logarithm #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source

theorem real.has_strict_deriv_at_log_of_pos {x : ℝ} (hx : 0 < x) :

has_strict_deriv_at real.log x⁻¹ x

source

theorem real.has_strict_deriv_at_log {x : ℝ} (hx : x ≠ 0) :

has_strict_deriv_at real.log x⁻¹ x

source

theorem real.has_deriv_at_log {x : ℝ} (hx : x ≠ 0) :

has_deriv_at real.log x⁻¹ x

source

theorem real.differentiable_at_log {x : ℝ} (hx : x ≠ 0) :

differentiable_at ℝ real.log x

source

theorem real.differentiable_on_log :

differentiable_on ℝ real.log {0}ᶜ

source

@[simp]

theorem real.differentiable_at_log_iff {x : ℝ} :

differentiable_at ℝ real.log x ↔ x ≠ 0

source

theorem real.deriv_log (x : ℝ) :

deriv real.log x = x⁻¹

source

@[simp]

theorem real.deriv_log' :

deriv real.log = has_inv.inv

source

theorem real.cont_diff_on_log {n : ℕ∞} :

cont_diff_on ℝ n real.log {0}ᶜ

source

theorem real.cont_diff_at_log {x : ℝ} {n : ℕ∞} :

cont_diff_at ℝ n real.log x ↔ x ≠ 0

source

theorem has_deriv_within_at.log {f : ℝ → ℝ} {x f' : ℝ} {s : set ℝ} (hf : has_deriv_within_at f f' s x) (hx : f x ≠ 0) :

has_deriv_within_at (λ (y : ℝ), real.log (f y)) (f' / f x) s x

source

theorem has_deriv_at.log {f : ℝ → ℝ} {x f' : ℝ} (hf : has_deriv_at f f' x) (hx : f x ≠ 0) :

has_deriv_at (λ (y : ℝ), real.log (f y)) (f' / f x) x

source

theorem has_strict_deriv_at.log {f : ℝ → ℝ} {x f' : ℝ} (hf : has_strict_deriv_at f f' x) (hx : f x ≠ 0) :

has_strict_deriv_at (λ (y : ℝ), real.log (f y)) (f' / f x) x

source

theorem deriv_within.log {f : ℝ → ℝ} {x : ℝ} {s : set ℝ} (hf : differentiable_within_at ℝ f s x) (hx : f x ≠ 0) (hxs : unique_diff_within_at ℝ s x) :

deriv_within (λ (x : ℝ), real.log (f x)) s x = deriv_within f s x / f x

source

@[simp]

theorem deriv.log {f : ℝ → ℝ} {x : ℝ} (hf : differentiable_at ℝ f x) (hx : f x ≠ 0) :

deriv (λ (x : ℝ), real.log (f x)) x = deriv f x / f x

source

theorem has_fderiv_within_at.log {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E → ℝ} {x : E} {f' : E →L[ℝ ] ℝ} {s : set E} (hf : has_fderiv_within_at f f' s x) (hx : f x ≠ 0) :

has_fderiv_within_at (λ (x : E), real.log (f x)) ((f x)⁻¹ • f') s x

source

theorem has_fderiv_at.log {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E → ℝ} {x : E} {f' : E →L[ℝ ] ℝ} (hf : has_fderiv_at f f' x) (hx : f x ≠ 0) :

has_fderiv_at (λ (x : E), real.log (f x)) ((f x)⁻¹ • f') x

source

theorem has_strict_fderiv_at.log {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E → ℝ} {x : E} {f' : E →L[ℝ ] ℝ} (hf : has_strict_fderiv_at f f' x) (hx : f x ≠ 0) :

has_strict_fderiv_at (λ (x : E), real.log (f x)) ((f x)⁻¹ • f') x

source

theorem differentiable_within_at.log {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E → ℝ} {x : E} {s : set E} (hf : differentiable_within_at ℝ f s x) (hx : f x ≠ 0) :

differentiable_within_at ℝ (λ (x : E), real.log (f x)) s x

source

@[simp]

theorem differentiable_at.log {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E → ℝ} {x : E} (hf : differentiable_at ℝ f x) (hx : f x ≠ 0) :

differentiable_at ℝ (λ (x : E), real.log (f x)) x

source

theorem cont_diff_at.log {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E → ℝ} {x : E} {n : ℕ∞} (hf : cont_diff_at ℝ n f x) (hx : f x ≠ 0) :

cont_diff_at ℝ n (λ (x : E), real.log (f x)) x

source

theorem cont_diff_within_at.log {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E → ℝ} {x : E} {s : set E} {n : ℕ∞} (hf : cont_diff_within_at ℝ n f s x) (hx : f x ≠ 0) :

cont_diff_within_at ℝ n (λ (x : E), real.log (f x)) s x

source

theorem cont_diff_on.log {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E → ℝ} {s : set E} {n : ℕ∞} (hf : cont_diff_on ℝ n f s) (hs : ∀ (x : E), x ∈ s → f x ≠ 0) :

cont_diff_on ℝ n (λ (x : E), real.log (f x)) s

source

theorem cont_diff.log {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E → ℝ} {n : ℕ∞} (hf : cont_diff ℝ n f) (h : ∀ (x : E), f x ≠ 0) :

cont_diff ℝ n (λ (x : E), real.log (f x))

source

theorem differentiable_on.log {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E → ℝ} {s : set E} (hf : differentiable_on ℝ f s) (hx : ∀ (x : E), x ∈ s → f x ≠ 0) :

differentiable_on ℝ (λ (x : E), real.log (f x)) s

source

@[simp]

theorem differentiable.log {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E → ℝ} (hf : differentiable ℝ f) (hx : ∀ (x : E), f x ≠ 0) :

differentiable ℝ (λ (x : E), real.log (f x))

source

theorem fderiv_within.log {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E → ℝ} {x : E} {s : set E} (hf : differentiable_within_at ℝ f s x) (hx : f x ≠ 0) (hxs : unique_diff_within_at ℝ s x) :

fderiv_within ℝ (λ (x : E), real.log (f x)) s x = (f x)⁻¹ • fderiv_within ℝ f s x

source

@[simp]

theorem fderiv.log {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {f : E → ℝ} {x : E} (hf : differentiable_at ℝ f x) (hx : f x ≠ 0) :

fderiv ℝ (λ (x : E), real.log (f x)) x = (f x)⁻¹ • fderiv ℝ f x

source

theorem real.tendsto_mul_log_one_plus_div_at_top (t : ℝ) :

filter.tendsto (λ (x : ℝ), x * real.log (1 + t / x)) filter.at_top (nhds t)

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

source

theorem real.abs_log_sub_add_sum_range_le {x : ℝ} (h : |x| < 1) (n : ℕ) :

|(finset.range n).sum (λ (i : ℕ), 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 has_sum_pow_div_log_of_abs_lt_1.

source

theorem real.has_sum_pow_div_log_of_abs_lt_1 {x : ℝ} (h : |x| < 1) :

has_sum (λ (n : ℕ), x ^ (n + 1) / (↑n + 1)) (-real.log (1 - x))

Power series expansion of the logarithm around 1.

source

theorem real.has_sum_log_sub_log_of_abs_lt_1 {x : ℝ} (h : |x| < 1) :

has_sum (λ (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.

source

theorem real.has_sum_log_one_add_inv {a : ℝ} (h : 0 < a) :

has_sum (λ (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).