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

source
theorem complex.has_strict_deriv_at_sin (x : ℂ) :
has_strict_deriv_at complex.sin (complex.cos x) x

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

source
theorem complex.has_deriv_at_sin (x : ℂ) :
has_deriv_at complex.sin (complex.cos x) x

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

source
theorem complex.cont_diff_sin {n : ℕ∞} :
cont_diff ℂ n complex.sin
source
theorem complex.differentiable_sin  :
differentiable ℂ complex.sin
source
theorem complex.differentiable_at_sin {x : ℂ} :
differentiable_at ℂ complex.sin x
source
@[simp]
theorem complex.deriv_sin  :
deriv complex.sin = complex.cos
source
theorem complex.has_strict_deriv_at_cos (x : ℂ) :
has_strict_deriv_at complex.cos (-complex.sin x) x

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

source
theorem complex.has_deriv_at_cos (x : ℂ) :
has_deriv_at complex.cos (-complex.sin x) x

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

source
theorem complex.cont_diff_cos {n : ℕ∞} :
cont_diff ℂ n complex.cos
source
theorem complex.differentiable_cos  :
differentiable ℂ complex.cos
source
theorem complex.differentiable_at_cos {x : ℂ} :
differentiable_at ℂ complex.cos x
source
theorem complex.deriv_cos {x : ℂ} :
deriv complex.cos x = -complex.sin x
source
@[simp]
theorem complex.deriv_cos'  :
deriv complex.cos = λ (x : ℂ), -complex.sin x
source
theorem complex.has_strict_deriv_at_sinh (x : ℂ) :
has_strict_deriv_at complex.sinh (complex.cosh x) x

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

source
theorem complex.has_deriv_at_sinh (x : ℂ) :
has_deriv_at complex.sinh (complex.cosh x) x

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

source
theorem complex.cont_diff_sinh {n : ℕ∞} :
cont_diff ℂ n complex.sinh
source
theorem complex.differentiable_sinh  :
differentiable ℂ complex.sinh
source
theorem complex.differentiable_at_sinh {x : ℂ} :
differentiable_at ℂ complex.sinh x
source
@[simp]
theorem complex.deriv_sinh  :
deriv complex.sinh = complex.cosh
source
theorem complex.has_strict_deriv_at_cosh (x : ℂ) :
has_strict_deriv_at complex.cosh (complex.sinh x) x

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

source
theorem complex.has_deriv_at_cosh (x : ℂ) :
has_deriv_at complex.cosh (complex.sinh x) x

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

source
theorem complex.cont_diff_cosh {n : ℕ∞} :
cont_diff ℂ n complex.cosh
source
theorem complex.differentiable_cosh  :
differentiable ℂ complex.cosh
source
theorem complex.differentiable_at_cosh {x : ℂ} :
differentiable_at ℂ complex.cosh x
source
@[simp]
theorem complex.deriv_cosh  :
deriv complex.cosh = complex.sinh

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

complex.cos #

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

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

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

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

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

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

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

source
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
source
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
source
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
source
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
source
@[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
source
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
source
@[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))
source
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
source
@[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
source
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))
source
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
source
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
source
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
source
theorem real.has_strict_deriv_at_sin (x : ℝ) :
has_strict_deriv_at real.sin (real.cos x) x
source
theorem real.has_deriv_at_sin (x : ℝ) :
has_deriv_at real.sin (real.cos x) x
source
theorem real.cont_diff_sin {n : ℕ∞} :
cont_diff ℝ n real.sin
source
theorem real.differentiable_sin  :
differentiable ℝ real.sin
source
theorem real.differentiable_at_sin {x : ℝ} :
differentiable_at ℝ real.sin x
source
@[simp]
theorem real.deriv_sin  :
deriv real.sin = real.cos
source
theorem real.has_strict_deriv_at_cos (x : ℝ) :
has_strict_deriv_at real.cos (-real.sin x) x
source
theorem real.has_deriv_at_cos (x : ℝ) :
has_deriv_at real.cos (-real.sin x) x
source
theorem real.cont_diff_cos {n : ℕ∞} :
cont_diff ℝ n real.cos
source
theorem real.differentiable_cos  :
differentiable ℝ real.cos
source
theorem real.differentiable_at_cos {x : ℝ} :
differentiable_at ℝ real.cos x
source
theorem real.deriv_cos {x : ℝ} :
deriv real.cos x = -real.sin x
source
@[simp]
theorem real.deriv_cos'  :
deriv real.cos = λ (x : ℝ), -real.sin x
source
theorem real.has_strict_deriv_at_sinh (x : ℝ) :
has_strict_deriv_at real.sinh (real.cosh x) x
source
theorem real.has_deriv_at_sinh (x : ℝ) :
has_deriv_at real.sinh (real.cosh x) x
source
theorem real.cont_diff_sinh {n : ℕ∞} :
cont_diff ℝ n real.sinh
source
theorem real.differentiable_sinh  :
differentiable ℝ real.sinh
source
theorem real.differentiable_at_sinh {x : ℝ} :
differentiable_at ℝ real.sinh x
source
@[simp]
theorem real.deriv_sinh  :
deriv real.sinh = real.cosh
source
theorem real.has_strict_deriv_at_cosh (x : ℝ) :
has_strict_deriv_at real.cosh (real.sinh x) x
source
theorem real.has_deriv_at_cosh (x : ℝ) :
has_deriv_at real.cosh (real.sinh x) x
source
theorem real.cont_diff_cosh {n : ℕ∞} :
cont_diff ℝ n real.cosh
source
theorem real.differentiable_cosh  :
differentiable ℝ real.cosh
source
theorem real.differentiable_at_cosh {x : ℝ} :
differentiable_at ℝ real.cosh x
source
@[simp]
theorem real.deriv_cosh  :
deriv real.cosh = real.sinh
source
theorem real.sinh_strict_mono  :
strict_mono real.sinh

sinh is strictly monotone.

source
theorem real.sinh_injective  :
function.injective real.sinh

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

source
@[simp]
theorem real.sinh_inj {x y : ℝ} :
real.sinh x = real.sinh y ↔ x = y
source
@[simp]
theorem real.sinh_le_sinh {x y : ℝ} :
real.sinh x ≤ real.sinh y ↔ x ≤ y
source
@[simp]
theorem real.sinh_lt_sinh {x y : ℝ} :
real.sinh x < real.sinh y ↔ x < y
source
@[simp]
theorem real.sinh_pos_iff {x : ℝ} :
0 < real.sinh x ↔ 0 < x
source
@[simp]
theorem real.sinh_nonpos_iff {x : ℝ} :
real.sinh x ≤ 0 ↔ x ≤ 0
source
@[simp]
theorem real.sinh_neg_iff {x : ℝ} :
real.sinh x < 0 ↔ x < 0
source
@[simp]
theorem real.sinh_nonneg_iff {x : ℝ} :
0 ≤ real.sinh x ↔ 0 ≤ x
source
theorem real.abs_sinh (x : ℝ) :
|real.sinh x| = real.sinh |x|
source
theorem real.cosh_strict_mono_on  :
strict_mono_on real.cosh (set.Ici 0)
source
@[simp]
theorem real.cosh_le_cosh {x y : ℝ} :
real.cosh x ≤ real.cosh y ↔ |x| ≤ |y|
source
@[simp]
theorem real.cosh_lt_cosh {x y : ℝ} :
real.cosh x < real.cosh y ↔ |x| < |y|
source
@[simp]
theorem real.one_le_cosh (x : ℝ) :
1 ≤ real.cosh x
source
@[simp]
theorem real.one_lt_cosh {x : ℝ} :
1 < real.cosh x ↔ x ≠ 0
source
theorem real.sinh_sub_id_strict_mono  :
strict_mono (λ (x : ℝ), real.sinh x - x)
source
@[simp]
theorem real.self_le_sinh_iff {x : ℝ} :
x ≤ real.sinh x ↔ 0 ≤ x
source
@[simp]
theorem real.sinh_le_self_iff {x : ℝ} :
real.sinh x ≤ x ↔ x ≤ 0
source
@[simp]
theorem real.self_lt_sinh_iff {x : ℝ} :
x < real.sinh x ↔ 0 < x
source
@[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 #

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

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

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

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

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

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

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

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