Derivative of cosine
Builds on Sine and cosinePower series are differentiable inside the radius of convergence
Statement
The cosine function is differentiable on , and for all real .
Remarks
Differentiate the power series term by term. The derivative of is for .
So and . Both functions solve .
Mathlib states it as Real.hasDerivAt_cos.
Reading path
To understand this page from the ground up, read these 54 pages in order. The foundations come first.
- Limit point of a set definition
- Local maximum definition
- Sequence definition
- Limit of a function definition
- Local minimum definition
- Real sequence definition
- Subsequence definition
- Continuity at a point definition
- Derivative definition
- Bounded sequence definition
- Cauchy sequence definition
- Geometric sequence definition
- Limit of a sequence definition
- Monotone sequence definition
- Series definition
- Continuous function definition
- Fermat's theorem on stationary points statement
- Limit superior definition
- Cauchy sequences are bounded statement
- Sum of a finite geometric series statement
- Monotone convergence theorem for sequences statement
- Every sequence has a monotone subsequence statement
- Convergent sequence definition
- Pointwise convergence definition
- Squeeze theorem statement
- Partial sum definition
- Power series definition
- Bolzano–Weierstrass theorem statement
- The sequence r^n tends to zero for |r| < 1 example
- Radius of convergence definition
- Convergent series definition
- Uniform convergence definition
- Sine and cosine definition
- Boundedness theorem statement
- Cauchy criterion for sequences statement
- Uniform convergence on a set definition
- Absolute convergence definition
- A series of nonnegative terms converges iff its partial sums are bounded statement
- Series of functions definition
- Sum of a series definition
- Extreme value theorem statement
- Uniformly Cauchy sequence of functions definition
- Geometric series example
- Comparison test statement
- Rolle's theorem statement
- Root test statement
- Weierstrass M-test statement
- Mean value theorem statement
- Cauchy–Hadamard theorem statement
- Power series converge uniformly on smaller discs inside the radius of convergence statement
- Uniform convergence of derivatives allows term-by-term differentiation statement
- Term-by-term differentiation statement
- Power series are differentiable inside the radius of convergence statement
- Derivative of cosine statement
Where this leads
23 pages build on this one.
- cos pi = -1
- Inverse trigonometric functions
- Leibniz formula for pi
- Pythagorean trigonometric identity
- Derivative of arctangent
- Arcsine
- pi
- Basel problem
- Trigonometric substitution
- Derivative of arcsine
- Integral of sine
- Stirling's formula
- Sine is 2π-periodic
- Irrationality of pi
- pi is greater than 3
- Arccosine
- Power-reduction formula for cosine
- Derivative of tangent
- Power series of arctangent
- Ramanujan's series for 1/pi
- Viète's formula
- Basel problem via Fourier series
- Chudnovsky algorithm
Further reading
- Web https://en.wikipedia.org/wiki/Differentiation_of_trigonometric_functions, Derivative of the cosine function
About this page
| Tag | 0V2DV29EGT |
|---|---|
| URI | m2://0V2DV29EGT |
| Kind | statement, theorem |
| Writing | W0 stub |
| MSC | 33B10, 26A24 |
| Status | This copy of the site has no build data. Run m2 status 0V2DV29EGT. |
| Uses | Sine and cosine, Power series are differentiable inside the radius of convergence |
Markdown · JSON · Edit on GitHub
What this page needs for W1
- an inventory row: the row of the inventory that the node accounts for (0 of 1)
The writing levels say how complete the text of a page is. They do not measure its truth.