mathlib3 documentation

analysis.special_functions.log.deriv

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

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_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
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
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
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
@[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
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
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
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
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))
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
@[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))
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
@[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

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 : ) :
|(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.

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.

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.

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).