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

theorem Complex.hasStrictDerivAt_sin (x : ℂ) : HasStrictDerivAt sin (cos x) x

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

theorem Complex.hasDerivAt_sin (x : ℂ) : HasDerivAt sin (cos x) x

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

theorem Complex.isEquivalent_sin : Asymptotics.IsEquivalent (nhds 0) sin id

theorem Complex.contDiff_sin {n : WithTop ℕ∞} : ContDiff ℂ n sin

@[simp]

theorem Complex.differentiable_sin : Differentiable ℂ sin

@[simp]

theorem Complex.differentiableAt_sin {x : ℂ} : DifferentiableAt ℂ sin x

theorem Complex.analyticAt_sin {x : ℂ} : AnalyticAt ℂ sin x

The function Complex.sin is complex analytic.

theorem Complex.analyticWithinAt_sin {x : ℂ} {s : Set ℂ} : AnalyticWithinAt ℂ sin s x

The function Complex.sin is complex analytic.

theorem Complex.analyticOnNhd_sin {s : Set ℂ} : AnalyticOnNhd ℂ sin s

The function Complex.sin is complex analytic.

theorem Complex.analyticOn_sin {s : Set ℂ} : AnalyticOn ℂ sin s

The function Complex.sin is complex analytic.

@[simp]

theorem Complex.deriv_sin : deriv sin = cos

theorem Complex.hasStrictDerivAt_cos (x : ℂ) : HasStrictDerivAt cos (-sin x) x

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

theorem Complex.hasDerivAt_cos (x : ℂ) : HasDerivAt cos (-sin x) x

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

theorem Complex.contDiff_cos {n : WithTop ℕ∞} : ContDiff ℂ n cos

@[simp]

theorem Complex.differentiable_cos : Differentiable ℂ cos

@[simp]

theorem Complex.differentiableAt_cos {x : ℂ} : DifferentiableAt ℂ cos x

theorem Complex.analyticAt_cos {x : ℂ} : AnalyticAt ℂ cos x

The function Complex.cos is complex analytic.

theorem Complex.analyticWithinAt_cos {x : ℂ} {s : Set ℂ} : AnalyticWithinAt ℂ cos s x

The function Complex.cos is complex analytic.

theorem Complex.analyticOnNhd_cos {s : Set ℂ} : AnalyticOnNhd ℂ cos s

The function Complex.cos is complex analytic.

theorem Complex.analyticOn_cos {s : Set ℂ} : AnalyticOn ℂ cos s

The function Complex.cos is complex analytic.

theorem Complex.deriv_cos {x : ℂ} : deriv cos x = -sin x

@[simp]

theorem Complex.deriv_cos' : deriv cos = fun (x : ℂ) => -sin x

theorem Complex.hasStrictDerivAt_sinh (x : ℂ) : HasStrictDerivAt sinh (cosh x) x

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

theorem Complex.hasDerivAt_sinh (x : ℂ) : HasDerivAt sinh (cosh x) x

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

theorem Complex.isEquivalent_sinh : Asymptotics.IsEquivalent (nhds 0) sinh id

theorem Complex.contDiff_sinh {n : WithTop ℕ∞} : ContDiff ℂ n sinh

@[simp]

theorem Complex.differentiable_sinh : Differentiable ℂ sinh

@[simp]

theorem Complex.differentiableAt_sinh {x : ℂ} : DifferentiableAt ℂ sinh x

theorem Complex.analyticAt_sinh {x : ℂ} : AnalyticAt ℂ sinh x

The function Complex.sinh is complex analytic.

theorem Complex.analyticWithinAt_sinh {x : ℂ} {s : Set ℂ} : AnalyticWithinAt ℂ sinh s x

The function Complex.sinh is complex analytic.

theorem Complex.analyticOnNhd_sinh {s : Set ℂ} : AnalyticOnNhd ℂ sinh s

The function Complex.sinh is complex analytic.

theorem Complex.analyticOn_sinh {s : Set ℂ} : AnalyticOn ℂ sinh s

The function Complex.sinh is complex analytic.

@[simp]

theorem Complex.deriv_sinh : deriv sinh = cosh

theorem Complex.hasStrictDerivAt_cosh (x : ℂ) : HasStrictDerivAt cosh (sinh x) x

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

theorem Complex.hasDerivAt_cosh (x : ℂ) : HasDerivAt cosh (sinh x) x

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

theorem Complex.contDiff_cosh {n : WithTop ℕ∞} : ContDiff ℂ n cosh

@[simp]

theorem Complex.differentiable_cosh : Differentiable ℂ cosh

@[simp]

theorem Complex.differentiableAt_cosh {x : ℂ} : DifferentiableAt ℂ cosh x

theorem Complex.analyticAt_cosh {x : ℂ} : AnalyticAt ℂ cosh x

The function Complex.cosh is complex analytic.

theorem Complex.analyticWithinAt_cosh {x : ℂ} {s : Set ℂ} : AnalyticWithinAt ℂ cosh s x

The function Complex.cosh is complex analytic.

theorem Complex.analyticOnNhd_cosh {s : Set ℂ} : AnalyticOnNhd ℂ cosh s

The function Complex.cosh is complex analytic.

theorem Complex.analyticOn_cosh {s : Set ℂ} : AnalyticOn ℂ cosh s

The function Complex.cosh is complex analytic.

@[simp]

theorem Complex.deriv_cosh : deriv cosh = sinh

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' : StrongDual ℂ E} {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' : StrongDual ℂ E} {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' : StrongDual ℂ E} {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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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' : StrongDual ℂ E} {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' : StrongDual ℂ E} {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' : StrongDual ℂ E} {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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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' : StrongDual ℂ E} {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' : StrongDual ℂ E} {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' : StrongDual ℂ E} {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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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' : StrongDual ℂ E} {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' : StrongDual ℂ E} {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' : StrongDual ℂ E} {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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (hf : ContDiffWithinAt ℂ n f s x) : ContDiffWithinAt ℂ n (fun (x : E) => Complex.sinh (f x)) s x

theorem Real.hasStrictDerivAt_sin (x : ℝ) : HasStrictDerivAt sin (cos x) x

theorem Real.hasDerivAt_sin (x : ℝ) : HasDerivAt sin (cos x) x

theorem Real.isEquivalent_sin : Asymptotics.IsEquivalent (nhds 0) sin id

theorem Real.contDiff_sin {n : WithTop ℕ∞} : ContDiff ℝ n sin

@[simp]

theorem Real.differentiable_sin : Differentiable ℝ sin

@[simp]

theorem Real.differentiableAt_sin {x : ℝ} : DifferentiableAt ℝ sin x

theorem Real.analyticAt_sin {x : ℝ} : AnalyticAt ℝ sin x

The function Real.sin is real analytic.

theorem Real.analyticWithinAt_sin {x : ℝ} {s : Set ℝ} : AnalyticWithinAt ℝ sin s x

The function Real.sin is real analytic.

theorem Real.analyticOnNhd_sin {s : Set ℝ} : AnalyticOnNhd ℝ sin s

The function Real.sin is real analytic.

theorem Real.analyticOn_sin {s : Set ℝ} : AnalyticOn ℝ sin s

The function Real.sin is real analytic.

@[simp]

theorem Real.deriv_sin : deriv sin = cos

theorem Real.hasStrictDerivAt_cos (x : ℝ) : HasStrictDerivAt cos (-sin x) x

theorem Real.hasDerivAt_cos (x : ℝ) : HasDerivAt cos (-sin x) x

theorem Real.contDiff_cos {n : WithTop ℕ∞} : ContDiff ℝ n cos

@[simp]

theorem Real.differentiable_cos : Differentiable ℝ cos

@[simp]

theorem Real.differentiableAt_cos {x : ℝ} : DifferentiableAt ℝ cos x

theorem Real.analyticAt_cos {x : ℝ} : AnalyticAt ℝ cos x

The function Real.cos is real analytic.

theorem Real.analyticWithinAt_cos {x : ℝ} {s : Set ℝ} : AnalyticWithinAt ℝ cos s x

The function Real.cos is real analytic.

theorem Real.analyticOnNhd_cos {s : Set ℝ} : AnalyticOnNhd ℝ cos s

The function Real.cos is real analytic.

theorem Real.analyticOn_cos {s : Set ℝ} : AnalyticOn ℝ cos s

The function Real.cos is real analytic.

theorem Real.deriv_cos {x : ℝ} : deriv cos x = -sin x

@[simp]

theorem Real.deriv_cos' : deriv cos = fun (x : ℝ) => -sin x

theorem Real.hasStrictDerivAt_sinh (x : ℝ) : HasStrictDerivAt sinh (cosh x) x

theorem Real.hasDerivAt_sinh (x : ℝ) : HasDerivAt sinh (cosh x) x

theorem Real.isEquivalent_sinh : Asymptotics.IsEquivalent (nhds 0) sinh id

theorem Real.contDiff_sinh {n : WithTop ℕ∞} : ContDiff ℝ n sinh

@[simp]

theorem Real.differentiable_sinh : Differentiable ℝ sinh

@[simp]

theorem Real.differentiableAt_sinh {x : ℝ} : DifferentiableAt ℝ sinh x

theorem Real.analyticAt_sinh {x : ℝ} : AnalyticAt ℝ sinh x

The function Real.sinh is real analytic.

theorem Real.analyticWithinAt_sinh {x : ℝ} {s : Set ℝ} : AnalyticWithinAt ℝ sinh s x

The function Real.sinh is real analytic.

theorem Real.analyticOnNhd_sinh {s : Set ℝ} : AnalyticOnNhd ℝ sinh s

The function Real.sinh is real analytic.

theorem Real.analyticOn_sinh {s : Set ℝ} : AnalyticOn ℝ sinh s

The function Real.sinh is real analytic.

@[simp]

theorem Real.deriv_sinh : deriv sinh = cosh

theorem Real.hasStrictDerivAt_cosh (x : ℝ) : HasStrictDerivAt cosh (sinh x) x

theorem Real.hasDerivAt_cosh (x : ℝ) : HasDerivAt cosh (sinh x) x

theorem Real.contDiff_cosh {n : WithTop ℕ∞} : ContDiff ℝ n cosh

@[simp]

theorem Real.differentiable_cosh : Differentiable ℝ cosh

@[simp]

theorem Real.differentiableAt_cosh {x : ℝ} : DifferentiableAt ℝ cosh x

theorem Real.analyticAt_cosh {x : ℝ} : AnalyticAt ℝ cosh x

The function Real.cosh is real analytic.

theorem Real.analyticWithinAt_cosh {x : ℝ} {s : Set ℝ} : AnalyticWithinAt ℝ cosh s x

The function Real.cosh is real analytic.

theorem Real.analyticOnNhd_cosh {s : Set ℝ} : AnalyticOnNhd ℝ cosh s

The function Real.cosh is real analytic.

theorem Real.analyticOn_cosh {s : Set ℝ} : AnalyticOn ℝ cosh s

The function Real.cosh is real analytic.

@[simp]

theorem Real.deriv_cosh : deriv cosh = sinh

theorem Real.sinh_strictMono : StrictMono sinh

sinh is strictly monotone.

theorem Real.sinh_injective : Function.Injective sinh

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

@[simp]

theorem Real.sinh_inj {x y : ℝ} : sinh x = sinh y ↔ x = y

@[simp]

theorem Real.sinh_le_sinh {x y : ℝ} : sinh x ≤ sinh y ↔ x ≤ y

@[simp]

theorem Real.sinh_lt_sinh {x y : ℝ} : sinh x < sinh y ↔ x < y

@[simp]

theorem Real.sinh_eq_zero {x : ℝ} : sinh x = 0 ↔ x = 0

theorem Real.sinh_ne_zero {x : ℝ} : sinh x ≠ 0 ↔ x ≠ 0

@[simp]

theorem Real.sinh_pos_iff {x : ℝ} : 0 < sinh x ↔ 0 < x

@[simp]

theorem Real.sinh_nonpos_iff {x : ℝ} : sinh x ≤ 0 ↔ x ≤ 0

@[simp]

theorem Real.sinh_neg_iff {x : ℝ} : sinh x < 0 ↔ x < 0

@[simp]

theorem Real.sinh_nonneg_iff {x : ℝ} : 0 ≤ sinh x ↔ 0 ≤ x

theorem Real.abs_sinh (x : ℝ) : |sinh x| = sinh |x|

theorem Real.cosh_strictMonoOn : StrictMonoOn cosh (Set.Ici 0)

@[simp]

theorem Real.cosh_le_cosh {x y : ℝ} : cosh x ≤ cosh y ↔ |x| ≤ |y|

@[simp]

theorem Real.cosh_lt_cosh {x y : ℝ} : cosh x < cosh y ↔ |x| < |y|

@[simp]

theorem Real.one_le_cosh (x : ℝ) : 1 ≤ cosh x

@[simp]

theorem Real.one_lt_cosh {x : ℝ} : 1 < cosh x ↔ x ≠ 0

theorem Real.sinh_sub_id_strictMono : StrictMono fun (x : ℝ) => sinh x - x

@[simp]

theorem Real.self_le_sinh_iff {x : ℝ} : x ≤ sinh x ↔ 0 ≤ x

@[simp]

theorem Real.sinh_le_self_iff {x : ℝ} : sinh x ≤ x ↔ x ≤ 0

@[simp]

theorem Real.self_lt_sinh_iff {x : ℝ} : x < sinh x ↔ 0 < x

@[simp]

theorem Real.sinh_lt_self_iff {x : ℝ} : sinh x < x ↔ x < 0

Simp lemmas for iterated derivaties of sin and cos.

@[simp]

theorem Complex.iteratedDeriv_add_one_sin (n : ℕ) : iteratedDeriv (n + 1) sin = iteratedDeriv n cos

@[simp]

theorem Complex.iteratedDeriv_add_one_cos (n : ℕ) : iteratedDeriv (n + 1) cos = -iteratedDeriv n sin

@[simp]

theorem Complex.iteratedDeriv_even_sin (n : ℕ) : iteratedDeriv (2 * n) sin = (-1) ^ n * sin

@[simp]

theorem Complex.iteratedDeriv_even_cos (n : ℕ) : iteratedDeriv (2 * n) cos = (-1) ^ n * cos

theorem Complex.iteratedDeriv_odd_sin (n : ℕ) : iteratedDeriv (2 * n + 1) sin = (-1) ^ n * cos

theorem Complex.iteratedDeriv_odd_cos (n : ℕ) : iteratedDeriv (2 * n + 1) cos = (-1) ^ (n + 1) * sin

theorem Complex.differentiable_iteratedDeriv_sin (n : ℕ) : Differentiable ℂ (iteratedDeriv n sin)

theorem Complex.differentiable_iteratedDeriv_cos (n : ℕ) : Differentiable ℂ (iteratedDeriv n cos)

@[simp]

theorem Complex.iteratedDeriv_add_one_sinh (n : ℕ) : iteratedDeriv (n + 1) sinh = iteratedDeriv n cosh

@[simp]

theorem Complex.iteratedDeriv_add_one_cosh (n : ℕ) : iteratedDeriv (n + 1) cosh = iteratedDeriv n sinh

@[simp]

theorem Complex.iteratedDeriv_even_sinh (n : ℕ) : iteratedDeriv (2 * n) sinh = sinh

@[simp]

theorem Complex.iteratedDeriv_even_cosh (n : ℕ) : iteratedDeriv (2 * n) cosh = cosh

theorem Complex.iteratedDeriv_odd_sinh (n : ℕ) : iteratedDeriv (2 * n + 1) sinh = cosh

theorem Complex.iteratedDeriv_odd_cosh (n : ℕ) : iteratedDeriv (2 * n + 1) cosh = sinh

theorem Complex.differentiable_iteratedDeriv_sinh (n : ℕ) : Differentiable ℂ (iteratedDeriv n sinh)

theorem Complex.differentiable_iteratedDeriv_cosh (n : ℕ) : Differentiable ℂ (iteratedDeriv n cosh)

@[simp]

theorem Real.iteratedDeriv_add_one_sin (n : ℕ) : iteratedDeriv (n + 1) sin = iteratedDeriv n cos

@[simp]

theorem Real.iteratedDeriv_add_one_cos (n : ℕ) : iteratedDeriv (n + 1) cos = -iteratedDeriv n sin

@[simp]

theorem Real.iteratedDeriv_even_sin (n : ℕ) : iteratedDeriv (2 * n) sin = (-1) ^ n * sin

@[simp]

theorem Real.iteratedDeriv_even_cos (n : ℕ) : iteratedDeriv (2 * n) cos = (-1) ^ n * cos

theorem Real.iteratedDeriv_odd_sin (n : ℕ) : iteratedDeriv (2 * n + 1) sin = (-1) ^ n * cos

theorem Real.iteratedDeriv_odd_cos (n : ℕ) : iteratedDeriv (2 * n + 1) cos = (-1) ^ (n + 1) * sin

theorem Real.differentiable_iteratedDeriv_sin (n : ℕ) : Differentiable ℝ (iteratedDeriv n sin)

theorem Real.differentiable_iteratedDeriv_cos (n : ℕ) : Differentiable ℝ (iteratedDeriv n cos)

theorem Real.abs_iteratedDeriv_sin_le_one (n : ℕ) (x : ℝ) : |iteratedDeriv n sin x| ≤ 1

theorem Real.abs_iteratedDeriv_cos_le_one (n : ℕ) (x : ℝ) : |iteratedDeriv n cos x| ≤ 1

@[simp]

theorem Real.iteratedDeriv_add_one_sinh (n : ℕ) : iteratedDeriv (n + 1) sinh = iteratedDeriv n cosh

@[simp]

theorem Real.iteratedDeriv_add_one_cosh (n : ℕ) : iteratedDeriv (n + 1) cosh = iteratedDeriv n sinh

@[simp]

theorem Real.iteratedDeriv_even_sinh (n : ℕ) : iteratedDeriv (2 * n) sinh = sinh

@[simp]

theorem Real.iteratedDeriv_even_cosh (n : ℕ) : iteratedDeriv (2 * n) cosh = cosh

theorem Real.iteratedDeriv_odd_sinh (n : ℕ) : iteratedDeriv (2 * n + 1) sinh = cosh

theorem Real.iteratedDeriv_odd_cosh (n : ℕ) : iteratedDeriv (2 * n + 1) cosh = sinh

theorem Real.differentiable_iteratedDeriv_sinh (n : ℕ) : Differentiable ℝ (iteratedDeriv n sinh)

theorem Real.differentiable_iteratedDeriv_cosh (n : ℕ) : Differentiable ℝ (iteratedDeriv n cosh)

@[simp]

theorem Real.iteratedDerivWithin_sin_Icc (n : ℕ) {a b : ℝ} (h : a < b) {x : ℝ} (hx : x ∈ Set.Icc a b) : iteratedDerivWithin n sin (Set.Icc a b) x = iteratedDeriv n sin x

@[simp]

theorem Real.iteratedDerivWithin_cos_Icc (n : ℕ) {a b : ℝ} (h : a < b) {x : ℝ} (hx : x ∈ Set.Icc a b) : iteratedDerivWithin n cos (Set.Icc a b) x = iteratedDeriv n cos x

@[simp]

theorem Real.iteratedDerivWithin_sinh_Icc (n : ℕ) {a b : ℝ} (h : a < b) {x : ℝ} (hx : x ∈ Set.Icc a b) : iteratedDerivWithin n sinh (Set.Icc a b) x = iteratedDeriv n sinh x

@[simp]

theorem Real.iteratedDerivWithin_cosh_Icc (n : ℕ) {a b : ℝ} (h : a < b) {x : ℝ} (hx : x ∈ Set.Icc a b) : iteratedDerivWithin n cosh (Set.Icc a b) x = iteratedDeriv n cosh x

@[simp]

theorem Real.iteratedDerivWithin_sin_Ioo (n : ℕ) {a b x : ℝ} (hx : x ∈ Set.Ioo a b) : iteratedDerivWithin n sin (Set.Ioo a b) x = iteratedDeriv n sin x

@[simp]

theorem Real.iteratedDerivWithin_cos_Ioo (n : ℕ) {a b x : ℝ} (hx : x ∈ Set.Ioo a b) : iteratedDerivWithin n cos (Set.Ioo a b) x = iteratedDeriv n cos x

@[simp]

theorem Real.iteratedDerivWithin_sinh_Ioo (n : ℕ) {a b x : ℝ} (hx : x ∈ Set.Ioo a b) : iteratedDerivWithin n sinh (Set.Ioo a b) x = iteratedDeriv n sinh x

@[simp]

theorem Real.iteratedDerivWithin_cosh_Ioo (n : ℕ) {a b x : ℝ} (hx : x ∈ Set.Ioo a b) : iteratedDerivWithin n cosh (Set.Ioo a b) x = iteratedDeriv n cosh x

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' : StrongDual ℝ E} {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' : StrongDual ℝ E} {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' : StrongDual ℝ E} {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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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' : StrongDual ℝ E} {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' : StrongDual ℝ E} {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' : StrongDual ℝ E} {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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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' : StrongDual ℝ E} {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' : StrongDual ℝ E} {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' : StrongDual ℝ E} {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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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' : StrongDual ℝ E} {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' : StrongDual ℝ E} {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' : StrongDual ℝ E} {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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (hf : ContDiffWithinAt ℝ n f s x) : ContDiffWithinAt ℝ n (fun (x : E) => Real.sinh (f x)) s x

@[simp]

theorem Complex.logDeriv_sin : logDeriv sin = cot

@[simp]

theorem Real.logDeriv_sin : logDeriv sin = cot

@[simp]

theorem Complex.logDeriv_cos : logDeriv cos = -tan

@[simp]

theorem Real.logDeriv_cos : logDeriv cos = -tan

@[simp]

theorem Complex.logDeriv_cosh : logDeriv cosh = tanh

@[simp]

theorem Real.logDeriv_cosh : logDeriv cosh = tanh

@[simp]

theorem Complex.LogDeriv_exp : logDeriv exp = 1

@[simp]

theorem Real.LogDeriv_exp : logDeriv exp = 1

def Mathlib.Meta.Positivity.evalSinh : PositivityExt

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

Equations

• One or more equations did not get rendered due to their size.