Documentation

Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Differentiability of hyperbolic trigonometric functions #

Main statements #

The differentiability of the hyperbolic trigonometric functions is proved, and their derivatives are computed.

Tags #

sinh, cosh, tanh

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

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

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

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

source
theorem Complex.isEquivalent_sinh :
Asymptotics.IsEquivalent (nhds 0) sinh id
source
theorem Complex.contDiff_sinh {n : WithTop ℕ∞} :
ContDiff ℂ n sinh
source
@[simp]
theorem Complex.differentiable_sinh :
Differentiable ℂ sinh
source
@[simp]
theorem Complex.differentiableAt_sinh {x : ℂ} :
DifferentiableAt ℂ sinh x
source
theorem Complex.analyticAt_sinh {x : ℂ} :
AnalyticAt ℂ sinh x

The function Complex.sinh is complex analytic.

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

The function Complex.sinh is complex analytic.

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

The function Complex.sinh is complex analytic.

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

The function Complex.sinh is complex analytic.

source
@[simp]
theorem Complex.deriv_sinh :
deriv sinh = cosh
source
theorem Complex.hasStrictDerivAt_cosh (x : ℂ) :
HasStrictDerivAt cosh (sinh x) x

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

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

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

source
theorem Complex.contDiff_cosh {n : WithTop ℕ∞} :
ContDiff ℂ n cosh
source
@[simp]
theorem Complex.differentiable_cosh :
Differentiable ℂ cosh
source
@[simp]
theorem Complex.differentiableAt_cosh {x : ℂ} :
DifferentiableAt ℂ cosh x
source
theorem Complex.analyticAt_cosh {x : ℂ} :
AnalyticAt ℂ cosh x

The function Complex.cosh is complex analytic.

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

The function Complex.cosh is complex analytic.

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

The function Complex.cosh is complex analytic.

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

The function Complex.cosh is complex analytic.

source
@[simp]
theorem Complex.deriv_cosh :
deriv cosh = sinh

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

Complex.cosh #

source
theorem HasStrictDerivAt.ccosh {f : ℂ → ℂ} {f' x : ℂ} (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (x : ℂ) => Complex.cosh (f x)) (Complex.sinh (f x) * f') x
source
theorem HasDerivAt.ccosh {f : ℂ → ℂ} {f' x : ℂ} (hf : HasDerivAt f f' x) :
HasDerivAt (fun (x : ℂ) => Complex.cosh (f x)) (Complex.sinh (f x) * f') x
source
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
source
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
source
@[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 #

source
theorem HasStrictDerivAt.csinh {f : ℂ → ℂ} {f' x : ℂ} (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (x : ℂ) => Complex.sinh (f x)) (Complex.cosh (f x) * f') x
source
theorem HasDerivAt.csinh {f : ℂ → ℂ} {f' x : ℂ} (hf : HasDerivAt f f' x) :
HasDerivAt (fun (x : ℂ) => Complex.sinh (f x)) (Complex.cosh (f x) * f') x
source
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
source
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
source
@[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.cosh #

source
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
source
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
source
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
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) => Complex.cosh (f x)) 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) => Complex.cosh (f x)) 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) => Complex.cosh (f x)) s
source
@[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)
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) => Complex.cosh (f x)) s x = Complex.sinh (f x) • 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) => Complex.cosh (f x)) x = Complex.sinh (f x) • fderiv ℂ f x
source
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)
source
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
source
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
source
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 #

source
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
source
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
source
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
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) => Complex.sinh (f x)) 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) => Complex.sinh (f x)) 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) => Complex.sinh (f x)) s
source
@[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)
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) => Complex.sinh (f x)) s x = Complex.cosh (f x) • 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) => Complex.sinh (f x)) x = Complex.cosh (f x) • fderiv ℂ f x
source
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)
source
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
source
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
source
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
source
theorem Real.hasStrictDerivAt_sinh (x : ℝ) :
HasStrictDerivAt sinh (cosh x) x
source
theorem Real.hasDerivAt_sinh (x : ℝ) :
HasDerivAt sinh (cosh x) x
source
theorem Real.isEquivalent_sinh :
Asymptotics.IsEquivalent (nhds 0) sinh id
source
theorem Real.contDiff_sinh {n : WithTop ℕ∞} :
ContDiff ℝ n sinh
source
@[simp]
theorem Real.differentiable_sinh :
Differentiable ℝ sinh
source
@[simp]
theorem Real.differentiableAt_sinh {x : ℝ} :
DifferentiableAt ℝ sinh x
source
theorem Real.analyticAt_sinh {x : ℝ} :
AnalyticAt ℝ sinh x

The function Real.sinh is real analytic.

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

The function Real.sinh is real analytic.

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

The function Real.sinh is real analytic.

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

The function Real.sinh is real analytic.

source
@[simp]
theorem Real.deriv_sinh :
deriv sinh = cosh
source
theorem Real.hasStrictDerivAt_cosh (x : ℝ) :
HasStrictDerivAt cosh (sinh x) x
source
theorem Real.hasDerivAt_cosh (x : ℝ) :
HasDerivAt cosh (sinh x) x
source
theorem Real.contDiff_cosh {n : WithTop ℕ∞} :
ContDiff ℝ n cosh
source
@[simp]
theorem Real.differentiable_cosh :
Differentiable ℝ cosh
source
@[simp]
theorem Real.differentiableAt_cosh {x : ℝ} :
DifferentiableAt ℝ cosh x
source
theorem Real.analyticAt_cosh {x : ℝ} :
AnalyticAt ℝ cosh x

The function Real.cosh is real analytic.

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

The function Real.cosh is real analytic.

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

The function Real.cosh is real analytic.

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

The function Real.cosh is real analytic.

source
@[simp]
theorem Real.deriv_cosh :
deriv cosh = sinh
source
theorem Real.sinh_strictMono :
StrictMono sinh

sinh is strictly monotone.

source
theorem Real.sinh_injective :
Function.Injective sinh

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

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

Simp lemmas for iterated derivatives of sinh and cosh. #

source
@[simp]
theorem Complex.iteratedDeriv_add_one_sinh (n : ℕ) :
iteratedDeriv (n + 1) sinh = iteratedDeriv n cosh
source
@[simp]
theorem Complex.iteratedDeriv_add_one_cosh (n : ℕ) :
iteratedDeriv (n + 1) cosh = iteratedDeriv n sinh
source
@[simp]
theorem Complex.iteratedDeriv_even_sinh (n : ℕ) :
iteratedDeriv (2 * n) sinh = sinh
source
@[simp]
theorem Complex.iteratedDeriv_even_cosh (n : ℕ) :
iteratedDeriv (2 * n) cosh = cosh
source
theorem Complex.iteratedDeriv_odd_sinh (n : ℕ) :
iteratedDeriv (2 * n + 1) sinh = cosh
source
theorem Complex.iteratedDeriv_odd_cosh (n : ℕ) :
iteratedDeriv (2 * n + 1) cosh = sinh
source
theorem Complex.differentiable_iteratedDeriv_sinh (n : ℕ) :
Differentiable ℂ (iteratedDeriv n sinh)
source
theorem Complex.differentiable_iteratedDeriv_cosh (n : ℕ) :
Differentiable ℂ (iteratedDeriv n cosh)
source
@[simp]
theorem Real.iteratedDeriv_add_one_sinh (n : ℕ) :
iteratedDeriv (n + 1) sinh = iteratedDeriv n cosh
source
@[simp]
theorem Real.iteratedDeriv_add_one_cosh (n : ℕ) :
iteratedDeriv (n + 1) cosh = iteratedDeriv n sinh
source
@[simp]
theorem Real.iteratedDeriv_even_sinh (n : ℕ) :
iteratedDeriv (2 * n) sinh = sinh
source
@[simp]
theorem Real.iteratedDeriv_even_cosh (n : ℕ) :
iteratedDeriv (2 * n) cosh = cosh
source
theorem Real.iteratedDeriv_odd_sinh (n : ℕ) :
iteratedDeriv (2 * n + 1) sinh = cosh
source
theorem Real.iteratedDeriv_odd_cosh (n : ℕ) :
iteratedDeriv (2 * n + 1) cosh = sinh
source
theorem Real.differentiable_iteratedDeriv_sinh (n : ℕ) :
Differentiable ℝ (iteratedDeriv n sinh)
source
theorem Real.differentiable_iteratedDeriv_cosh (n : ℕ) :
Differentiable ℝ (iteratedDeriv n cosh)
source
@[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
source
@[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
source
@[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
source
@[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.cosh #

source
theorem HasStrictDerivAt.cosh {f : ℝ → ℝ} {f' x : ℝ} (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (x : ℝ) => Real.cosh (f x)) (Real.sinh (f x) * f') x
source
theorem HasDerivAt.cosh {f : ℝ → ℝ} {f' x : ℝ} (hf : HasDerivAt f f' x) :
HasDerivAt (fun (x : ℝ) => Real.cosh (f x)) (Real.sinh (f x) * f') x
source
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
source
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
source
@[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 #

source
theorem HasStrictDerivAt.sinh {f : ℝ → ℝ} {f' x : ℝ} (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (x : ℝ) => Real.sinh (f x)) (Real.cosh (f x) * f') x
source
theorem HasDerivAt.sinh {f : ℝ → ℝ} {f' x : ℝ} (hf : HasDerivAt f f' x) :
HasDerivAt (fun (x : ℝ) => Real.sinh (f x)) (Real.cosh (f x) * f') x
source
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
source
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
source
@[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.cosh #

source
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
source
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
source
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
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) => Real.cosh (f x)) 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) => Real.cosh (f x)) 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) => Real.cosh (f x)) s
source
@[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)
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) => Real.cosh (f x)) s x = Real.sinh (f x) • 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) => Real.cosh (f x)) x = Real.sinh (f x) • fderiv ℝ f x
source
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)
source
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
source
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
source
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 #

source
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
source
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
source
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
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) => Real.sinh (f x)) 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) => Real.sinh (f x)) 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) => Real.sinh (f x)) s
source
@[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)
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) => Real.sinh (f x)) s x = Real.cosh (f x) • 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) => Real.sinh (f x)) x = Real.cosh (f x) • fderiv ℝ f x
source
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)
source
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
source
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
source
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
source
@[simp]
theorem Complex.logDeriv_cosh :
logDeriv cosh = tanh
source
@[simp]
theorem Real.logDeriv_cosh :
logDeriv cosh = tanh
source
theorem Mathlib.Meta.Positivity.sinh_pos_of_pos {x : ℝ} :
0 < x → 0 < Real.sinh x

Alias of the reverse direction of Real.sinh_pos_iff.

source
theorem Mathlib.Meta.Positivity.sinh_nonneg_of_nonneg {x : ℝ} :
0 ≤ x → 0 ≤ Real.sinh x

Alias of the reverse direction of Real.sinh_nonneg_iff.

source
theorem Mathlib.Meta.Positivity.sinh_ne_zero_of_ne_zero {x : ℝ} :
x ≠ 0 → Real.sinh x ≠ 0

Alias of the reverse direction of Real.sinh_ne_zero.

source
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.
Instances For