mathlib documentation

analysis.special_functions.log_deriv

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 #

logarighm, derivative

theorem real.has_deriv_at_log {x : } (hx : x 0) :
theorem real.deriv_log (x : ) :
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
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
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
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
@[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
theorem has_fderiv_within_at.log {E : Type u_1} [normed_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
theorem has_fderiv_at.log {E : Type u_1} [normed_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
theorem has_strict_fderiv_at.log {E : Type u_1} [normed_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
theorem differentiable_within_at.log {E : Type u_1} [normed_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
@[simp]
theorem differentiable_at.log {E : Type u_1} [normed_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
theorem times_cont_diff_at.log {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {n : with_top } (hf : times_cont_diff_at n f x) (hx : f x 0) :
times_cont_diff_at n (λ (x : E), real.log (f x)) x
theorem times_cont_diff_within_at.log {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : times_cont_diff_within_at n f s x) (hx : f x 0) :
times_cont_diff_within_at n (λ (x : E), real.log (f x)) s x
theorem times_cont_diff_on.log {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} {n : with_top } (hf : times_cont_diff_on n f s) (hs : ∀ (x : E), x sf x 0) :
times_cont_diff_on n (λ (x : E), real.log (f x)) s
theorem times_cont_diff.log {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } (hf : times_cont_diff n f) (h : ∀ (x : E), f x 0) :
times_cont_diff n (λ (x : E), real.log (f x))
theorem differentiable_on.log {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} (hf : differentiable_on f s) (hx : ∀ (x : E), x sf x 0) :
differentiable_on (λ (x : E), real.log (f x)) s
@[simp]
theorem differentiable.log {E : Type u_1} [normed_group E] [normed_space E] {f : E → } (hf : differentiable f) (hx : ∀ (x : E), f x 0) :
differentiable (λ (x : E), real.log (f x))
theorem fderiv_within.log {E : Type u_1} [normed_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
@[simp]
theorem fderiv.log {E : Type u_1} [normed_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

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 : ) in 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 has_sum_pow_div_log_of_abs_lt_1.

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.