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 sin (cos x) x

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

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

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

source
theorem Complex.isEquivalent_sin :
Asymptotics.IsEquivalent (nhds 0) sin id
source
theorem Complex.contDiff_sin {n : WithTop ℕ∞} :
ContDiff ℂ n sin
source
@[simp]
theorem Complex.differentiable_sin :
Differentiable ℂ sin
source
@[simp]
theorem Complex.differentiableAt_sin {x : ℂ} :
DifferentiableAt ℂ sin x
source
theorem Complex.analyticAt_sin {x : ℂ} :
AnalyticAt ℂ sin x

The function Complex.sin is complex analytic.

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

The function Complex.sin is complex analytic.

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

The function Complex.sin is complex analytic.

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

The function Complex.sin is complex analytic.

source
@[simp]
theorem Complex.deriv_sin :
deriv sin = cos
source
theorem Complex.hasStrictDerivAt_cos (x : ℂ) :
HasStrictDerivAt cos (-sin x) x

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

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

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

source
theorem Complex.contDiff_cos {n : WithTop ℕ∞} :
ContDiff ℂ n cos
source
@[simp]
theorem Complex.differentiable_cos :
Differentiable ℂ cos
source
@[simp]
theorem Complex.differentiableAt_cos {x : ℂ} :
DifferentiableAt ℂ cos x
source
theorem Complex.analyticAt_cos {x : ℂ} :
AnalyticAt ℂ cos x

The function Complex.cos is complex analytic.

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

The function Complex.cos is complex analytic.

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

The function Complex.cos is complex analytic.

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

The function Complex.cos is complex analytic.

source
theorem Complex.deriv_cos {x : ℂ} :
deriv cos x = -sin x
source
@[simp]
theorem Complex.deriv_cos' :
deriv cos = fun (x : ℂ) => -sin x

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

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

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' : StrongDual ℂ E} {x : E} (hf : HasStrictFDerivAt f f' x) :
HasStrictFDerivAt (fun (x : E) => Complex.cos (f x)) (-Complex.sin (f x) • f') x
source
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
source
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
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) => Complex.cos (f x)) 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) => Complex.cos (f x)) 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) => Complex.cos (f x)) s
source
@[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)
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) => Complex.cos (f x)) s x = -Complex.sin (f x) • 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) => Complex.cos (f x)) x = -Complex.sin (f x) • fderiv ℂ f x
source
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)
source
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
source
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
source
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 #

source
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
source
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
source
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
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) => Complex.sin (f x)) 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) => Complex.sin (f x)) 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) => Complex.sin (f x)) s
source
@[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)
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) => Complex.sin (f x)) s x = Complex.cos (f x) • 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) => Complex.sin (f x)) x = Complex.cos (f x) • fderiv ℂ f x
source
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)
source
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
source
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
source
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
source
theorem Real.hasStrictDerivAt_sin (x : ℝ) :
HasStrictDerivAt sin (cos x) x
source
theorem Real.hasDerivAt_sin (x : ℝ) :
HasDerivAt sin (cos x) x
source
theorem Real.isEquivalent_sin :
Asymptotics.IsEquivalent (nhds 0) sin id
source
theorem Real.contDiff_sin {n : WithTop ℕ∞} :
ContDiff ℝ n sin
source
@[simp]
theorem Real.differentiable_sin :
Differentiable ℝ sin
source
@[simp]
theorem Real.differentiableAt_sin {x : ℝ} :
DifferentiableAt ℝ sin x
source
theorem Real.analyticAt_sin {x : ℝ} :
AnalyticAt ℝ sin x

The function Real.sin is real analytic.

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

The function Real.sin is real analytic.

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

The function Real.sin is real analytic.

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

The function Real.sin is real analytic.

source
@[simp]
theorem Real.deriv_sin :
deriv sin = cos
source
theorem Real.hasStrictDerivAt_cos (x : ℝ) :
HasStrictDerivAt cos (-sin x) x
source
theorem Real.hasDerivAt_cos (x : ℝ) :
HasDerivAt cos (-sin x) x
source
theorem Real.contDiff_cos {n : WithTop ℕ∞} :
ContDiff ℝ n cos
source
@[simp]
theorem Real.differentiable_cos :
Differentiable ℝ cos
source
@[simp]
theorem Real.differentiableAt_cos {x : ℝ} :
DifferentiableAt ℝ cos x
source
theorem Real.analyticAt_cos {x : ℝ} :
AnalyticAt ℝ cos x

The function Real.cos is real analytic.

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

The function Real.cos is real analytic.

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

The function Real.cos is real analytic.

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

The function Real.cos is real analytic.

source
theorem Real.deriv_cos {x : ℝ} :
deriv cos x = -sin x
source
@[simp]
theorem Real.deriv_cos' :
deriv cos = fun (x : ℝ) => -sin x

Simp lemmas for iterated derivatives of sin and cos. #

source
@[simp]
theorem Complex.iteratedDeriv_add_one_sin (n : ℕ) :
iteratedDeriv (n + 1) sin = iteratedDeriv n cos
source
@[simp]
theorem Complex.iteratedDeriv_add_one_cos (n : ℕ) :
iteratedDeriv (n + 1) cos = -iteratedDeriv n sin
source
@[simp]
theorem Complex.iteratedDeriv_even_sin (n : ℕ) :
iteratedDeriv (2 * n) sin = (-1) ^ n * sin
source
@[simp]
theorem Complex.iteratedDeriv_even_cos (n : ℕ) :
iteratedDeriv (2 * n) cos = (-1) ^ n * cos
source
theorem Complex.iteratedDeriv_odd_sin (n : ℕ) :
iteratedDeriv (2 * n + 1) sin = (-1) ^ n * cos
source
theorem Complex.iteratedDeriv_odd_cos (n : ℕ) :
iteratedDeriv (2 * n + 1) cos = (-1) ^ (n + 1) * sin
source
theorem Complex.differentiable_iteratedDeriv_sin (n : ℕ) :
Differentiable ℂ (iteratedDeriv n sin)
source
theorem Complex.differentiable_iteratedDeriv_cos (n : ℕ) :
Differentiable ℂ (iteratedDeriv n cos)
source
@[simp]
theorem Real.iteratedDeriv_add_one_sin (n : ℕ) :
iteratedDeriv (n + 1) sin = iteratedDeriv n cos
source
@[simp]
theorem Real.iteratedDeriv_add_one_cos (n : ℕ) :
iteratedDeriv (n + 1) cos = -iteratedDeriv n sin
source
@[simp]
theorem Real.iteratedDeriv_even_sin (n : ℕ) :
iteratedDeriv (2 * n) sin = (-1) ^ n * sin
source
@[simp]
theorem Real.iteratedDeriv_even_cos (n : ℕ) :
iteratedDeriv (2 * n) cos = (-1) ^ n * cos
source
theorem Real.iteratedDeriv_odd_sin (n : ℕ) :
iteratedDeriv (2 * n + 1) sin = (-1) ^ n * cos
source
theorem Real.iteratedDeriv_odd_cos (n : ℕ) :
iteratedDeriv (2 * n + 1) cos = (-1) ^ (n + 1) * sin
source
theorem Real.differentiable_iteratedDeriv_sin (n : ℕ) :
Differentiable ℝ (iteratedDeriv n sin)
source
theorem Real.differentiable_iteratedDeriv_cos (n : ℕ) :
Differentiable ℝ (iteratedDeriv n cos)
source
theorem Real.abs_iteratedDeriv_sin_le_one (n : ℕ) (x : ℝ) :
|iteratedDeriv n sin x| ≤ 1
source
theorem Real.abs_iteratedDeriv_cos_le_one (n : ℕ) (x : ℝ) :
|iteratedDeriv n cos x| ≤ 1
source
@[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
source
@[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
source
@[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
source
@[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 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 : ℝ) => Real.cos (f x)) (-Real.sin (f x) * f') x
source
theorem HasDerivAt.cos {f : ℝ → ℝ} {f' x : ℝ} (hf : HasDerivAt f f' x) :
HasDerivAt (fun (x : ℝ) => Real.cos (f x)) (-Real.sin (f x) * f') x
source
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
source
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
source
@[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 #

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

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' : StrongDual ℝ E} {x : E} (hf : HasStrictFDerivAt f f' x) :
HasStrictFDerivAt (fun (x : E) => Real.cos (f x)) (-Real.sin (f x) • f') x
source
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
source
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
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) => Real.cos (f x)) 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) => Real.cos (f x)) 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) => Real.cos (f x)) s
source
@[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)
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) => Real.cos (f x)) s x = -Real.sin (f x) • 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) => Real.cos (f x)) x = -Real.sin (f x) • fderiv ℝ f x
source
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)
source
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
source
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
source
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 #

source
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
source
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
source
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
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) => Real.sin (f x)) 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) => Real.sin (f x)) 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) => Real.sin (f x)) s
source
@[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)
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) => Real.sin (f x)) s x = Real.cos (f x) • 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) => Real.sin (f x)) x = Real.cos (f x) • fderiv ℝ f x
source
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)
source
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
source
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
source
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
source
@[simp]
theorem Complex.logDeriv_sin :
logDeriv sin = cot
source
@[simp]
theorem Real.logDeriv_sin :
logDeriv sin = cot
source
@[simp]
theorem Complex.logDeriv_cos :
logDeriv cos = -tan
source
@[simp]
theorem Real.logDeriv_cos :
logDeriv cos = -tan
source
@[simp]
theorem Complex.LogDeriv_exp :
logDeriv exp = 1
source
@[simp]
theorem Real.LogDeriv_exp :
logDeriv exp = 1