# Differentiability of trigonometric functions #

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

theorem Complex.hasDerivAt_sin (x : ) :

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

@[simp]

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

theorem Complex.hasDerivAt_cos (x : ) :

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

@[simp]
theorem Complex.deriv_cos' :
= fun (x : ) =>

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.

@[simp]

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]

### Simp lemmas for derivatives of fun x => Complex.cos (f x) etc., f : ℂ → ℂ#

#### Complex.cos#

theorem HasStrictDerivAt.ccos {f : } {f' : } {x : } (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (x : ) => Complex.cos (f x)) (-Complex.sin (f x) * f') x
theorem HasDerivAt.ccos {f : } {f' : } {x : } (hf : HasDerivAt f f' x) :
HasDerivAt (fun (x : ) => Complex.cos (f x)) (-Complex.sin (f x) * f') x
theorem HasDerivWithinAt.ccos {f : } {f' : } {x : } {s : } (hf : HasDerivWithinAt f f' s x) :
HasDerivWithinAt (fun (x : ) => Complex.cos (f x)) (-Complex.sin (f x) * f') s x
theorem derivWithin_ccos {f : } {x : } {s : } (hf : ) (hxs : ) :
derivWithin (fun (x : ) => Complex.cos (f x)) s x = -Complex.sin (f x) * derivWithin f s x
@[simp]
theorem deriv_ccos {f : } {x : } (hc : ) :
deriv (fun (x : ) => Complex.cos (f x)) x = -Complex.sin (f x) * deriv f x

#### Complex.sin#

theorem HasStrictDerivAt.csin {f : } {f' : } {x : } (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (x : ) => Complex.sin (f x)) (Complex.cos (f x) * f') x
theorem HasDerivAt.csin {f : } {f' : } {x : } (hf : HasDerivAt f f' x) :
HasDerivAt (fun (x : ) => Complex.sin (f x)) (Complex.cos (f x) * f') x
theorem HasDerivWithinAt.csin {f : } {f' : } {x : } {s : } (hf : HasDerivWithinAt f f' s x) :
HasDerivWithinAt (fun (x : ) => Complex.sin (f x)) (Complex.cos (f x) * f') s x
theorem derivWithin_csin {f : } {x : } {s : } (hf : ) (hxs : ) :
derivWithin (fun (x : ) => Complex.sin (f x)) s x = Complex.cos (f x) * derivWithin f s x
@[simp]
theorem deriv_csin {f : } {x : } (hc : ) :
deriv (fun (x : ) => Complex.sin (f x)) x = Complex.cos (f x) * deriv f x

#### Complex.cosh#

theorem HasStrictDerivAt.ccosh {f : } {f' : } {x : } (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (x : ) => Complex.cosh (f x)) (Complex.sinh (f x) * f') x
theorem HasDerivAt.ccosh {f : } {f' : } {x : } (hf : HasDerivAt f f' x) :
HasDerivAt (fun (x : ) => Complex.cosh (f x)) (Complex.sinh (f x) * f') x
theorem HasDerivWithinAt.ccosh {f : } {f' : } {x : } {s : } (hf : HasDerivWithinAt f f' s x) :
HasDerivWithinAt (fun (x : ) => Complex.cosh (f x)) (Complex.sinh (f x) * f') s x
theorem derivWithin_ccosh {f : } {x : } {s : } (hf : ) (hxs : ) :
derivWithin (fun (x : ) => Complex.cosh (f x)) s x = Complex.sinh (f x) * derivWithin f s x
@[simp]
theorem deriv_ccosh {f : } {x : } (hc : ) :
deriv (fun (x : ) => Complex.cosh (f x)) x = Complex.sinh (f x) * deriv f x

#### Complex.sinh#

theorem HasStrictDerivAt.csinh {f : } {f' : } {x : } (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (x : ) => Complex.sinh (f x)) (Complex.cosh (f x) * f') x
theorem HasDerivAt.csinh {f : } {f' : } {x : } (hf : HasDerivAt f f' x) :
HasDerivAt (fun (x : ) => Complex.sinh (f x)) (Complex.cosh (f x) * f') x
theorem HasDerivWithinAt.csinh {f : } {f' : } {x : } {s : } (hf : HasDerivWithinAt f f' s x) :
HasDerivWithinAt (fun (x : ) => Complex.sinh (f x)) (Complex.cosh (f x) * f') s x
theorem derivWithin_csinh {f : } {x : } {s : } (hf : ) (hxs : ) :
derivWithin (fun (x : ) => Complex.sinh (f x)) s x = Complex.cosh (f x) * derivWithin f s x
@[simp]
theorem deriv_csinh {f : } {x : } (hc : ) :
deriv (fun (x : ) => Complex.sinh (f x)) x = Complex.cosh (f x) * deriv f x

### Simp lemmas for derivatives of fun x => Complex.cos (f x) etc., f : E → ℂ#

#### Complex.cos#

theorem HasStrictFDerivAt.ccos {E : Type u_1} [] {f : E} {f' : } {x : E} (hf : ) :
HasStrictFDerivAt (fun (x : E) => Complex.cos (f x)) (-Complex.sin (f x) f') x
theorem HasFDerivAt.ccos {E : Type u_1} [] {f : E} {f' : } {x : E} (hf : HasFDerivAt f f' x) :
HasFDerivAt (fun (x : E) => Complex.cos (f x)) (-Complex.sin (f x) f') x
theorem HasFDerivWithinAt.ccos {E : Type u_1} [] {f : E} {f' : } {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) :
HasFDerivWithinAt (fun (x : E) => Complex.cos (f x)) (-Complex.sin (f x) f') s x
theorem DifferentiableWithinAt.ccos {E : Type u_1} [] {f : E} {x : E} {s : Set E} (hf : ) :
DifferentiableWithinAt (fun (x : E) => Complex.cos (f x)) s x
@[simp]
theorem DifferentiableAt.ccos {E : Type u_1} [] {f : E} {x : E} (hc : ) :
DifferentiableAt (fun (x : E) => Complex.cos (f x)) x
theorem DifferentiableOn.ccos {E : Type u_1} [] {f : E} {s : Set E} (hc : ) :
DifferentiableOn (fun (x : E) => Complex.cos (f x)) s
@[simp]
theorem Differentiable.ccos {E : Type u_1} [] {f : E} (hc : ) :
Differentiable fun (x : E) => Complex.cos (f x)
theorem fderivWithin_ccos {E : Type u_1} [] {f : E} {x : E} {s : Set E} (hf : ) (hxs : ) :
fderivWithin (fun (x : E) => Complex.cos (f x)) s x = -Complex.sin (f x)
@[simp]
theorem fderiv_ccos {E : Type u_1} [] {f : E} {x : E} (hc : ) :
fderiv (fun (x : E) => Complex.cos (f x)) x = -Complex.sin (f x) fderiv f x
theorem ContDiff.ccos {E : Type u_1} [] {f : E} {n : ℕ∞} (h : ) :
ContDiff n fun (x : E) => Complex.cos (f x)
theorem ContDiffAt.ccos {E : Type u_1} [] {f : E} {x : E} {n : ℕ∞} (hf : ContDiffAt n f x) :
ContDiffAt n (fun (x : E) => Complex.cos (f x)) x
theorem ContDiffOn.ccos {E : Type u_1} [] {f : E} {s : Set E} {n : ℕ∞} (hf : ContDiffOn n f s) :
ContDiffOn n (fun (x : E) => Complex.cos (f x)) s
theorem ContDiffWithinAt.ccos {E : Type u_1} [] {f : E} {x : E} {s : Set E} {n : ℕ∞} (hf : ) :
ContDiffWithinAt n (fun (x : E) => Complex.cos (f x)) s x

#### Complex.sin#

theorem HasStrictFDerivAt.csin {E : Type u_1} [] {f : E} {f' : } {x : E} (hf : ) :
HasStrictFDerivAt (fun (x : E) => Complex.sin (f x)) (Complex.cos (f x) f') x
theorem HasFDerivAt.csin {E : Type u_1} [] {f : E} {f' : } {x : E} (hf : HasFDerivAt f f' x) :
HasFDerivAt (fun (x : E) => Complex.sin (f x)) (Complex.cos (f x) f') x
theorem HasFDerivWithinAt.csin {E : Type u_1} [] {f : E} {f' : } {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) :
HasFDerivWithinAt (fun (x : E) => Complex.sin (f x)) (Complex.cos (f x) f') s x
theorem DifferentiableWithinAt.csin {E : Type u_1} [] {f : E} {x : E} {s : Set E} (hf : ) :
DifferentiableWithinAt (fun (x : E) => Complex.sin (f x)) s x
@[simp]
theorem DifferentiableAt.csin {E : Type u_1} [] {f : E} {x : E} (hc : ) :
DifferentiableAt (fun (x : E) => Complex.sin (f x)) x
theorem DifferentiableOn.csin {E : Type u_1} [] {f : E} {s : Set E} (hc : ) :
DifferentiableOn (fun (x : E) => Complex.sin (f x)) s
@[simp]
theorem Differentiable.csin {E : Type u_1} [] {f : E} (hc : ) :
Differentiable fun (x : E) => Complex.sin (f x)
theorem fderivWithin_csin {E : Type u_1} [] {f : E} {x : E} {s : Set E} (hf : ) (hxs : ) :
fderivWithin (fun (x : E) => Complex.sin (f x)) s x = Complex.cos (f x)
@[simp]
theorem fderiv_csin {E : Type u_1} [] {f : E} {x : E} (hc : ) :
fderiv (fun (x : E) => Complex.sin (f x)) x = Complex.cos (f x) fderiv f x
theorem ContDiff.csin {E : Type u_1} [] {f : E} {n : ℕ∞} (h : ) :
ContDiff n fun (x : E) => Complex.sin (f x)
theorem ContDiffAt.csin {E : Type u_1} [] {f : E} {x : E} {n : ℕ∞} (hf : ContDiffAt n f x) :
ContDiffAt n (fun (x : E) => Complex.sin (f x)) x
theorem ContDiffOn.csin {E : Type u_1} [] {f : E} {s : Set E} {n : ℕ∞} (hf : ContDiffOn n f s) :
ContDiffOn n (fun (x : E) => Complex.sin (f x)) s
theorem ContDiffWithinAt.csin {E : Type u_1} [] {f : E} {x : E} {s : Set E} {n : ℕ∞} (hf : ) :
ContDiffWithinAt n (fun (x : E) => Complex.sin (f x)) s x

#### Complex.cosh#

theorem HasStrictFDerivAt.ccosh {E : Type u_1} [] {f : E} {f' : } {x : E} (hf : ) :
HasStrictFDerivAt (fun (x : E) => Complex.cosh (f x)) (Complex.sinh (f x) f') x
theorem HasFDerivAt.ccosh {E : Type u_1} [] {f : E} {f' : } {x : E} (hf : HasFDerivAt f f' x) :
HasFDerivAt (fun (x : E) => Complex.cosh (f x)) (Complex.sinh (f x) f') x
theorem HasFDerivWithinAt.ccosh {E : Type u_1} [] {f : E} {f' : } {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) :
HasFDerivWithinAt (fun (x : E) => Complex.cosh (f x)) (Complex.sinh (f x) f') s x
theorem DifferentiableWithinAt.ccosh {E : Type u_1} [] {f : E} {x : E} {s : Set E} (hf : ) :
DifferentiableWithinAt (fun (x : E) => Complex.cosh (f x)) s x
@[simp]
theorem DifferentiableAt.ccosh {E : Type u_1} [] {f : E} {x : E} (hc : ) :
DifferentiableAt (fun (x : E) => Complex.cosh (f x)) x
theorem DifferentiableOn.ccosh {E : Type u_1} [] {f : E} {s : Set E} (hc : ) :
DifferentiableOn (fun (x : E) => Complex.cosh (f x)) s
@[simp]
theorem Differentiable.ccosh {E : Type u_1} [] {f : E} (hc : ) :
Differentiable fun (x : E) => Complex.cosh (f x)
theorem fderivWithin_ccosh {E : Type u_1} [] {f : E} {x : E} {s : Set E} (hf : ) (hxs : ) :
fderivWithin (fun (x : E) => Complex.cosh (f x)) s x = Complex.sinh (f x)
@[simp]
theorem fderiv_ccosh {E : Type u_1} [] {f : E} {x : E} (hc : ) :
fderiv (fun (x : E) => Complex.cosh (f x)) x = Complex.sinh (f x) fderiv f x
theorem ContDiff.ccosh {E : Type u_1} [] {f : E} {n : ℕ∞} (h : ) :
ContDiff n fun (x : E) => Complex.cosh (f x)
theorem ContDiffAt.ccosh {E : Type u_1} [] {f : E} {x : E} {n : ℕ∞} (hf : ContDiffAt n f x) :
ContDiffAt n (fun (x : E) => Complex.cosh (f x)) x
theorem ContDiffOn.ccosh {E : Type u_1} [] {f : E} {s : Set E} {n : ℕ∞} (hf : ContDiffOn n f s) :
ContDiffOn n (fun (x : E) => Complex.cosh (f x)) s
theorem ContDiffWithinAt.ccosh {E : Type u_1} [] {f : E} {x : E} {s : Set E} {n : ℕ∞} (hf : ) :
ContDiffWithinAt n (fun (x : E) => Complex.cosh (f x)) s x

#### Complex.sinh#

theorem HasStrictFDerivAt.csinh {E : Type u_1} [] {f : E} {f' : } {x : E} (hf : ) :
HasStrictFDerivAt (fun (x : E) => Complex.sinh (f x)) (Complex.cosh (f x) f') x
theorem HasFDerivAt.csinh {E : Type u_1} [] {f : E} {f' : } {x : E} (hf : HasFDerivAt f f' x) :
HasFDerivAt (fun (x : E) => Complex.sinh (f x)) (Complex.cosh (f x) f') x
theorem HasFDerivWithinAt.csinh {E : Type u_1} [] {f : E} {f' : } {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) :
HasFDerivWithinAt (fun (x : E) => Complex.sinh (f x)) (Complex.cosh (f x) f') s x
theorem DifferentiableWithinAt.csinh {E : Type u_1} [] {f : E} {x : E} {s : Set E} (hf : ) :
DifferentiableWithinAt (fun (x : E) => Complex.sinh (f x)) s x
@[simp]
theorem DifferentiableAt.csinh {E : Type u_1} [] {f : E} {x : E} (hc : ) :
DifferentiableAt (fun (x : E) => Complex.sinh (f x)) x
theorem DifferentiableOn.csinh {E : Type u_1} [] {f : E} {s : Set E} (hc : ) :
DifferentiableOn (fun (x : E) => Complex.sinh (f x)) s
@[simp]
theorem Differentiable.csinh {E : Type u_1} [] {f : E} (hc : ) :
Differentiable fun (x : E) => Complex.sinh (f x)
theorem fderivWithin_csinh {E : Type u_1} [] {f : E} {x : E} {s : Set E} (hf : ) (hxs : ) :
fderivWithin (fun (x : E) => Complex.sinh (f x)) s x = Complex.cosh (f x)
@[simp]
theorem fderiv_csinh {E : Type u_1} [] {f : E} {x : E} (hc : ) :
fderiv (fun (x : E) => Complex.sinh (f x)) x = Complex.cosh (f x) fderiv f x
theorem ContDiff.csinh {E : Type u_1} [] {f : E} {n : ℕ∞} (h : ) :
ContDiff n fun (x : E) => Complex.sinh (f x)
theorem ContDiffAt.csinh {E : Type u_1} [] {f : E} {x : E} {n : ℕ∞} (hf : ContDiffAt n f x) :
ContDiffAt n (fun (x : E) => Complex.sinh (f x)) x
theorem ContDiffOn.csinh {E : Type u_1} [] {f : E} {s : Set E} {n : ℕ∞} (hf : ContDiffOn n f s) :
ContDiffOn n (fun (x : E) => Complex.sinh (f x)) s
theorem ContDiffWithinAt.csinh {E : Type u_1} [] {f : E} {x : E} {s : Set E} {n : ℕ∞} (hf : ) :
ContDiffWithinAt n (fun (x : E) => Complex.sinh (f x)) s x
@[simp]
theorem Real.deriv_sin :
theorem Real.deriv_cos {x : } :
@[simp]
theorem Real.deriv_cos' :
= fun (x : ) =>
@[simp]
theorem Real.deriv_sinh :
@[simp]
theorem Real.deriv_cosh :

sinh is strictly monotone.

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

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

### Simp lemmas for derivatives of fun x => Real.cos (f x) etc., f : ℝ → ℝ#

#### Real.cos#

theorem HasStrictDerivAt.cos {f : } {f' : } {x : } (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (x : ) => Real.cos (f x)) (-Real.sin (f x) * f') x
theorem HasDerivAt.cos {f : } {f' : } {x : } (hf : HasDerivAt f f' x) :
HasDerivAt (fun (x : ) => Real.cos (f x)) (-Real.sin (f x) * f') x
theorem HasDerivWithinAt.cos {f : } {f' : } {x : } {s : } (hf : HasDerivWithinAt f f' s x) :
HasDerivWithinAt (fun (x : ) => Real.cos (f x)) (-Real.sin (f x) * f') s x
theorem derivWithin_cos {f : } {x : } {s : } (hf : ) (hxs : ) :
derivWithin (fun (x : ) => Real.cos (f x)) s x = -Real.sin (f x) * derivWithin f s x
@[simp]
theorem deriv_cos {f : } {x : } (hc : ) :
deriv (fun (x : ) => Real.cos (f x)) x = -Real.sin (f x) * deriv f x

#### Real.sin#

theorem HasStrictDerivAt.sin {f : } {f' : } {x : } (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (x : ) => Real.sin (f x)) (Real.cos (f x) * f') x
theorem HasDerivAt.sin {f : } {f' : } {x : } (hf : HasDerivAt f f' x) :
HasDerivAt (fun (x : ) => Real.sin (f x)) (Real.cos (f x) * f') x
theorem HasDerivWithinAt.sin {f : } {f' : } {x : } {s : } (hf : HasDerivWithinAt f f' s x) :
HasDerivWithinAt (fun (x : ) => Real.sin (f x)) (Real.cos (f x) * f') s x
theorem derivWithin_sin {f : } {x : } {s : } (hf : ) (hxs : ) :
derivWithin (fun (x : ) => Real.sin (f x)) s x = Real.cos (f x) * derivWithin f s x
@[simp]
theorem deriv_sin {f : } {x : } (hc : ) :
deriv (fun (x : ) => Real.sin (f x)) x = Real.cos (f x) * deriv f x

#### Real.cosh#

theorem HasStrictDerivAt.cosh {f : } {f' : } {x : } (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (x : ) => Real.cosh (f x)) (Real.sinh (f x) * f') x
theorem HasDerivAt.cosh {f : } {f' : } {x : } (hf : HasDerivAt f f' x) :
HasDerivAt (fun (x : ) => Real.cosh (f x)) (Real.sinh (f x) * f') x
theorem HasDerivWithinAt.cosh {f : } {f' : } {x : } {s : } (hf : HasDerivWithinAt f f' s x) :
HasDerivWithinAt (fun (x : ) => Real.cosh (f x)) (Real.sinh (f x) * f') s x
theorem derivWithin_cosh {f : } {x : } {s : } (hf : ) (hxs : ) :
derivWithin (fun (x : ) => Real.cosh (f x)) s x = Real.sinh (f x) * derivWithin f s x
@[simp]
theorem deriv_cosh {f : } {x : } (hc : ) :
deriv (fun (x : ) => Real.cosh (f x)) x = Real.sinh (f x) * deriv f x

#### Real.sinh#

theorem HasStrictDerivAt.sinh {f : } {f' : } {x : } (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (x : ) => Real.sinh (f x)) (Real.cosh (f x) * f') x
theorem HasDerivAt.sinh {f : } {f' : } {x : } (hf : HasDerivAt f f' x) :
HasDerivAt (fun (x : ) => Real.sinh (f x)) (Real.cosh (f x) * f') x
theorem HasDerivWithinAt.sinh {f : } {f' : } {x : } {s : } (hf : HasDerivWithinAt f f' s x) :
HasDerivWithinAt (fun (x : ) => Real.sinh (f x)) (Real.cosh (f x) * f') s x
theorem derivWithin_sinh {f : } {x : } {s : } (hf : ) (hxs : ) :
derivWithin (fun (x : ) => Real.sinh (f x)) s x = Real.cosh (f x) * derivWithin f s x
@[simp]
theorem deriv_sinh {f : } {x : } (hc : ) :
deriv (fun (x : ) => Real.sinh (f x)) x = Real.cosh (f x) * deriv f x

### Simp lemmas for derivatives of fun x => Real.cos (f x) etc., f : E → ℝ#

#### Real.cos#

theorem HasStrictFDerivAt.cos {E : Type u_1} [] {f : E} {f' : } {x : E} (hf : ) :
HasStrictFDerivAt (fun (x : E) => Real.cos (f x)) (-Real.sin (f x) f') x
theorem HasFDerivAt.cos {E : Type u_1} [] {f : E} {f' : } {x : E} (hf : HasFDerivAt f f' x) :
HasFDerivAt (fun (x : E) => Real.cos (f x)) (-Real.sin (f x) f') x
theorem HasFDerivWithinAt.cos {E : Type u_1} [] {f : E} {f' : } {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) :
HasFDerivWithinAt (fun (x : E) => Real.cos (f x)) (-Real.sin (f x) f') s x
theorem DifferentiableWithinAt.cos {E : Type u_1} [] {f : E} {x : E} {s : Set E} (hf : ) :
DifferentiableWithinAt (fun (x : E) => Real.cos (f x)) s x
@[simp]
theorem DifferentiableAt.cos {E : Type u_1} [] {f : E} {x : E} (hc : ) :
DifferentiableAt (fun (x : E) => Real.cos (f x)) x
theorem DifferentiableOn.cos {E : Type u_1} [] {f : E} {s : Set E} (hc : ) :
DifferentiableOn (fun (x : E) => Real.cos (f x)) s
@[simp]
theorem Differentiable.cos {E : Type u_1} [] {f : E} (hc : ) :
Differentiable fun (x : E) => Real.cos (f x)
theorem fderivWithin_cos {E : Type u_1} [] {f : E} {x : E} {s : Set E} (hf : ) (hxs : ) :
fderivWithin (fun (x : E) => Real.cos (f x)) s x = -Real.sin (f x)
@[simp]
theorem fderiv_cos {E : Type u_1} [] {f : E} {x : E} (hc : ) :
fderiv (fun (x : E) => Real.cos (f x)) x = -Real.sin (f x) fderiv f x
theorem ContDiff.cos {E : Type u_1} [] {f : E} {n : ℕ∞} (h : ) :
ContDiff n fun (x : E) => Real.cos (f x)
theorem ContDiffAt.cos {E : Type u_1} [] {f : E} {x : E} {n : ℕ∞} (hf : ContDiffAt n f x) :
ContDiffAt n (fun (x : E) => Real.cos (f x)) x
theorem ContDiffOn.cos {E : Type u_1} [] {f : E} {s : Set E} {n : ℕ∞} (hf : ContDiffOn n f s) :
ContDiffOn n (fun (x : E) => Real.cos (f x)) s
theorem ContDiffWithinAt.cos {E : Type u_1} [] {f : E} {x : E} {s : Set E} {n : ℕ∞} (hf : ) :
ContDiffWithinAt n (fun (x : E) => Real.cos (f x)) s x

#### Real.sin#

theorem HasStrictFDerivAt.sin {E : Type u_1} [] {f : E} {f' : } {x : E} (hf : ) :
HasStrictFDerivAt (fun (x : E) => Real.sin (f x)) (Real.cos (f x) f') x
theorem HasFDerivAt.sin {E : Type u_1} [] {f : E} {f' : } {x : E} (hf : HasFDerivAt f f' x) :
HasFDerivAt (fun (x : E) => Real.sin (f x)) (Real.cos (f x) f') x
theorem HasFDerivWithinAt.sin {E : Type u_1} [] {f : E} {f' : } {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) :
HasFDerivWithinAt (fun (x : E) => Real.sin (f x)) (Real.cos (f x) f') s x
theorem DifferentiableWithinAt.sin {E : Type u_1} [] {f : E} {x : E} {s : Set E} (hf : ) :
DifferentiableWithinAt (fun (x : E) => Real.sin (f x)) s x
@[simp]
theorem DifferentiableAt.sin {E : Type u_1} [] {f : E} {x : E} (hc : ) :
DifferentiableAt (fun (x : E) => Real.sin (f x)) x
theorem DifferentiableOn.sin {E : Type u_1} [] {f : E} {s : Set E} (hc : ) :
DifferentiableOn (fun (x : E) => Real.sin (f x)) s
@[simp]
theorem Differentiable.sin {E : Type u_1} [] {f : E} (hc : ) :
Differentiable fun (x : E) => Real.sin (f x)
theorem fderivWithin_sin {E : Type u_1} [] {f : E} {x : E} {s : Set E} (hf : ) (hxs : ) :
fderivWithin (fun (x : E) => Real.sin (f x)) s x = Real.cos (f x)
@[simp]
theorem fderiv_sin {E : Type u_1} [] {f : E} {x : E} (hc : ) :
fderiv (fun (x : E) => Real.sin (f x)) x = Real.cos (f x) fderiv f x
theorem ContDiff.sin {E : Type u_1} [] {f : E} {n : ℕ∞} (h : ) :
ContDiff n fun (x : E) => Real.sin (f x)
theorem ContDiffAt.sin {E : Type u_1} [] {f : E} {x : E} {n : ℕ∞} (hf : ContDiffAt n f x) :
ContDiffAt n (fun (x : E) => Real.sin (f x)) x
theorem ContDiffOn.sin {E : Type u_1} [] {f : E} {s : Set E} {n : ℕ∞} (hf : ContDiffOn n f s) :
ContDiffOn n (fun (x : E) => Real.sin (f x)) s
theorem ContDiffWithinAt.sin {E : Type u_1} [] {f : E} {x : E} {s : Set E} {n : ℕ∞} (hf : ) :
ContDiffWithinAt n (fun (x : E) => Real.sin (f x)) s x

#### Real.cosh#

theorem HasStrictFDerivAt.cosh {E : Type u_1} [] {f : E} {f' : } {x : E} (hf : ) :
HasStrictFDerivAt (fun (x : E) => Real.cosh (f x)) (Real.sinh (f x) f') x
theorem HasFDerivAt.cosh {E : Type u_1} [] {f : E} {f' : } {x : E} (hf : HasFDerivAt f f' x) :
HasFDerivAt (fun (x : E) => Real.cosh (f x)) (Real.sinh (f x) f') x
theorem HasFDerivWithinAt.cosh {E : Type u_1} [] {f : E} {f' : } {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) :
HasFDerivWithinAt (fun (x : E) => Real.cosh (f x)) (Real.sinh (f x) f') s x
theorem DifferentiableWithinAt.cosh {E : Type u_1} [] {f : E} {x : E} {s : Set E} (hf : ) :
DifferentiableWithinAt (fun (x : E) => Real.cosh (f x)) s x
@[simp]
theorem DifferentiableAt.cosh {E : Type u_1} [] {f : E} {x : E} (hc : ) :
DifferentiableAt (fun (x : E) => Real.cosh (f x)) x
theorem DifferentiableOn.cosh {E : Type u_1} [] {f : E} {s : Set E} (hc : ) :
DifferentiableOn (fun (x : E) => Real.cosh (f x)) s
@[simp]
theorem Differentiable.cosh {E : Type u_1} [] {f : E} (hc : ) :
Differentiable fun (x : E) => Real.cosh (f x)
theorem fderivWithin_cosh {E : Type u_1} [] {f : E} {x : E} {s : Set E} (hf : ) (hxs : ) :
fderivWithin (fun (x : E) => Real.cosh (f x)) s x = Real.sinh (f x)
@[simp]
theorem fderiv_cosh {E : Type u_1} [] {f : E} {x : E} (hc : ) :
fderiv (fun (x : E) => Real.cosh (f x)) x = Real.sinh (f x) fderiv f x
theorem ContDiff.cosh {E : Type u_1} [] {f : E} {n : ℕ∞} (h : ) :
ContDiff n fun (x : E) => Real.cosh (f x)
theorem ContDiffAt.cosh {E : Type u_1} [] {f : E} {x : E} {n : ℕ∞} (hf : ContDiffAt n f x) :
ContDiffAt n (fun (x : E) => Real.cosh (f x)) x
theorem ContDiffOn.cosh {E : Type u_1} [] {f : E} {s : Set E} {n : ℕ∞} (hf : ContDiffOn n f s) :
ContDiffOn n (fun (x : E) => Real.cosh (f x)) s
theorem ContDiffWithinAt.cosh {E : Type u_1} [] {f : E} {x : E} {s : Set E} {n : ℕ∞} (hf : ) :
ContDiffWithinAt n (fun (x : E) => Real.cosh (f x)) s x

#### Real.sinh#

theorem HasStrictFDerivAt.sinh {E : Type u_1} [] {f : E} {f' : } {x : E} (hf : ) :
HasStrictFDerivAt (fun (x : E) => Real.sinh (f x)) (Real.cosh (f x) f') x
theorem HasFDerivAt.sinh {E : Type u_1} [] {f : E} {f' : } {x : E} (hf : HasFDerivAt f f' x) :
HasFDerivAt (fun (x : E) => Real.sinh (f x)) (Real.cosh (f x) f') x
theorem HasFDerivWithinAt.sinh {E : Type u_1} [] {f : E} {f' : } {x : E} {s : Set E} (hf : HasFDerivWithinAt f f' s x) :
HasFDerivWithinAt (fun (x : E) => Real.sinh (f x)) (Real.cosh (f x) f') s x
theorem DifferentiableWithinAt.sinh {E : Type u_1} [] {f : E} {x : E} {s : Set E} (hf : ) :
DifferentiableWithinAt (fun (x : E) => Real.sinh (f x)) s x
@[simp]
theorem DifferentiableAt.sinh {E : Type u_1} [] {f : E} {x : E} (hc : ) :
DifferentiableAt (fun (x : E) => Real.sinh (f x)) x
theorem DifferentiableOn.sinh {E : Type u_1} [] {f : E} {s : Set E} (hc : ) :
DifferentiableOn (fun (x : E) => Real.sinh (f x)) s
@[simp]
theorem Differentiable.sinh {E : Type u_1} [] {f : E} (hc : ) :
Differentiable fun (x : E) => Real.sinh (f x)
theorem fderivWithin_sinh {E : Type u_1} [] {f : E} {x : E} {s : Set E} (hf : ) (hxs : ) :
fderivWithin (fun (x : E) => Real.sinh (f x)) s x = Real.cosh (f x)
@[simp]
theorem fderiv_sinh {E : Type u_1} [] {f : E} {x : E} (hc : ) :
fderiv (fun (x : E) => Real.sinh (f x)) x = Real.cosh (f x) fderiv f x
theorem ContDiff.sinh {E : Type u_1} [] {f : E} {n : ℕ∞} (h : ) :
ContDiff n fun (x : E) => Real.sinh (f x)
theorem ContDiffAt.sinh {E : Type u_1} [] {f : E} {x : E} {n : ℕ∞} (hf : ContDiffAt n f x) :
ContDiffAt n (fun (x : E) => Real.sinh (f x)) x
theorem ContDiffOn.sinh {E : Type u_1} [] {f : E} {s : Set E} {n : ℕ∞} (hf : ContDiffOn n f s) :
ContDiffOn n (fun (x : E) => Real.sinh (f x)) s
theorem ContDiffWithinAt.sinh {E : Type u_1} [] {f : E} {x : E} {s : Set E} {n : ℕ∞} (hf : ) :
ContDiffWithinAt n (fun (x : E) => Real.sinh (f x)) s x

Extension for the positivity tactic: Real.sinh is positive/nonnegative/nonzero if its input is.

Instances For