Documentation

Mathlib.Analysis.SpecialFunctions.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 #

logarithm, derivative

@[simp]
theorem Real.deriv_log' :
deriv Real.log = Inv.inv
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) :

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 : ℕ∞} (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 : ℕ∞} (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 : ℕ∞} (hf : ContDiffOn n f s) (hs : xs, 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 : ℕ∞} (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 : xs, 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 : ) :
|iFinset.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 (#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.

@[deprecated Real.hasSum_pow_div_log_of_abs_lt_one]
theorem Real.hasSum_pow_div_log_of_abs_lt_1 {x : } (h : |x| < 1) :
HasSum (fun (n : ) => x ^ (n + 1) / (n + 1)) (-Real.log (1 - x))

Alias of Real.hasSum_pow_div_log_of_abs_lt_one.


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.

@[deprecated Real.hasSum_log_sub_log_of_abs_lt_one]
theorem Real.hasSum_log_sub_log_of_abs_lt_1 {x : } (h : |x| < 1) :
HasSum (fun (k : ) => 2 * (1 / (2 * k + 1)) * x ^ (2 * k + 1)) (Real.log (1 + x) - Real.log (1 - x))

Alias of Real.hasSum_log_sub_log_of_abs_lt_one.


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