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

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

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

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

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

source
theorem Complex.contDiff_sin {n : ℕ∞} :
ContDiff ℂ n Complex.sin
source
theorem Complex.differentiable_sin :
Differentiable ℂ Complex.sin
source
theorem Complex.differentiableAt_sin {x : ℂ} :
DifferentiableAt ℂ Complex.sin x
source
@[simp]
theorem Complex.deriv_sin :
deriv Complex.sin = Complex.cos
source
theorem Complex.hasStrictDerivAt_cos (x : ℂ) :
HasStrictDerivAt Complex.cos (-x.sin) x

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

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

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

source
theorem Complex.contDiff_cos {n : ℕ∞} :
ContDiff ℂ n Complex.cos
source
theorem Complex.differentiable_cos :
Differentiable ℂ Complex.cos
source
theorem Complex.differentiableAt_cos {x : ℂ} :
DifferentiableAt ℂ Complex.cos x
source
theorem Complex.deriv_cos {x : ℂ} :
deriv Complex.cos x = -x.sin
source
@[simp]
theorem Complex.deriv_cos' :
deriv Complex.cos = fun (x : ℂ) => -x.sin
source
theorem Complex.hasStrictDerivAt_sinh (x : ℂ) :
HasStrictDerivAt Complex.sinh x.cosh x

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

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

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

source
theorem Complex.contDiff_sinh {n : ℕ∞} :
ContDiff ℂ n Complex.sinh
source
theorem Complex.differentiable_sinh :
Differentiable ℂ Complex.sinh
source
theorem Complex.differentiableAt_sinh {x : ℂ} :
DifferentiableAt ℂ Complex.sinh x
source
@[simp]
theorem Complex.deriv_sinh :
deriv Complex.sinh = Complex.cosh
source
theorem Complex.hasStrictDerivAt_cosh (x : ℂ) :
HasStrictDerivAt Complex.cosh x.sinh x

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

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

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

source
theorem Complex.contDiff_cosh {n : ℕ∞} :
ContDiff ℂ n Complex.cosh
source
theorem Complex.differentiable_cosh :
Differentiable ℂ Complex.cosh
source
theorem Complex.differentiableAt_cosh {x : ℂ} :
DifferentiableAt ℂ Complex.cosh x
source
@[simp]
theorem Complex.deriv_cosh :
deriv Complex.cosh = Complex.sinh

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

Complex.cos #

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

Complex.sin #

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

Complex.cosh #

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

Complex.sinh #

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

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

Complex.cos #

source
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) => (f x).cos) (-(f x).sin • f') x
source
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) => (f x).cos) (-(f x).sin • f') x
source
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) => (f x).cos) (-(f x).sin • f') s x
source
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) => (f x).cos) s x
source
@[simp]
theorem DifferentiableAt.ccos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {x : E} (hc : DifferentiableAt ℂ f x) :
DifferentiableAt ℂ (fun (x : E) => (f x).cos) x
source
theorem DifferentiableOn.ccos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {s : Set E} (hc : DifferentiableOn ℂ f s) :
DifferentiableOn ℂ (fun (x : E) => (f x).cos) s
source
@[simp]
theorem Differentiable.ccos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} (hc : Differentiable ℂ f) :
Differentiable ℂ fun (x : E) => (f x).cos
source
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) => (f x).cos) s x = -(f x).sin • fderivWithin ℂ f s x
source
@[simp]
theorem fderiv_ccos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {x : E} (hc : DifferentiableAt ℂ f x) :
fderiv ℂ (fun (x : E) => (f x).cos) x = -(f x).sin • fderiv ℂ f x
source
theorem ContDiff.ccos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {n : ℕ∞} (h : ContDiff ℂ n f) :
ContDiff ℂ n fun (x : E) => (f x).cos
source
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) => (f x).cos) x
source
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) => (f x).cos) s
source
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) => (f x).cos) s x

Complex.sin #

source
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) => (f x).sin) ((f x).cos • f') x
source
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) => (f x).sin) ((f x).cos • f') x
source
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) => (f x).sin) ((f x).cos • f') s x
source
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) => (f x).sin) s x
source
@[simp]
theorem DifferentiableAt.csin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {x : E} (hc : DifferentiableAt ℂ f x) :
DifferentiableAt ℂ (fun (x : E) => (f x).sin) x
source
theorem DifferentiableOn.csin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {s : Set E} (hc : DifferentiableOn ℂ f s) :
DifferentiableOn ℂ (fun (x : E) => (f x).sin) s
source
@[simp]
theorem Differentiable.csin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} (hc : Differentiable ℂ f) :
Differentiable ℂ fun (x : E) => (f x).sin
source
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) => (f x).sin) s x = (f x).cos • fderivWithin ℂ f s x
source
@[simp]
theorem fderiv_csin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {x : E} (hc : DifferentiableAt ℂ f x) :
fderiv ℂ (fun (x : E) => (f x).sin) x = (f x).cos • fderiv ℂ f x
source
theorem ContDiff.csin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {n : ℕ∞} (h : ContDiff ℂ n f) :
ContDiff ℂ n fun (x : E) => (f x).sin
source
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) => (f x).sin) x
source
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) => (f x).sin) s
source
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) => (f x).sin) s x

Complex.cosh #

source
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) => (f x).cosh) ((f x).sinh • f') x
source
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) => (f x).cosh) ((f x).sinh • f') x
source
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) => (f x).cosh) ((f x).sinh • f') s x
source
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) => (f x).cosh) s x
source
@[simp]
theorem DifferentiableAt.ccosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {x : E} (hc : DifferentiableAt ℂ f x) :
DifferentiableAt ℂ (fun (x : E) => (f x).cosh) x
source
theorem DifferentiableOn.ccosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {s : Set E} (hc : DifferentiableOn ℂ f s) :
DifferentiableOn ℂ (fun (x : E) => (f x).cosh) s
source
@[simp]
theorem Differentiable.ccosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} (hc : Differentiable ℂ f) :
Differentiable ℂ fun (x : E) => (f x).cosh
source
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) => (f x).cosh) s x = (f x).sinh • fderivWithin ℂ f s x
source
@[simp]
theorem fderiv_ccosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {x : E} (hc : DifferentiableAt ℂ f x) :
fderiv ℂ (fun (x : E) => (f x).cosh) x = (f x).sinh • fderiv ℂ f x
source
theorem ContDiff.ccosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {n : ℕ∞} (h : ContDiff ℂ n f) :
ContDiff ℂ n fun (x : E) => (f x).cosh
source
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) => (f x).cosh) x
source
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) => (f x).cosh) s
source
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) => (f x).cosh) s x

Complex.sinh #

source
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) => (f x).sinh) ((f x).cosh • f') x
source
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) => (f x).sinh) ((f x).cosh • f') x
source
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) => (f x).sinh) ((f x).cosh • f') s x
source
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) => (f x).sinh) s x
source
@[simp]
theorem DifferentiableAt.csinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {x : E} (hc : DifferentiableAt ℂ f x) :
DifferentiableAt ℂ (fun (x : E) => (f x).sinh) x
source
theorem DifferentiableOn.csinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {s : Set E} (hc : DifferentiableOn ℂ f s) :
DifferentiableOn ℂ (fun (x : E) => (f x).sinh) s
source
@[simp]
theorem Differentiable.csinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} (hc : Differentiable ℂ f) :
Differentiable ℂ fun (x : E) => (f x).sinh
source
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) => (f x).sinh) s x = (f x).cosh • fderivWithin ℂ f s x
source
@[simp]
theorem fderiv_csinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {x : E} (hc : DifferentiableAt ℂ f x) :
fderiv ℂ (fun (x : E) => (f x).sinh) x = (f x).cosh • fderiv ℂ f x
source
theorem ContDiff.csinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {n : ℕ∞} (h : ContDiff ℂ n f) :
ContDiff ℂ n fun (x : E) => (f x).sinh
source
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) => (f x).sinh) x
source
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) => (f x).sinh) s
source
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) => (f x).sinh) s x
source
theorem Real.hasStrictDerivAt_sin (x : ℝ) :
HasStrictDerivAt Real.sin x.cos x
source
theorem Real.hasDerivAt_sin (x : ℝ) :
HasDerivAt Real.sin x.cos x
source
theorem Real.contDiff_sin {n : ℕ∞} :
ContDiff ℝ n Real.sin
source
theorem Real.differentiable_sin :
Differentiable ℝ Real.sin
source
theorem Real.differentiableAt_sin {x : ℝ} :
DifferentiableAt ℝ Real.sin x
source
@[simp]
theorem Real.deriv_sin :
deriv Real.sin = Real.cos
source
theorem Real.hasStrictDerivAt_cos (x : ℝ) :
HasStrictDerivAt Real.cos (-x.sin) x
source
theorem Real.hasDerivAt_cos (x : ℝ) :
HasDerivAt Real.cos (-x.sin) x
source
theorem Real.contDiff_cos {n : ℕ∞} :
ContDiff ℝ n Real.cos
source
theorem Real.differentiable_cos :
Differentiable ℝ Real.cos
source
theorem Real.differentiableAt_cos {x : ℝ} :
DifferentiableAt ℝ Real.cos x
source
theorem Real.deriv_cos {x : ℝ} :
deriv Real.cos x = -x.sin
source
@[simp]
theorem Real.deriv_cos' :
deriv Real.cos = fun (x : ℝ) => -x.sin
source
theorem Real.hasStrictDerivAt_sinh (x : ℝ) :
HasStrictDerivAt Real.sinh x.cosh x
source
theorem Real.hasDerivAt_sinh (x : ℝ) :
HasDerivAt Real.sinh x.cosh x
source
theorem Real.contDiff_sinh {n : ℕ∞} :
ContDiff ℝ n Real.sinh
source
theorem Real.differentiable_sinh :
Differentiable ℝ Real.sinh
source
theorem Real.differentiableAt_sinh {x : ℝ} :
DifferentiableAt ℝ Real.sinh x
source
@[simp]
theorem Real.deriv_sinh :
deriv Real.sinh = Real.cosh
source
theorem Real.hasStrictDerivAt_cosh (x : ℝ) :
HasStrictDerivAt Real.cosh x.sinh x
source
theorem Real.hasDerivAt_cosh (x : ℝ) :
HasDerivAt Real.cosh x.sinh x
source
theorem Real.contDiff_cosh {n : ℕ∞} :
ContDiff ℝ n Real.cosh
source
theorem Real.differentiable_cosh :
Differentiable ℝ Real.cosh
source
theorem Real.differentiableAt_cosh {x : ℝ} :
DifferentiableAt ℝ Real.cosh x
source
@[simp]
theorem Real.deriv_cosh :
deriv Real.cosh = Real.sinh
source
theorem Real.sinh_strictMono :
StrictMono Real.sinh

sinh is strictly monotone.

source
theorem Real.sinh_injective :
Function.Injective Real.sinh

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

source
@[simp]
theorem Real.sinh_inj {x : ℝ} {y : ℝ} :
x.sinh = y.sinh ↔ x = y
source
@[simp]
theorem Real.sinh_le_sinh {x : ℝ} {y : ℝ} :
x.sinh ≤ y.sinh ↔ x ≤ y
source
@[simp]
theorem Real.sinh_lt_sinh {x : ℝ} {y : ℝ} :
x.sinh < y.sinh ↔ x < y
source
@[simp]
theorem Real.sinh_eq_zero {x : ℝ} :
x.sinh = 0 ↔ x = 0
source
theorem Real.sinh_ne_zero {x : ℝ} :
x.sinh ≠ 0 ↔ x ≠ 0
source
@[simp]
theorem Real.sinh_pos_iff {x : ℝ} :
0 < x.sinh ↔ 0 < x
source
@[simp]
theorem Real.sinh_nonpos_iff {x : ℝ} :
x.sinh ≤ 0 ↔ x ≤ 0
source
@[simp]
theorem Real.sinh_neg_iff {x : ℝ} :
x.sinh < 0 ↔ x < 0
source
@[simp]
theorem Real.sinh_nonneg_iff {x : ℝ} :
0 ≤ x.sinh ↔ 0 ≤ x
source
theorem Real.abs_sinh (x : ℝ) :
|x.sinh| = |x|.sinh
source
theorem Real.cosh_strictMonoOn :
StrictMonoOn Real.cosh (Set.Ici 0)
source
@[simp]
theorem Real.cosh_le_cosh {x : ℝ} {y : ℝ} :
x.cosh ≤ y.cosh ↔ |x| ≤ |y|
source
@[simp]
theorem Real.cosh_lt_cosh {x : ℝ} {y : ℝ} :
x.cosh < y.cosh ↔ |x| < |y|
source
@[simp]
theorem Real.one_le_cosh (x : ℝ) :
1 ≤ x.cosh
source
@[simp]
theorem Real.one_lt_cosh {x : ℝ} :
1 < x.cosh ↔ x ≠ 0
source
theorem Real.sinh_sub_id_strictMono :
StrictMono fun (x : ℝ) => x.sinh - x
source
@[simp]
theorem Real.self_le_sinh_iff {x : ℝ} :
x ≤ x.sinh ↔ 0 ≤ x
source
@[simp]
theorem Real.sinh_le_self_iff {x : ℝ} :
x.sinh ≤ x ↔ x ≤ 0
source
@[simp]
theorem Real.self_lt_sinh_iff {x : ℝ} :
x < x.sinh ↔ 0 < x
source
@[simp]
theorem Real.sinh_lt_self_iff {x : ℝ} :
x.sinh < x ↔ x < 0

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

Real.cos #

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

Real.sin #

source
theorem HasStrictDerivAt.sin {f : ℝ → ℝ} {f' : ℝ} {x : ℝ} (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (x : ℝ) => (f x).sin) ((f x).cos * f') x
source
theorem HasDerivAt.sin {f : ℝ → ℝ} {f' : ℝ} {x : ℝ} (hf : HasDerivAt f f' x) :
HasDerivAt (fun (x : ℝ) => (f x).sin) ((f x).cos * f') x
source
theorem HasDerivWithinAt.sin {f : ℝ → ℝ} {f' : ℝ} {x : ℝ} {s : Set ℝ} (hf : HasDerivWithinAt f f' s x) :
HasDerivWithinAt (fun (x : ℝ) => (f x).sin) ((f x).cos * f') s x
source
theorem derivWithin_sin {f : ℝ → ℝ} {x : ℝ} {s : Set ℝ} (hf : DifferentiableWithinAt ℝ f s x) (hxs : UniqueDiffWithinAt ℝ s x) :
derivWithin (fun (x : ℝ) => (f x).sin) s x = (f x).cos * derivWithin f s x
source
@[simp]
theorem deriv_sin {f : ℝ → ℝ} {x : ℝ} (hc : DifferentiableAt ℝ f x) :
deriv (fun (x : ℝ) => (f x).sin) x = (f x).cos * deriv f x

Real.cosh #

source
theorem HasStrictDerivAt.cosh {f : ℝ → ℝ} {f' : ℝ} {x : ℝ} (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (x : ℝ) => (f x).cosh) ((f x).sinh * f') x
source
theorem HasDerivAt.cosh {f : ℝ → ℝ} {f' : ℝ} {x : ℝ} (hf : HasDerivAt f f' x) :
HasDerivAt (fun (x : ℝ) => (f x).cosh) ((f x).sinh * f') x
source
theorem HasDerivWithinAt.cosh {f : ℝ → ℝ} {f' : ℝ} {x : ℝ} {s : Set ℝ} (hf : HasDerivWithinAt f f' s x) :
HasDerivWithinAt (fun (x : ℝ) => (f x).cosh) ((f x).sinh * f') s x
source
theorem derivWithin_cosh {f : ℝ → ℝ} {x : ℝ} {s : Set ℝ} (hf : DifferentiableWithinAt ℝ f s x) (hxs : UniqueDiffWithinAt ℝ s x) :
derivWithin (fun (x : ℝ) => (f x).cosh) s x = (f x).sinh * derivWithin f s x
source
@[simp]
theorem deriv_cosh {f : ℝ → ℝ} {x : ℝ} (hc : DifferentiableAt ℝ f x) :
deriv (fun (x : ℝ) => (f x).cosh) x = (f x).sinh * deriv f x

Real.sinh #

source
theorem HasStrictDerivAt.sinh {f : ℝ → ℝ} {f' : ℝ} {x : ℝ} (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (x : ℝ) => (f x).sinh) ((f x).cosh * f') x
source
theorem HasDerivAt.sinh {f : ℝ → ℝ} {f' : ℝ} {x : ℝ} (hf : HasDerivAt f f' x) :
HasDerivAt (fun (x : ℝ) => (f x).sinh) ((f x).cosh * f') x
source
theorem HasDerivWithinAt.sinh {f : ℝ → ℝ} {f' : ℝ} {x : ℝ} {s : Set ℝ} (hf : HasDerivWithinAt f f' s x) :
HasDerivWithinAt (fun (x : ℝ) => (f x).sinh) ((f x).cosh * f') s x
source
theorem derivWithin_sinh {f : ℝ → ℝ} {x : ℝ} {s : Set ℝ} (hf : DifferentiableWithinAt ℝ f s x) (hxs : UniqueDiffWithinAt ℝ s x) :
derivWithin (fun (x : ℝ) => (f x).sinh) s x = (f x).cosh * derivWithin f s x
source
@[simp]
theorem deriv_sinh {f : ℝ → ℝ} {x : ℝ} (hc : DifferentiableAt ℝ f x) :
deriv (fun (x : ℝ) => (f x).sinh) x = (f x).cosh * deriv f x

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

Real.cos #

source
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) => (f x).cos) (-(f x).sin • f') x
source
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) => (f x).cos) (-(f x).sin • f') x
source
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) => (f x).cos) (-(f x).sin • f') s x
source
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) => (f x).cos) s x
source
@[simp]
theorem DifferentiableAt.cos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hc : DifferentiableAt ℝ f x) :
DifferentiableAt ℝ (fun (x : E) => (f x).cos) x
source
theorem DifferentiableOn.cos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} (hc : DifferentiableOn ℝ f s) :
DifferentiableOn ℝ (fun (x : E) => (f x).cos) s
source
@[simp]
theorem Differentiable.cos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hc : Differentiable ℝ f) :
Differentiable ℝ fun (x : E) => (f x).cos
source
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) => (f x).cos) s x = -(f x).sin • fderivWithin ℝ f s x
source
@[simp]
theorem fderiv_cos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hc : DifferentiableAt ℝ f x) :
fderiv ℝ (fun (x : E) => (f x).cos) x = -(f x).sin • fderiv ℝ f x
source
theorem ContDiff.cos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {n : ℕ∞} (h : ContDiff ℝ n f) :
ContDiff ℝ n fun (x : E) => (f x).cos
source
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) => (f x).cos) x
source
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) => (f x).cos) s
source
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) => (f x).cos) s x

Real.sin #

source
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) => (f x).sin) ((f x).cos • f') x
source
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) => (f x).sin) ((f x).cos • f') x
source
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) => (f x).sin) ((f x).cos • f') s x
source
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) => (f x).sin) s x
source
@[simp]
theorem DifferentiableAt.sin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hc : DifferentiableAt ℝ f x) :
DifferentiableAt ℝ (fun (x : E) => (f x).sin) x
source
theorem DifferentiableOn.sin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} (hc : DifferentiableOn ℝ f s) :
DifferentiableOn ℝ (fun (x : E) => (f x).sin) s
source
@[simp]
theorem Differentiable.sin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hc : Differentiable ℝ f) :
Differentiable ℝ fun (x : E) => (f x).sin
source
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) => (f x).sin) s x = (f x).cos • fderivWithin ℝ f s x
source
@[simp]
theorem fderiv_sin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hc : DifferentiableAt ℝ f x) :
fderiv ℝ (fun (x : E) => (f x).sin) x = (f x).cos • fderiv ℝ f x
source
theorem ContDiff.sin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {n : ℕ∞} (h : ContDiff ℝ n f) :
ContDiff ℝ n fun (x : E) => (f x).sin
source
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) => (f x).sin) x
source
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) => (f x).sin) s
source
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) => (f x).sin) s x

Real.cosh #

source
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) => (f x).cosh) ((f x).sinh • f') x
source
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) => (f x).cosh) ((f x).sinh • f') x
source
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) => (f x).cosh) ((f x).sinh • f') s x
source
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) => (f x).cosh) s x
source
@[simp]
theorem DifferentiableAt.cosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hc : DifferentiableAt ℝ f x) :
DifferentiableAt ℝ (fun (x : E) => (f x).cosh) x
source
theorem DifferentiableOn.cosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} (hc : DifferentiableOn ℝ f s) :
DifferentiableOn ℝ (fun (x : E) => (f x).cosh) s
source
@[simp]
theorem Differentiable.cosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hc : Differentiable ℝ f) :
Differentiable ℝ fun (x : E) => (f x).cosh
source
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) => (f x).cosh) s x = (f x).sinh • fderivWithin ℝ f s x
source
@[simp]
theorem fderiv_cosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hc : DifferentiableAt ℝ f x) :
fderiv ℝ (fun (x : E) => (f x).cosh) x = (f x).sinh • fderiv ℝ f x
source
theorem ContDiff.cosh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {n : ℕ∞} (h : ContDiff ℝ n f) :
ContDiff ℝ n fun (x : E) => (f x).cosh
source
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) => (f x).cosh) x
source
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) => (f x).cosh) s
source
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) => (f x).cosh) s x

Real.sinh #

source
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) => (f x).sinh) ((f x).cosh • f') x
source
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) => (f x).sinh) ((f x).cosh • f') x
source
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) => (f x).sinh) ((f x).cosh • f') s x
source
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) => (f x).sinh) s x
source
@[simp]
theorem DifferentiableAt.sinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hc : DifferentiableAt ℝ f x) :
DifferentiableAt ℝ (fun (x : E) => (f x).sinh) x
source
theorem DifferentiableOn.sinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {s : Set E} (hc : DifferentiableOn ℝ f s) :
DifferentiableOn ℝ (fun (x : E) => (f x).sinh) s
source
@[simp]
theorem Differentiable.sinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hc : Differentiable ℝ f) :
Differentiable ℝ fun (x : E) => (f x).sinh
source
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) => (f x).sinh) s x = (f x).cosh • fderivWithin ℝ f s x
source
@[simp]
theorem fderiv_sinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hc : DifferentiableAt ℝ f x) :
fderiv ℝ (fun (x : E) => (f x).sinh) x = (f x).cosh • fderiv ℝ f x
source
theorem ContDiff.sinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {n : ℕ∞} (h : ContDiff ℝ n f) :
ContDiff ℝ n fun (x : E) => (f x).sinh
source
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) => (f x).sinh) x
source
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) => (f x).sinh) s
source
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) => (f x).sinh) s x
source
def Mathlib.Meta.Positivity.evalSinh :
Mathlib.Meta.Positivity.PositivityExt

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

Instances For