Cosine as Complex Exponential

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.ChebyshevOrthogonality

Statement

Theorem Cosine as Complex Exponential
[blueprint]

For $x \in \mathbb{R}$, $\cos(x) = \operatorname{Re}\!\left(\frac{e^{ix} + e^{-ix}}{2}\right)$. This is the standard Euler representation of cosine used to convert trigonometric power sums into complex exponential sums amenable to discrete Fourier analysis.

theorem cos_as_exp_chebyshev (x : ℝ) :
    Real.cos x = ((Complex.exp (x * Complex.I) + Complex.exp (-(x * Complex.I))) / 2).re := by
Proof ▼ 


  rw [show (Complex.exp (↑x * Complex.I) + Complex.exp (-(↑x * Complex.I))) / 2 =
    Complex.cos (x : ℂ) by
    rw [Complex.cos]
    congr 2
    congr 1
    rw [neg_mul]]
  exact Complex.cos_ofReal_re x

Dependencies (uses)

None

Dependents (used by)

Neighborhood

Legend
Not Ready
Work in Progress
Sorry (theorems only)
Proven/Defined
Fully Proven (theorems only)
Axiom
Mathlib Ready
Theorems/Lemmas
Definitions
Axioms