analysis.special_functions.exp_log

theorem has_fderiv_within_at.cexp {E : Type u_1} [normed_group E] [normed_space ℂ E] {f : E → ℂ} {f' : E →L[ℂ ] ℂ} {x : E} {s : set E} (hf : has_fderiv_within_at f f' s x) :

has_fderiv_within_at (λ (x : E), complex.exp (f x)) (complex.exp (f x) • f') s x

source

theorem has_fderiv_at.cexp {E : Type u_1} [normed_group E] [normed_space ℂ E] {f : E → ℂ} {f' : E →L[ℂ ] ℂ} {x : E} (hf : has_fderiv_at f f' x) :

has_fderiv_at (λ (x : E), complex.exp (f x)) (complex.exp (f x) • f') x

source

theorem differentiable_within_at.cexp {E : Type u_1} [normed_group E] [normed_space ℂ E] {f : E → ℂ} {x : E} {s : set E} (hf : differentiable_within_at ℂ f s x) :

differentiable_within_at ℂ (λ (x : E), complex.exp (f x)) s x

source

@[simp]

theorem differentiable_at.cexp {E : Type u_1} [normed_group E] [normed_space ℂ E] {f : E → ℂ} {x : E} (hc : differentiable_at ℂ f x) :

differentiable_at ℂ (λ (x : E), complex.exp (f x)) x

source

theorem differentiable_on.cexp {E : Type u_1} [normed_group E] [normed_space ℂ E] {f : E → ℂ} {s : set E} (hc : differentiable_on ℂ f s) :

differentiable_on ℂ (λ (x : E), complex.exp (f x)) s

source

@[simp]

theorem differentiable.cexp {E : Type u_1} [normed_group E] [normed_space ℂ E] {f : E → ℂ} (hc : differentiable ℂ f) :

differentiable ℂ (λ (x : E), complex.exp (f x))

source

theorem times_cont_diff.cexp {E : Type u_1} [normed_group E] [normed_space ℂ E] {f : E → ℂ} {n : with_top ℕ} (h : times_cont_diff ℂ n f) :

times_cont_diff ℂ n (λ (x : E), complex.exp (f x))

source

theorem times_cont_diff_at.cexp {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) :

times_cont_diff_at ℂ n (λ (x : E), complex.exp (f x)) x

source

theorem times_cont_diff_on.cexp {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) :

times_cont_diff_on ℂ n (λ (x : E), complex.exp (f x)) s

source

theorem times_cont_diff_within_at.cexp {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) :

times_cont_diff_within_at ℂ n (λ (x : E), complex.exp (f x)) s x

source

theorem real.has_strict_deriv_at_exp (x : ℝ) :

has_strict_deriv_at real.exp (real.exp x) x

source

theorem real.has_deriv_at_exp (x : ℝ) :

has_deriv_at real.exp (real.exp x) x

source

theorem real.times_cont_diff_exp {n : with_top ℕ} :

times_cont_diff ℝ n real.exp

source

theorem real.differentiable_exp :

differentiable ℝ real.exp

source

theorem real.differentiable_at_exp {x : ℝ} :

differentiable_at ℝ real.exp x

source

@[simp]

theorem real.deriv_exp :

deriv real.exp = real.exp

source

@[simp]

theorem real.iter_deriv_exp (n : ℕ) :

deriv ^[n] real.exp = real.exp

source

@[continuity]

theorem real.continuous_exp :

continuous real.exp

source

theorem real.continuous_on_exp {s : set ℝ} :

continuous_on real.exp s

source

theorem real.measurable_exp :

measurable real.exp

source

theorem has_strict_deriv_at.exp {f : ℝ → ℝ} {f' x : ℝ} (hf : has_strict_deriv_at f f' x) :

has_strict_deriv_at (λ (x : ℝ), real.exp (f x)) ((real.exp (f x)) * f') x

source

theorem has_deriv_at.exp {f : ℝ → ℝ} {f' x : ℝ} (hf : has_deriv_at f f' x) :

has_deriv_at (λ (x : ℝ), real.exp (f x)) ((real.exp (f x)) * f') x

source

theorem has_deriv_within_at.exp {f : ℝ → ℝ} {f' x : ℝ} {s : set ℝ} (hf : has_deriv_within_at f f' s x) :

has_deriv_within_at (λ (x : ℝ), real.exp (f x)) ((real.exp (f x)) * f') s x

source

theorem deriv_within_exp {f : ℝ → ℝ} {x : ℝ} {s : set ℝ} (hf : differentiable_within_at ℝ f s x) (hxs : unique_diff_within_at ℝ s x) :

deriv_within (λ (x : ℝ), real.exp (f x)) s x = (real.exp (f x)) * deriv_within f s x

source

@[simp]

theorem deriv_exp {f : ℝ → ℝ} {x : ℝ} (hc : differentiable_at ℝ f x) :

deriv (λ (x : ℝ), real.exp (f x)) x = (real.exp (f x)) * deriv f x

source

theorem measurable.exp {α : Type u_1} [measurable_space α] {f : α → ℝ} (hf : measurable f) :

measurable (λ (x : α), real.exp (f x))

source

theorem times_cont_diff.exp {E : Type u_1} [normed_group E] [normed_space ℝ E] {f : E → ℝ} {n : with_top ℕ} (hf : times_cont_diff ℝ n f) :

times_cont_diff ℝ n (λ (x : E), real.exp (f x))

source

theorem times_cont_diff_at.exp {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) :

times_cont_diff_at ℝ n (λ (x : E), real.exp (f x)) x

source

theorem times_cont_diff_on.exp {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) :

times_cont_diff_on ℝ n (λ (x : E), real.exp (f x)) s

source

theorem times_cont_diff_within_at.exp {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) :

times_cont_diff_within_at ℝ n (λ (x : E), real.exp (f x)) s x

source

theorem has_fderiv_within_at.exp {E : Type u_1} [normed_group E] [normed_space ℝ E] {f : E → ℝ} {f' : E →L[ℝ ] ℝ} {x : E} {s : set E} (hf : has_fderiv_within_at f f' s x) :

has_fderiv_within_at (λ (x : E), real.exp (f x)) (real.exp (f x) • f') s x

source

theorem has_fderiv_at.exp {E : Type u_1} [normed_group E] [normed_space ℝ E] {f : E → ℝ} {f' : E →L[ℝ ] ℝ} {x : E} (hf : has_fderiv_at f f' x) :

has_fderiv_at (λ (x : E), real.exp (f x)) (real.exp (f x) • f') x

source

theorem has_strict_fderiv_at.exp {E : Type u_1} [normed_group E] [normed_space ℝ E] {f : E → ℝ} {f' : E →L[ℝ ] ℝ} {x : E} (hf : has_strict_fderiv_at f f' x) :

has_strict_fderiv_at (λ (x : E), real.exp (f x)) (real.exp (f x) • f') x

source

theorem differentiable_within_at.exp {E : Type u_1} [normed_group E] [normed_space ℝ E] {f : E → ℝ} {x : E} {s : set E} (hf : differentiable_within_at ℝ f s x) :

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

source

@[simp]

theorem differentiable_at.exp {E : Type u_1} [normed_group E] [normed_space ℝ E] {f : E → ℝ} {x : E} (hc : differentiable_at ℝ f x) :

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

source

theorem differentiable_on.exp {E : Type u_1} [normed_group E] [normed_space ℝ E] {f : E → ℝ} {s : set E} (hc : differentiable_on ℝ f s) :

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

source

@[simp]

theorem differentiable.exp {E : Type u_1} [normed_group E] [normed_space ℝ E] {f : E → ℝ} (hc : differentiable ℝ f) :

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

source

theorem fderiv_within_exp {E : Type u_1} [normed_group E] [normed_space ℝ E] {f : E → ℝ} {x : E} {s : set E} (hf : differentiable_within_at ℝ f s x) (hxs : unique_diff_within_at ℝ s x) :

fderiv_within ℝ (λ (x : E), real.exp (f x)) s x = real.exp (f x) • fderiv_within ℝ f s x

source

@[simp]

theorem fderiv_exp {E : Type u_1} [normed_group E] [normed_space ℝ E] {f : E → ℝ} {x : E} (hc : differentiable_at ℝ f x) :

fderiv ℝ (λ (x : E), real.exp (f x)) x = real.exp (f x) • fderiv ℝ f x

source

theorem real.tendsto_exp_at_top :

filter.tendsto real.exp filter.at_top filter.at_top

The real exponential function tends to +∞ at +∞.

source

theorem real.tendsto_exp_neg_at_top_nhds_0 :

filter.tendsto (λ (x : ℝ), real.exp (-x)) filter.at_top (𝓝 0)

The real exponential function tends to 0 at -∞ or, equivalently, exp(-x) tends to 0 at +∞

source

theorem real.tendsto_exp_nhds_0_nhds_1 :

filter.tendsto real.exp (𝓝 0) (𝓝 1)

The real exponential function tends to 1 at 0.

source

theorem real.tendsto_exp_at_bot :

filter.tendsto real.exp filter.at_bot (𝓝 0)

source

theorem real.tendsto_exp_at_bot_nhds_within :

filter.tendsto real.exp filter.at_bot (𝓝[set.Ioi 0] 0)

source

def real.exp_order_iso :

ℝ ≃o ↥(set.Ioi 0)

real.exp as an order isomorphism between ℝ and (0, +∞).

Equations

real.exp_order_iso = strict_mono.order_iso_of_surjective (set.cod_restrict real.exp (set.Ioi 0) real.exp_pos) real.exp_order_iso._proof_1 real.exp_order_iso._proof_2

source

@[simp]

theorem real.coe_exp_order_iso_apply (x : ℝ) :

↑(⇑real.exp_order_iso x) = real.exp x

source

@[simp]

theorem real.coe_comp_exp_order_iso :

coe ∘ ⇑real.exp_order_iso = real.exp

source

@[simp]

theorem real.range_exp :

set.range real.exp = set.Ioi 0

source

@[simp]

theorem real.map_exp_at_top :

filter.map real.exp filter.at_top = filter.at_top

source

@[simp]

theorem real.comap_exp_at_top :

filter.comap real.exp filter.at_top = filter.at_top

source

@[simp]

theorem real.tendsto_exp_comp_at_top {α : Type u_1} {l : filter α} {f : α → ℝ} :

filter.tendsto (λ (x : α), real.exp (f x)) l filter.at_top ↔ filter.tendsto f l filter.at_top

source

theorem real.tendsto_comp_exp_at_top {α : Type u_1} {l : filter α} {f : ℝ → α} :

filter.tendsto (λ (x : ℝ), f (real.exp x)) filter.at_top l ↔ filter.tendsto f filter.at_top l

source

@[simp]

theorem real.map_exp_at_bot :

filter.map real.exp filter.at_bot = 𝓝[set.Ioi 0] 0

source

theorem real.comap_exp_nhds_within_Ioi_zero :

filter.comap real.exp (𝓝[set.Ioi 0] 0) = filter.at_bot

source

theorem real.tendsto_comp_exp_at_bot {α : Type u_1} {l : filter α} {f : ℝ → α} :

filter.tendsto (λ (x : ℝ), f (real.exp x)) filter.at_bot l ↔ filter.tendsto f (𝓝[set.Ioi 0] 0) l

source

def real.log (x : ℝ) :

ℝ

The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. We use this unconventional extension to (-∞, 0] as it gives the formula log (x * y) = log x + log y for all nonzero x and y, and the derivative of log is 1/x away from 0.

Equations

real.log x = dite (x = 0) (λ (hx : x = 0), 0) (λ (hx : ¬x = 0), ⇑(real.exp_order_iso.symm) ⟨abs x, _⟩)

source

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

real.log x = ⇑(real.exp_order_iso.symm) ⟨abs x, _⟩

source

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

real.log x = ⇑(real.exp_order_iso.symm) ⟨x, hx⟩

source

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

real.exp (real.log x) = abs x

source

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

real.exp (real.log x) = x

source

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

real.exp (real.log x) = -x

source

@[simp]

theorem real.log_exp (x : ℝ) :

real.log (real.exp x) = x

source

theorem real.surj_on_log :

set.surj_on real.log (set.Ioi 0) set.univ

source

theorem real.log_surjective :

function.surjective real.log

source

@[simp]

theorem real.range_log :

set.range real.log = set.univ

source

@[simp]

theorem real.log_zero :

real.log 0 = 0

source

@[simp]

theorem real.log_one :

real.log 1 = 0

source

@[simp]

theorem real.log_abs (x : ℝ) :

real.log (abs x) = real.log x

source

@[simp]

theorem real.log_neg_eq_log (x : ℝ) :

real.log (-x) = real.log x

source

theorem real.surj_on_log' :

set.surj_on real.log (set.Iio 0) set.univ

source

theorem real.log_mul {x y : ℝ} (hx : x ≠ 0) (hy : y ≠ 0) :

real.log (x * y) = real.log x + real.log y

source

theorem real.log_div {x y : ℝ} (hx : x ≠ 0) (hy : y ≠ 0) :

real.log (x / y) = real.log x - real.log y

source

@[simp]

theorem real.log_inv (x : ℝ) :

real.log x⁻¹ = -real.log x

source

theorem real.log_le_log {x y : ℝ} (h : 0 < x) (h₁ : 0 < y) :

real.log x ≤ real.log y ↔ x ≤ y

source

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

x < y → real.log x < real.log y

source

theorem real.log_lt_log_iff {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :

real.log x < real.log y ↔ x < y

source

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

0 < real.log x ↔ 1 < x

source

theorem real.log_pos {x : ℝ} (hx : 1 < x) :

0 < real.log x

source

theorem real.log_neg_iff {x : ℝ} (h : 0 < x) :

real.log x < 0 ↔ x < 1

source

theorem real.log_neg {x : ℝ} (h0 : 0 < x) (h1 : x < 1) :

real.log x < 0

source

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

0 ≤ real.log x ↔ 1 ≤ x

source

theorem real.log_nonneg {x : ℝ} (hx : 1 ≤ x) :

0 ≤ real.log x

source

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

real.log x ≤ 0 ↔ x ≤ 1

source

theorem real.log_nonpos_iff' {x : ℝ} (hx : 0 ≤ x) :

real.log x ≤ 0 ↔ x ≤ 1

source

theorem real.log_nonpos {x : ℝ} (hx : 0 ≤ x) (h'x : x ≤ 1) :

real.log x ≤ 0

source

theorem real.strict_mono_incr_on_log :

strict_mono_incr_on real.log (set.Ioi 0)

source

theorem real.strict_mono_decr_on_log :

strict_mono_decr_on real.log (set.Iio 0)

source

theorem real.log_inj_on_pos :

set.inj_on real.log (set.Ioi 0)

source

theorem real.eq_one_of_pos_of_log_eq_zero {x : ℝ} (h₁ : 0 < x) (h₂ : real.log x = 0) :

x = 1

source

theorem real.log_ne_zero_of_pos_of_ne_one {x : ℝ} (hx_pos : 0 < x) (hx : x ≠ 1) :

real.log x ≠ 0

source

theorem real.tendsto_log_at_top :

filter.tendsto real.log filter.at_top filter.at_top

The real logarithm function tends to +∞ at +∞.

source

theorem real.tendsto_log_nhds_within_zero :

filter.tendsto real.log (𝓝[{0}ᶜ ] 0) filter.at_bot

source

theorem real.continuous_on_log :

continuous_on real.log {0}ᶜ

source

@[continuity]

theorem real.continuous_log' :

continuous (λ (x : {x // 0 < x}), real.log ↑x)

source

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

continuous_at real.log x

source

@[simp]

theorem real.continuous_at_log_iff {x : ℝ} :

continuous_at real.log x ↔ x ≠ 0

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.measurable_log :

measurable real.log

source

theorem real.times_cont_diff_on_log {n : with_top ℕ} :

times_cont_diff_on ℝ n real.log {0}ᶜ

source

theorem real.times_cont_diff_at_log {x : ℝ} {n : with_top ℕ} :

times_cont_diff_at ℝ n real.log x ↔ x ≠ 0

source

theorem filter.tendsto.log {α : Type u_1} {f : α → ℝ} {l : filter α} {x : ℝ} (h : filter.tendsto f l (𝓝 x)) (hx : x ≠ 0) :

filter.tendsto (λ (x : α), real.log (f x)) l (𝓝 (real.log x))

source

theorem continuous.log {α : Type u_1} [topological_space α] {f : α → ℝ} (hf : continuous f) (h₀ : ∀ (x : α), f x ≠ 0) :

continuous (λ (x : α), real.log (f x))

source

theorem continuous_at.log {α : Type u_1} [topological_space α] {f : α → ℝ} {a : α} (hf : continuous_at f a) (h₀ : f a ≠ 0) :

continuous_at (λ (x : α), real.log (f x)) a

source

theorem continuous_within_at.log {α : Type u_1} [topological_space α] {f : α → ℝ} {s : set α} {a : α} (hf : continuous_within_at f s a) (h₀ : f a ≠ 0) :

continuous_within_at (λ (x : α), real.log (f x)) s a

source

theorem continuous_on.log {α : Type u_1} [topological_space α] {f : α → ℝ} {s : set α} (hf : continuous_on f s) (h₀ : ∀ (x : α), x ∈ s → f x ≠ 0) :

continuous_on (λ (x : α), real.log (f x)) s

source

theorem measurable.log {α : Type u_1} [measurable_space α] {f : α → ℝ} (hf : measurable f) :

measurable (λ (x : α), real.log (f x))

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_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_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_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_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_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 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

source

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

source

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 ∈ s → f x ≠ 0) :

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

source

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

source

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 ∈ s → f x ≠ 0) :

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

source

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

source

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

source

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

source

theorem real.tendsto_exp_div_pow_at_top (n : ℕ) :

filter.tendsto (λ (x : ℝ), real.exp x / x ^ n) filter.at_top filter.at_top

The function exp(x)/x^n tends to +∞ at +∞, for any natural number n

source

theorem real.tendsto_pow_mul_exp_neg_at_top_nhds_0 (n : ℕ) :

filter.tendsto (λ (x : ℝ), (x ^ n) * real.exp (-x)) filter.at_top (𝓝 0)

The function x^n * exp(-x) tends to 0 at +∞, for any natural number n.

source

theorem real.tendsto_mul_exp_add_div_pow_at_top (b c : ℝ) (n : ℕ) (hb : 0 < b) (hn : 1 ≤ n) :

filter.tendsto (λ (x : ℝ), (b * real.exp x + c) / x ^ n) filter.at_top filter.at_top

The function (b * exp x + c) / (x ^ n) tends to +∞ at +∞, for any positive natural number n and any real numbers b and c such that b is positive.

source

theorem real.tendsto_div_pow_mul_exp_add_at_top (b c : ℝ) (n : ℕ) (hb : 0 ≠ b) (hn : 1 ≤ n) :

filter.tendsto (λ (x : ℝ), x ^ n / (b * real.exp x + c)) filter.at_top (𝓝 0)

The function (x ^ n) / (b * exp x + c) tends to 0 at +∞, for any positive natural number n and any real numbers b and c such that b is nonzero.

source

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

abs (∑ (i : ℕ) in finset.range n, x ^ (i + 1) / (↑i + 1) + real.log (1 - x)) ≤ abs x ^ (n + 1) / (1 - abs 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 : abs x < 1) :

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

Power series expansion of the logarithm around 1.

mathlib documentation

Complex and real exponential, real logarithm #

Main statements #

Tags #