Power series expansion of elementary functions

TheoremCos (power series expansion of elementary functions)#

The power series expansion of Complex.cos.

Complex.hasSum_cos (z : ℂ) :
  HasSum (fun n => (-1) ^ n * z ^ (2 * n) / ↑(2 * n).factorial) (Complex.cos z)
Sources
MathlibComplex.hasSum_cos
Uses 7
Statement usesCos (extension of trigonometric functions to the complex plane) · Infinite sum · Metric space
Proof usesCharacteristic zero · Completeness of R · Field \(\C\) of complex numbers · Matrix exponential

TheoremSin (power series expansion of elementary functions)#

The power series expansion of Complex.sin.

Complex.hasSum_sin (z : ℂ) :
  HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1).factorial) (Complex.sin z)
Sources
MathlibComplex.hasSum_sin
Uses 7
Statement usesInfinite sum · Metric space · Sin (extension of trigonometric functions to the complex plane)
Proof usesCharacteristic zero · Completeness of R · Field \(\C\) of complex numbers · Matrix exponential

TheoremLog#

The Taylor series of the complex logarithm at 1 converges to the logarithm in the open unit disk.

Complex.hasSum_taylorSeries_log {z : ℂ} (hz : ‖z‖ < 1) :
  HasSum (fun n => (-1) ^ (n + 1) * z ^ n / ↑n) (Complex.log (1 + z))
Sources
MathlibComplex.hasSum_taylorSeries_log
Uses 11 · Used by 1
Statement usesInfinite sum · Inverse trigonometric functions · Logarithm · Metric space
Proof usesAbsolutely convergent series in Banach spaces · Characteristic p · Characteristic zero · Derivative at a point · Field \(\C\) of complex numbers · Fundamental theorem of calculus, part 2 · Heine-Borel theorem (finite-dimensional normed spaces are proper)
Used byLeibniz’s Series for Pi

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.