Quartic Cosine Power Reduction

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.PowerSums

Statement

Theorem Quartic Cosine Power Reduction
[blueprint]

$\cos^4 x = \dfrac{3 + 4\cos(2x) + \cos(4x)}{8}.$

theorem cos_four_formula (x : ℝ) :
    Real.cos x ^ 4 = (3 + 4 * Real.cos (2 * x) + Real.cos (4 * x)) / 8 := by
Proof ▼ 


  have h1 : Real.cos x ^ 4 = (Real.cos x ^ 2) ^ 2 := by ring
  rw [h1]
  have h2 : Real.cos x ^ 2 = (1 + Real.cos (2 * x)) / 2 := by rw [Real.cos_sq]; ring
  rw [h2]
  have h3 : ((1 + Real.cos (2 * x)) / 2) ^ 2 =
      (1 + 2 * Real.cos (2 * x) + Real.cos (2 * x) ^ 2) / 4 := by field_simp; ring
  rw [h3]
  have h4 : Real.cos (2 * x) ^ 2 = (1 + Real.cos (4 * x)) / 2 := by
    rw [Real.cos_sq]
    ring_nf
  rw [h4]
  field_simp
  ring

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