Quintic Cosine Power Reduction

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.PowerSums

Statement

Theorem Quintic Cosine Power Reduction
[blueprint]

$\cos^5 x = \dfrac{\cos(5x) + 5\cos(3x) + 10\cos x}{16}.$

theorem cos_five_formula (x : ℝ) :
    Real.cos x ^ 5 = (Real.cos (5 * x) + 5 * Real.cos (3 * x) + 10 * Real.cos x) / 16 := by
Proof ▼ 


  have h_five : Real.cos (5 * x) =
      16 * Real.cos x ^ 5 - 20 * Real.cos x ^ 3 + 5 * Real.cos x := cos_five_mul x
  have h_cube : Real.cos x ^ 3 = (Real.cos (3 * x) + 3 * Real.cos x) / 4 :=
      cos_cube_formula x
  rw [h_cube] at h_five
  have h_simplified :
      Real.cos (5 * x) = 16 * Real.cos x ^ 5 - 5 * Real.cos (3 * x) - 10 * Real.cos x := by
    calc Real.cos (5 * x)
        = 16 * Real.cos x ^ 5 - 20 * ((Real.cos (3 * x) + 3 * Real.cos x) / 4) +
          5 * Real.cos x := h_five
      _ = 16 * Real.cos x ^ 5 - 5 * (Real.cos (3 * x) + 3 * Real.cos x) +
          5 * Real.cos x := by ring
      _ = 16 * Real.cos x ^ 5 - 5 * Real.cos (3 * x) - 10 * Real.cos x := by ring
  linarith [h_simplified]

Dependencies (uses)

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