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

source

theorem Real.hasStrictDerivAt_log_of_pos {x : ℝ} (hx : 0 < x) :

HasStrictDerivAt Real.log x⁻¹ x

source

theorem Real.hasStrictDerivAt_log {x : ℝ} (hx : x ≠ 0) :

HasStrictDerivAt Real.log x⁻¹ x

source

theorem Real.hasDerivAt_log {x : ℝ} (hx : x ≠ 0) :

HasDerivAt Real.log x⁻¹ x

source

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

DifferentiableAt ℝ Real.log x

source

theorem Real.differentiableOn_log :

DifferentiableOn ℝ Real.log {0}ᶜ

source

@[simp]

theorem Real.differentiableAt_log_iff {x : ℝ} :

DifferentiableAt ℝ 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 = Inv.inv

source

theorem Real.contDiffOn_log {n : ℕ∞} :

ContDiffOn ℝ n Real.log {0}ᶜ

source

theorem Real.contDiffAt_log {x : ℝ} {n : ℕ∞} :

ContDiffAt ℝ n Real.log x ↔ x ≠ 0

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

theorem ContDiffOn.log {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {n : ℕ∞} (hf : ContDiffOn ℝ n f s) (hs : ∀ x ∈ s, f x ≠ 0) :

ContDiffOn ℝ n (fun (x : E) => Real.log (f x)) s

source

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)

source

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

source

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

source

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

source

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

source

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 +∞.

source

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

|(Finset.sum (Finset.range n) fun (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 hasSum_pow_div_log_of_abs_lt_1.

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

source