Documentation

Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

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.

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.

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 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 : Set } (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 : Set } (hf : DifferentiableWithinAt f s x) (hxs : UniqueDiffWithinAt s x) :
derivWithin (fun (x : ) => Complex.cos (f x)) s x = -Complex.sin (f x) * derivWithin f s x
@[simp]
theorem deriv_ccos {f : } {x : } (hc : DifferentiableAt f x) :
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 : Set } (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 : Set } (hf : DifferentiableWithinAt f s x) (hxs : UniqueDiffWithinAt s x) :
derivWithin (fun (x : ) => Complex.sin (f x)) s x = Complex.cos (f x) * derivWithin f s x
@[simp]
theorem deriv_csin {f : } {x : } (hc : DifferentiableAt f x) :
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 : Set } (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 : Set } (hf : DifferentiableWithinAt f s x) (hxs : UniqueDiffWithinAt s x) :
derivWithin (fun (x : ) => Complex.cosh (f x)) s x = Complex.sinh (f x) * derivWithin f s x
@[simp]
theorem deriv_ccosh {f : } {x : } (hc : DifferentiableAt f x) :
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 : Set } (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 : Set } (hf : DifferentiableWithinAt f s x) (hxs : UniqueDiffWithinAt s x) :
derivWithin (fun (x : ) => Complex.sinh (f x)) s x = Complex.cosh (f x) * derivWithin f s x
@[simp]
theorem deriv_csinh {f : } {x : } (hc : DifferentiableAt f x) :
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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {x : E} (hf : HasStrictFDerivAt f f' x) :
HasStrictFDerivAt (fun (x : E) => Complex.cos (f x)) (-Complex.sin (f x) f') x
theorem HasFDerivAt.ccos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} (hf : DifferentiableWithinAt f s x) :
DifferentiableWithinAt (fun (x : E) => Complex.cos (f x)) s x
@[simp]
theorem DifferentiableAt.ccos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} (hc : DifferentiableAt f x) :
DifferentiableAt (fun (x : E) => Complex.cos (f x)) x
theorem DifferentiableOn.ccos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {s : Set E} (hc : DifferentiableOn f s) :
DifferentiableOn (fun (x : E) => Complex.cos (f x)) s
@[simp]
theorem Differentiable.ccos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} (hc : Differentiable f) :
Differentiable fun (x : E) => Complex.cos (f x)
theorem fderivWithin_ccos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} (hf : DifferentiableWithinAt f s x) (hxs : UniqueDiffWithinAt s x) :
fderivWithin (fun (x : E) => Complex.cos (f x)) s x = -Complex.sin (f x) fderivWithin f s x
@[simp]
theorem fderiv_ccos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} (hc : DifferentiableAt f x) :
fderiv (fun (x : E) => Complex.cos (f x)) x = -Complex.sin (f x) fderiv f x
theorem ContDiff.ccos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {n : ℕ∞} (h : ContDiff n f) :
ContDiff n fun (x : E) => Complex.cos (f x)
theorem ContDiffAt.ccos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {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} [NormedAddCommGroup E] [NormedSpace E] {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} {n : ℕ∞} (hf : ContDiffWithinAt n f s x) :
ContDiffWithinAt n (fun (x : E) => Complex.cos (f x)) s x

Complex.sin #

theorem HasStrictFDerivAt.csin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {x : E} (hf : HasStrictFDerivAt f f' x) :
HasStrictFDerivAt (fun (x : E) => Complex.sin (f x)) (Complex.cos (f x) f') x
theorem HasFDerivAt.csin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} (hf : DifferentiableWithinAt f s x) :
DifferentiableWithinAt (fun (x : E) => Complex.sin (f x)) s x
@[simp]
theorem DifferentiableAt.csin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} (hc : DifferentiableAt f x) :
DifferentiableAt (fun (x : E) => Complex.sin (f x)) x
theorem DifferentiableOn.csin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {s : Set E} (hc : DifferentiableOn f s) :
DifferentiableOn (fun (x : E) => Complex.sin (f x)) s
@[simp]
theorem Differentiable.csin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} (hc : Differentiable f) :
Differentiable fun (x : E) => Complex.sin (f x)
theorem fderivWithin_csin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} (hf : DifferentiableWithinAt f s x) (hxs : UniqueDiffWithinAt s x) :
fderivWithin (fun (x : E) => Complex.sin (f x)) s x = Complex.cos (f x) fderivWithin f s x
@[simp]
theorem fderiv_csin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} (hc : DifferentiableAt f x) :
fderiv (fun (x : E) => Complex.sin (f x)) x = Complex.cos (f x) fderiv f x
theorem ContDiff.csin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {n : ℕ∞} (h : ContDiff n f) :
ContDiff n fun (x : E) => Complex.sin (f x)
theorem ContDiffAt.csin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {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} [NormedAddCommGroup E] [NormedSpace E] {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} {n : ℕ∞} (hf : ContDiffWithinAt n f s x) :
ContDiffWithinAt n (fun (x : E) => Complex.sin (f x)) s x

Complex.cosh #

theorem HasStrictFDerivAt.ccosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {x : E} (hf : HasStrictFDerivAt f f' x) :
HasStrictFDerivAt (fun (x : E) => Complex.cosh (f x)) (Complex.sinh (f x) f') x
theorem HasFDerivAt.ccosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} (hf : DifferentiableWithinAt f s x) :
DifferentiableWithinAt (fun (x : E) => Complex.cosh (f x)) s x
@[simp]
theorem DifferentiableAt.ccosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} (hc : DifferentiableAt f x) :
DifferentiableAt (fun (x : E) => Complex.cosh (f x)) x
theorem DifferentiableOn.ccosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {s : Set E} (hc : DifferentiableOn f s) :
DifferentiableOn (fun (x : E) => Complex.cosh (f x)) s
@[simp]
theorem Differentiable.ccosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} (hc : Differentiable f) :
Differentiable fun (x : E) => Complex.cosh (f x)
theorem fderivWithin_ccosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} (hf : DifferentiableWithinAt f s x) (hxs : UniqueDiffWithinAt s x) :
fderivWithin (fun (x : E) => Complex.cosh (f x)) s x = Complex.sinh (f x) fderivWithin f s x
@[simp]
theorem fderiv_ccosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} (hc : DifferentiableAt f x) :
fderiv (fun (x : E) => Complex.cosh (f x)) x = Complex.sinh (f x) fderiv f x
theorem ContDiff.ccosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {n : ℕ∞} (h : ContDiff n f) :
ContDiff n fun (x : E) => Complex.cosh (f x)
theorem ContDiffAt.ccosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {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} [NormedAddCommGroup E] [NormedSpace E] {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} {n : ℕ∞} (hf : ContDiffWithinAt n f s x) :
ContDiffWithinAt n (fun (x : E) => Complex.cosh (f x)) s x

Complex.sinh #

theorem HasStrictFDerivAt.csinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {x : E} (hf : HasStrictFDerivAt f f' x) :
HasStrictFDerivAt (fun (x : E) => Complex.sinh (f x)) (Complex.cosh (f x) f') x
theorem HasFDerivAt.csinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} (hf : DifferentiableWithinAt f s x) :
DifferentiableWithinAt (fun (x : E) => Complex.sinh (f x)) s x
@[simp]
theorem DifferentiableAt.csinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} (hc : DifferentiableAt f x) :
DifferentiableAt (fun (x : E) => Complex.sinh (f x)) x
theorem DifferentiableOn.csinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {s : Set E} (hc : DifferentiableOn f s) :
DifferentiableOn (fun (x : E) => Complex.sinh (f x)) s
@[simp]
theorem Differentiable.csinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} (hc : Differentiable f) :
Differentiable fun (x : E) => Complex.sinh (f x)
theorem fderivWithin_csinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} (hf : DifferentiableWithinAt f s x) (hxs : UniqueDiffWithinAt s x) :
fderivWithin (fun (x : E) => Complex.sinh (f x)) s x = Complex.cosh (f x) fderivWithin f s x
@[simp]
theorem fderiv_csinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} (hc : DifferentiableAt f x) :
fderiv (fun (x : E) => Complex.sinh (f x)) x = Complex.cosh (f x) fderiv f x
theorem ContDiff.csinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {n : ℕ∞} (h : ContDiff n f) :
ContDiff n fun (x : E) => Complex.sinh (f x)
theorem ContDiffAt.csinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {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} [NormedAddCommGroup E] [NormedSpace E] {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} {n : ℕ∞} (hf : ContDiffWithinAt n f s x) :
ContDiffWithinAt n (fun (x : E) => Complex.sinh (f x)) s x
@[simp]
theorem Real.deriv_cos' :
deriv Real.cos = fun (x : ) => -Real.sin x

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_eq_zero {x : } :
Real.sinh x = 0 x = 0
@[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 : } :
Real.cosh x < Real.cosh y |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 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 : Set } (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 : Set } (hf : DifferentiableWithinAt f s x) (hxs : UniqueDiffWithinAt s x) :
derivWithin (fun (x : ) => Real.cos (f x)) s x = -Real.sin (f x) * derivWithin f s x
@[simp]
theorem deriv_cos {f : } {x : } (hc : DifferentiableAt f x) :
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 : Set } (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 : Set } (hf : DifferentiableWithinAt f s x) (hxs : UniqueDiffWithinAt s x) :
derivWithin (fun (x : ) => Real.sin (f x)) s x = Real.cos (f x) * derivWithin f s x
@[simp]
theorem deriv_sin {f : } {x : } (hc : DifferentiableAt f x) :
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 : Set } (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 : Set } (hf : DifferentiableWithinAt f s x) (hxs : UniqueDiffWithinAt s x) :
derivWithin (fun (x : ) => Real.cosh (f x)) s x = Real.sinh (f x) * derivWithin f s x
@[simp]
theorem deriv_cosh {f : } {x : } (hc : DifferentiableAt f x) :
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 : Set } (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 : Set } (hf : DifferentiableWithinAt f s x) (hxs : UniqueDiffWithinAt s x) :
derivWithin (fun (x : ) => Real.sinh (f x)) s x = Real.cosh (f x) * derivWithin f s x
@[simp]
theorem deriv_sinh {f : } {x : } (hc : DifferentiableAt f x) :
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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {x : E} (hf : HasStrictFDerivAt f f' x) :
HasStrictFDerivAt (fun (x : E) => Real.cos (f x)) (-Real.sin (f x) f') x
theorem HasFDerivAt.cos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} (hf : DifferentiableWithinAt f s x) :
DifferentiableWithinAt (fun (x : E) => Real.cos (f x)) s x
@[simp]
theorem DifferentiableAt.cos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} (hc : DifferentiableAt f x) :
DifferentiableAt (fun (x : E) => Real.cos (f x)) x
theorem DifferentiableOn.cos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {s : Set E} (hc : DifferentiableOn f s) :
DifferentiableOn (fun (x : E) => Real.cos (f x)) s
@[simp]
theorem Differentiable.cos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} (hc : Differentiable f) :
Differentiable fun (x : E) => Real.cos (f x)
theorem fderivWithin_cos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} (hf : DifferentiableWithinAt f s x) (hxs : UniqueDiffWithinAt s x) :
fderivWithin (fun (x : E) => Real.cos (f x)) s x = -Real.sin (f x) fderivWithin f s x
@[simp]
theorem fderiv_cos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} (hc : DifferentiableAt f x) :
fderiv (fun (x : E) => Real.cos (f x)) x = -Real.sin (f x) fderiv f x
theorem ContDiff.cos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {n : ℕ∞} (h : ContDiff n f) :
ContDiff n fun (x : E) => Real.cos (f x)
theorem ContDiffAt.cos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {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} [NormedAddCommGroup E] [NormedSpace E] {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} {n : ℕ∞} (hf : ContDiffWithinAt n f s x) :
ContDiffWithinAt n (fun (x : E) => Real.cos (f x)) s x

Real.sin #

theorem HasStrictFDerivAt.sin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {x : E} (hf : HasStrictFDerivAt f f' x) :
HasStrictFDerivAt (fun (x : E) => Real.sin (f x)) (Real.cos (f x) f') x
theorem HasFDerivAt.sin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} (hf : DifferentiableWithinAt f s x) :
DifferentiableWithinAt (fun (x : E) => Real.sin (f x)) s x
@[simp]
theorem DifferentiableAt.sin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} (hc : DifferentiableAt f x) :
DifferentiableAt (fun (x : E) => Real.sin (f x)) x
theorem DifferentiableOn.sin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {s : Set E} (hc : DifferentiableOn f s) :
DifferentiableOn (fun (x : E) => Real.sin (f x)) s
@[simp]
theorem Differentiable.sin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} (hc : Differentiable f) :
Differentiable fun (x : E) => Real.sin (f x)
theorem fderivWithin_sin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} (hf : DifferentiableWithinAt f s x) (hxs : UniqueDiffWithinAt s x) :
fderivWithin (fun (x : E) => Real.sin (f x)) s x = Real.cos (f x) fderivWithin f s x
@[simp]
theorem fderiv_sin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} (hc : DifferentiableAt f x) :
fderiv (fun (x : E) => Real.sin (f x)) x = Real.cos (f x) fderiv f x
theorem ContDiff.sin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {n : ℕ∞} (h : ContDiff n f) :
ContDiff n fun (x : E) => Real.sin (f x)
theorem ContDiffAt.sin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {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} [NormedAddCommGroup E] [NormedSpace E] {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} {n : ℕ∞} (hf : ContDiffWithinAt n f s x) :
ContDiffWithinAt n (fun (x : E) => Real.sin (f x)) s x

Real.cosh #

theorem HasStrictFDerivAt.cosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {x : E} (hf : HasStrictFDerivAt f f' x) :
HasStrictFDerivAt (fun (x : E) => Real.cosh (f x)) (Real.sinh (f x) f') x
theorem HasFDerivAt.cosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} (hf : DifferentiableWithinAt f s x) :
DifferentiableWithinAt (fun (x : E) => Real.cosh (f x)) s x
@[simp]
theorem DifferentiableAt.cosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} (hc : DifferentiableAt f x) :
DifferentiableAt (fun (x : E) => Real.cosh (f x)) x
theorem DifferentiableOn.cosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {s : Set E} (hc : DifferentiableOn f s) :
DifferentiableOn (fun (x : E) => Real.cosh (f x)) s
@[simp]
theorem Differentiable.cosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} (hc : Differentiable f) :
Differentiable fun (x : E) => Real.cosh (f x)
theorem fderivWithin_cosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} (hf : DifferentiableWithinAt f s x) (hxs : UniqueDiffWithinAt s x) :
fderivWithin (fun (x : E) => Real.cosh (f x)) s x = Real.sinh (f x) fderivWithin f s x
@[simp]
theorem fderiv_cosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} (hc : DifferentiableAt f x) :
fderiv (fun (x : E) => Real.cosh (f x)) x = Real.sinh (f x) fderiv f x
theorem ContDiff.cosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {n : ℕ∞} (h : ContDiff n f) :
ContDiff n fun (x : E) => Real.cosh (f x)
theorem ContDiffAt.cosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {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} [NormedAddCommGroup E] [NormedSpace E] {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} {n : ℕ∞} (hf : ContDiffWithinAt n f s x) :
ContDiffWithinAt n (fun (x : E) => Real.cosh (f x)) s x

Real.sinh #

theorem HasStrictFDerivAt.sinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {x : E} (hf : HasStrictFDerivAt f f' x) :
HasStrictFDerivAt (fun (x : E) => Real.sinh (f x)) (Real.cosh (f x) f') x
theorem HasFDerivAt.sinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {f' : E →L[] } {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} (hf : DifferentiableWithinAt f s x) :
DifferentiableWithinAt (fun (x : E) => Real.sinh (f x)) s x
@[simp]
theorem DifferentiableAt.sinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} (hc : DifferentiableAt f x) :
DifferentiableAt (fun (x : E) => Real.sinh (f x)) x
theorem DifferentiableOn.sinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {s : Set E} (hc : DifferentiableOn f s) :
DifferentiableOn (fun (x : E) => Real.sinh (f x)) s
@[simp]
theorem Differentiable.sinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} (hc : Differentiable f) :
Differentiable fun (x : E) => Real.sinh (f x)
theorem fderivWithin_sinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} (hf : DifferentiableWithinAt f s x) (hxs : UniqueDiffWithinAt s x) :
fderivWithin (fun (x : E) => Real.sinh (f x)) s x = Real.cosh (f x) fderivWithin f s x
@[simp]
theorem fderiv_sinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} (hc : DifferentiableAt f x) :
fderiv (fun (x : E) => Real.sinh (f x)) x = Real.cosh (f x) fderiv f x
theorem ContDiff.sinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {n : ℕ∞} (h : ContDiff n f) :
ContDiff n fun (x : E) => Real.sinh (f x)
theorem ContDiffAt.sinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {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} [NormedAddCommGroup E] [NormedSpace E] {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} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} {s : Set E} {n : ℕ∞} (hf : ContDiffWithinAt n f s x) :
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