mathlib3 documentation

analysis.special_functions.trigonometric.deriv

Differentiability of trigonometric functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main statements #

The differentiability of the usual trigonometric functions is proved, and their derivatives are computed.

Tags #

sin, cos, tan, angle

The complex sine function is everywhere strictly differentiable, with the derivative cos x.

The complex sine function is everywhere differentiable, with the derivative cos x.

The complex cosine function is everywhere strictly differentiable, with the derivative -sin x.

The complex cosine function is everywhere differentiable, with the derivative -sin x.

@[simp]

The complex hyperbolic sine function is everywhere strictly differentiable, with the derivative cosh x.

The complex hyperbolic sine function is everywhere differentiable, with the derivative cosh x.

The complex hyperbolic cosine function is everywhere strictly differentiable, with the derivative sinh x.

The complex hyperbolic cosine function is everywhere differentiable, with the derivative sinh x.

Simp lemmas for derivatives of λ x, complex.cos (f x) etc., f : ℂ → ℂ #

complex.cos #

theorem has_strict_deriv_at.ccos {f : } {f' x : } (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ), complex.cos (f x)) (-complex.sin (f x) * f') x
theorem has_deriv_at.ccos {f : } {f' x : } (hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ), complex.cos (f x)) (-complex.sin (f x) * f') x
theorem has_deriv_within_at.ccos {f : } {f' x : } {s : set } (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ), complex.cos (f x)) (-complex.sin (f x) * f') s x
theorem deriv_within_ccos {f : } {x : } {s : set } (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), complex.cos (f x)) s x = -complex.sin (f x) * deriv_within f s x
@[simp]
theorem deriv_ccos {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), complex.cos (f x)) x = -complex.sin (f x) * deriv f x

complex.sin #

theorem has_strict_deriv_at.csin {f : } {f' x : } (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ), complex.sin (f x)) (complex.cos (f x) * f') x
theorem has_deriv_at.csin {f : } {f' x : } (hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ), complex.sin (f x)) (complex.cos (f x) * f') x
theorem has_deriv_within_at.csin {f : } {f' x : } {s : set } (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ), complex.sin (f x)) (complex.cos (f x) * f') s x
theorem deriv_within_csin {f : } {x : } {s : set } (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), complex.sin (f x)) s x = complex.cos (f x) * deriv_within f s x
@[simp]
theorem deriv_csin {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), complex.sin (f x)) x = complex.cos (f x) * deriv f x

complex.cosh #

theorem has_strict_deriv_at.ccosh {f : } {f' x : } (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ), complex.cosh (f x)) (complex.sinh (f x) * f') x
theorem has_deriv_at.ccosh {f : } {f' x : } (hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ), complex.cosh (f x)) (complex.sinh (f x) * f') x
theorem has_deriv_within_at.ccosh {f : } {f' x : } {s : set } (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ), complex.cosh (f x)) (complex.sinh (f x) * f') s x
theorem deriv_within_ccosh {f : } {x : } {s : set } (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), complex.cosh (f x)) s x = complex.sinh (f x) * deriv_within f s x
@[simp]
theorem deriv_ccosh {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), complex.cosh (f x)) x = complex.sinh (f x) * deriv f x

complex.sinh #

theorem has_strict_deriv_at.csinh {f : } {f' x : } (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ), complex.sinh (f x)) (complex.cosh (f x) * f') x
theorem has_deriv_at.csinh {f : } {f' x : } (hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ), complex.sinh (f x)) (complex.cosh (f x) * f') x
theorem has_deriv_within_at.csinh {f : } {f' x : } {s : set } (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ), complex.sinh (f x)) (complex.cosh (f x) * f') s x
theorem deriv_within_csinh {f : } {x : } {s : set } (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), complex.sinh (f x)) s x = complex.cosh (f x) * deriv_within f s x
@[simp]
theorem deriv_csinh {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), complex.sinh (f x)) x = complex.cosh (f x) * deriv f x

Simp lemmas for derivatives of λ x, complex.cos (f x) etc., f : E → ℂ #

complex.cos #

theorem has_strict_fderiv_at.ccos {E : Type u_1} [normed_add_comm_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), complex.cos (f x)) (-complex.sin (f x) f') x
theorem has_fderiv_at.ccos {E : Type u_1} [normed_add_comm_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.cos (f x)) (-complex.sin (f x) f') x
theorem has_fderiv_within_at.ccos {E : Type u_1} [normed_add_comm_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.cos (f x)) (-complex.sin (f x) f') s x
theorem differentiable_within_at.ccos {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) :
differentiable_within_at (λ (x : E), complex.cos (f x)) s x
@[simp]
theorem differentiable_at.ccos {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), complex.cos (f x)) x
theorem differentiable_on.ccos {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), complex.cos (f x)) s
@[simp]
theorem differentiable.ccos {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } (hc : differentiable f) :
differentiable (λ (x : E), complex.cos (f x))
theorem fderiv_within_ccos {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) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), complex.cos (f x)) s x = -complex.sin (f x) fderiv_within f s x
@[simp]
theorem fderiv_ccos {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), complex.cos (f x)) x = -complex.sin (f x) fderiv f x
theorem cont_diff.ccos {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {n : ℕ∞} (h : cont_diff n f) :
cont_diff n (λ (x : E), complex.cos (f x))
theorem cont_diff_at.ccos {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} {n : ℕ∞} (hf : cont_diff_at n f x) :
cont_diff_at n (λ (x : E), complex.cos (f x)) x
theorem cont_diff_on.ccos {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) :
cont_diff_on n (λ (x : E), complex.cos (f x)) s
theorem cont_diff_within_at.ccos {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) :
cont_diff_within_at n (λ (x : E), complex.cos (f x)) s x

complex.sin #

theorem has_strict_fderiv_at.csin {E : Type u_1} [normed_add_comm_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), complex.sin (f x)) (complex.cos (f x) f') x
theorem has_fderiv_at.csin {E : Type u_1} [normed_add_comm_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.sin (f x)) (complex.cos (f x) f') x
theorem has_fderiv_within_at.csin {E : Type u_1} [normed_add_comm_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.sin (f x)) (complex.cos (f x) f') s x
theorem differentiable_within_at.csin {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) :
differentiable_within_at (λ (x : E), complex.sin (f x)) s x
@[simp]
theorem differentiable_at.csin {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), complex.sin (f x)) x
theorem differentiable_on.csin {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), complex.sin (f x)) s
@[simp]
theorem differentiable.csin {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } (hc : differentiable f) :
differentiable (λ (x : E), complex.sin (f x))
theorem fderiv_within_csin {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) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), complex.sin (f x)) s x = complex.cos (f x) fderiv_within f s x
@[simp]
theorem fderiv_csin {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), complex.sin (f x)) x = complex.cos (f x) fderiv f x
theorem cont_diff.csin {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {n : ℕ∞} (h : cont_diff n f) :
cont_diff n (λ (x : E), complex.sin (f x))
theorem cont_diff_at.csin {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} {n : ℕ∞} (hf : cont_diff_at n f x) :
cont_diff_at n (λ (x : E), complex.sin (f x)) x
theorem cont_diff_on.csin {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) :
cont_diff_on n (λ (x : E), complex.sin (f x)) s
theorem cont_diff_within_at.csin {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) :
cont_diff_within_at n (λ (x : E), complex.sin (f x)) s x

complex.cosh #

theorem has_strict_fderiv_at.ccosh {E : Type u_1} [normed_add_comm_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), complex.cosh (f x)) (complex.sinh (f x) f') x
theorem has_fderiv_at.ccosh {E : Type u_1} [normed_add_comm_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.cosh (f x)) (complex.sinh (f x) f') x
theorem has_fderiv_within_at.ccosh {E : Type u_1} [normed_add_comm_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.cosh (f x)) (complex.sinh (f x) f') s x
theorem differentiable_within_at.ccosh {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) :
differentiable_within_at (λ (x : E), complex.cosh (f x)) s x
@[simp]
theorem differentiable_at.ccosh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), complex.cosh (f x)) x
theorem differentiable_on.ccosh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), complex.cosh (f x)) s
@[simp]
theorem differentiable.ccosh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } (hc : differentiable f) :
differentiable (λ (x : E), complex.cosh (f x))
theorem fderiv_within_ccosh {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) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), complex.cosh (f x)) s x = complex.sinh (f x) fderiv_within f s x
@[simp]
theorem fderiv_ccosh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), complex.cosh (f x)) x = complex.sinh (f x) fderiv f x
theorem cont_diff.ccosh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {n : ℕ∞} (h : cont_diff n f) :
cont_diff n (λ (x : E), complex.cosh (f x))
theorem cont_diff_at.ccosh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} {n : ℕ∞} (hf : cont_diff_at n f x) :
cont_diff_at n (λ (x : E), complex.cosh (f x)) x
theorem cont_diff_on.ccosh {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) :
cont_diff_on n (λ (x : E), complex.cosh (f x)) s
theorem cont_diff_within_at.ccosh {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) :
cont_diff_within_at n (λ (x : E), complex.cosh (f x)) s x

complex.sinh #

theorem has_strict_fderiv_at.csinh {E : Type u_1} [normed_add_comm_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), complex.sinh (f x)) (complex.cosh (f x) f') x
theorem has_fderiv_at.csinh {E : Type u_1} [normed_add_comm_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.sinh (f x)) (complex.cosh (f x) f') x
theorem has_fderiv_within_at.csinh {E : Type u_1} [normed_add_comm_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.sinh (f x)) (complex.cosh (f x) f') s x
theorem differentiable_within_at.csinh {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) :
differentiable_within_at (λ (x : E), complex.sinh (f x)) s x
@[simp]
theorem differentiable_at.csinh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), complex.sinh (f x)) x
theorem differentiable_on.csinh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), complex.sinh (f x)) s
@[simp]
theorem differentiable.csinh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } (hc : differentiable f) :
differentiable (λ (x : E), complex.sinh (f x))
theorem fderiv_within_csinh {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) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), complex.sinh (f x)) s x = complex.cosh (f x) fderiv_within f s x
@[simp]
theorem fderiv_csinh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), complex.sinh (f x)) x = complex.cosh (f x) fderiv f x
theorem cont_diff.csinh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {n : ℕ∞} (h : cont_diff n f) :
cont_diff n (λ (x : E), complex.sinh (f x))
theorem cont_diff_at.csinh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} {n : ℕ∞} (hf : cont_diff_at n f x) :
cont_diff_at n (λ (x : E), complex.sinh (f x)) x
theorem cont_diff_on.csinh {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) :
cont_diff_on n (λ (x : E), complex.sinh (f x)) s
theorem cont_diff_within_at.csinh {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) :
cont_diff_within_at n (λ (x : E), complex.sinh (f x)) s x
@[simp]
theorem real.deriv_cos'  :

sinh is strictly monotone.

sinh is injective, ∀ a b, sinh a = sinh b → a = b.

@[simp]
theorem real.sinh_inj {x y : } :
@[simp]
theorem real.sinh_le_sinh {x y : } :
@[simp]
theorem real.sinh_lt_sinh {x y : } :
@[simp]
theorem real.sinh_pos_iff {x : } :
0 < real.sinh x 0 < x
@[simp]
theorem real.sinh_nonpos_iff {x : } :
@[simp]
theorem real.sinh_neg_iff {x : } :
real.sinh x < 0 x < 0
@[simp]
theorem real.sinh_nonneg_iff {x : } :
@[simp]
theorem real.cosh_le_cosh {x y : } :
@[simp]
theorem real.cosh_lt_cosh {x y : } :
@[simp]
theorem real.one_le_cosh (x : ) :
@[simp]
theorem real.one_lt_cosh {x : } :
1 < real.cosh x x 0
@[simp]
theorem real.self_le_sinh_iff {x : } :
@[simp]
theorem real.sinh_le_self_iff {x : } :
@[simp]
theorem real.self_lt_sinh_iff {x : } :
x < real.sinh x 0 < x
@[simp]
theorem real.sinh_lt_self_iff {x : } :
real.sinh x < x x < 0

Simp lemmas for derivatives of λ x, real.cos (f x) etc., f : ℝ → ℝ #

real.cos #

theorem has_strict_deriv_at.cos {f : } {f' x : } (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ), real.cos (f x)) (-real.sin (f x) * f') x
theorem has_deriv_at.cos {f : } {f' x : } (hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ), real.cos (f x)) (-real.sin (f x) * f') x
theorem has_deriv_within_at.cos {f : } {f' x : } {s : set } (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ), real.cos (f x)) (-real.sin (f x) * f') s x
theorem deriv_within_cos {f : } {x : } {s : set } (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), real.cos (f x)) s x = -real.sin (f x) * deriv_within f s x
@[simp]
theorem deriv_cos {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), real.cos (f x)) x = -real.sin (f x) * deriv f x

real.sin #

theorem has_strict_deriv_at.sin {f : } {f' x : } (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ), real.sin (f x)) (real.cos (f x) * f') x
theorem has_deriv_at.sin {f : } {f' x : } (hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ), real.sin (f x)) (real.cos (f x) * f') x
theorem has_deriv_within_at.sin {f : } {f' x : } {s : set } (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ), real.sin (f x)) (real.cos (f x) * f') s x
theorem deriv_within_sin {f : } {x : } {s : set } (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), real.sin (f x)) s x = real.cos (f x) * deriv_within f s x
@[simp]
theorem deriv_sin {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), real.sin (f x)) x = real.cos (f x) * deriv f x

real.cosh #

theorem has_strict_deriv_at.cosh {f : } {f' x : } (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ), real.cosh (f x)) (real.sinh (f x) * f') x
theorem has_deriv_at.cosh {f : } {f' x : } (hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ), real.cosh (f x)) (real.sinh (f x) * f') x
theorem has_deriv_within_at.cosh {f : } {f' x : } {s : set } (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ), real.cosh (f x)) (real.sinh (f x) * f') s x
theorem deriv_within_cosh {f : } {x : } {s : set } (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), real.cosh (f x)) s x = real.sinh (f x) * deriv_within f s x
@[simp]
theorem deriv_cosh {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), real.cosh (f x)) x = real.sinh (f x) * deriv f x

real.sinh #

theorem has_strict_deriv_at.sinh {f : } {f' x : } (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ), real.sinh (f x)) (real.cosh (f x) * f') x
theorem has_deriv_at.sinh {f : } {f' x : } (hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ), real.sinh (f x)) (real.cosh (f x) * f') x
theorem has_deriv_within_at.sinh {f : } {f' x : } {s : set } (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ), real.sinh (f x)) (real.cosh (f x) * f') s x
theorem deriv_within_sinh {f : } {x : } {s : set } (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), real.sinh (f x)) s x = real.cosh (f x) * deriv_within f s x
@[simp]
theorem deriv_sinh {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), real.sinh (f x)) x = real.cosh (f x) * deriv f x

Simp lemmas for derivatives of λ x, real.cos (f x) etc., f : E → ℝ #

real.cos #

theorem has_strict_fderiv_at.cos {E : Type u_1} [normed_add_comm_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.cos (f x)) (-real.sin (f x) f') x
theorem has_fderiv_at.cos {E : Type u_1} [normed_add_comm_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.cos (f x)) (-real.sin (f x) f') x
theorem has_fderiv_within_at.cos {E : Type u_1} [normed_add_comm_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.cos (f x)) (-real.sin (f x) f') s x
theorem differentiable_within_at.cos {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) :
differentiable_within_at (λ (x : E), real.cos (f x)) s x
@[simp]
theorem differentiable_at.cos {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), real.cos (f x)) x
theorem differentiable_on.cos {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), real.cos (f x)) s
@[simp]
theorem differentiable.cos {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } (hc : differentiable f) :
differentiable (λ (x : E), real.cos (f x))
theorem fderiv_within_cos {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) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), real.cos (f x)) s x = -real.sin (f x) fderiv_within f s x
@[simp]
theorem fderiv_cos {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), real.cos (f x)) x = -real.sin (f x) fderiv f x
theorem cont_diff.cos {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {n : ℕ∞} (h : cont_diff n f) :
cont_diff n (λ (x : E), real.cos (f x))
theorem cont_diff_at.cos {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} {n : ℕ∞} (hf : cont_diff_at n f x) :
cont_diff_at n (λ (x : E), real.cos (f x)) x
theorem cont_diff_on.cos {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) :
cont_diff_on n (λ (x : E), real.cos (f x)) s
theorem cont_diff_within_at.cos {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) :
cont_diff_within_at n (λ (x : E), real.cos (f x)) s x

real.sin #

theorem has_strict_fderiv_at.sin {E : Type u_1} [normed_add_comm_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.sin (f x)) (real.cos (f x) f') x
theorem has_fderiv_at.sin {E : Type u_1} [normed_add_comm_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.sin (f x)) (real.cos (f x) f') x
theorem has_fderiv_within_at.sin {E : Type u_1} [normed_add_comm_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.sin (f x)) (real.cos (f x) f') s x
theorem differentiable_within_at.sin {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) :
differentiable_within_at (λ (x : E), real.sin (f x)) s x
@[simp]
theorem differentiable_at.sin {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), real.sin (f x)) x
theorem differentiable_on.sin {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), real.sin (f x)) s
@[simp]
theorem differentiable.sin {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } (hc : differentiable f) :
differentiable (λ (x : E), real.sin (f x))
theorem fderiv_within_sin {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) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), real.sin (f x)) s x = real.cos (f x) fderiv_within f s x
@[simp]
theorem fderiv_sin {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), real.sin (f x)) x = real.cos (f x) fderiv f x
theorem cont_diff.sin {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {n : ℕ∞} (h : cont_diff n f) :
cont_diff n (λ (x : E), real.sin (f x))
theorem cont_diff_at.sin {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} {n : ℕ∞} (hf : cont_diff_at n f x) :
cont_diff_at n (λ (x : E), real.sin (f x)) x
theorem cont_diff_on.sin {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) :
cont_diff_on n (λ (x : E), real.sin (f x)) s
theorem cont_diff_within_at.sin {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) :
cont_diff_within_at n (λ (x : E), real.sin (f x)) s x

real.cosh #

theorem has_strict_fderiv_at.cosh {E : Type u_1} [normed_add_comm_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.cosh (f x)) (real.sinh (f x) f') x
theorem has_fderiv_at.cosh {E : Type u_1} [normed_add_comm_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.cosh (f x)) (real.sinh (f x) f') x
theorem has_fderiv_within_at.cosh {E : Type u_1} [normed_add_comm_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.cosh (f x)) (real.sinh (f x) f') s x
theorem differentiable_within_at.cosh {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) :
differentiable_within_at (λ (x : E), real.cosh (f x)) s x
@[simp]
theorem differentiable_at.cosh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), real.cosh (f x)) x
theorem differentiable_on.cosh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), real.cosh (f x)) s
@[simp]
theorem differentiable.cosh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } (hc : differentiable f) :
differentiable (λ (x : E), real.cosh (f x))
theorem fderiv_within_cosh {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) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), real.cosh (f x)) s x = real.sinh (f x) fderiv_within f s x
@[simp]
theorem fderiv_cosh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), real.cosh (f x)) x = real.sinh (f x) fderiv f x
theorem cont_diff.cosh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {n : ℕ∞} (h : cont_diff n f) :
cont_diff n (λ (x : E), real.cosh (f x))
theorem cont_diff_at.cosh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} {n : ℕ∞} (hf : cont_diff_at n f x) :
cont_diff_at n (λ (x : E), real.cosh (f x)) x
theorem cont_diff_on.cosh {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) :
cont_diff_on n (λ (x : E), real.cosh (f x)) s
theorem cont_diff_within_at.cosh {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) :
cont_diff_within_at n (λ (x : E), real.cosh (f x)) s x

real.sinh #

theorem has_strict_fderiv_at.sinh {E : Type u_1} [normed_add_comm_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.sinh (f x)) (real.cosh (f x) f') x
theorem has_fderiv_at.sinh {E : Type u_1} [normed_add_comm_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.sinh (f x)) (real.cosh (f x) f') x
theorem has_fderiv_within_at.sinh {E : Type u_1} [normed_add_comm_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.sinh (f x)) (real.cosh (f x) f') s x
theorem differentiable_within_at.sinh {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) :
differentiable_within_at (λ (x : E), real.sinh (f x)) s x
@[simp]
theorem differentiable_at.sinh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), real.sinh (f x)) x
theorem differentiable_on.sinh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), real.sinh (f x)) s
@[simp]
theorem differentiable.sinh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } (hc : differentiable f) :
differentiable (λ (x : E), real.sinh (f x))
theorem fderiv_within_sinh {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) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), real.sinh (f x)) s x = real.cosh (f x) fderiv_within f s x
@[simp]
theorem fderiv_sinh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), real.sinh (f x)) x = real.cosh (f x) fderiv f x
theorem cont_diff.sinh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {n : ℕ∞} (h : cont_diff n f) :
cont_diff n (λ (x : E), real.sinh (f x))
theorem cont_diff_at.sinh {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} {n : ℕ∞} (hf : cont_diff_at n f x) :
cont_diff_at n (λ (x : E), real.sinh (f x)) x
theorem cont_diff_on.sinh {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) :
cont_diff_on n (λ (x : E), real.sinh (f x)) s
theorem cont_diff_within_at.sinh {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) :
cont_diff_within_at n (λ (x : E), real.sinh (f x)) s x