Cubic Cosine Power Reduction

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.TrigonometricIdentities

Statement

Theorem Cubic Cosine Power Reduction
[blueprint]

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

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

Immediate from the triple-angle formula $\cos(3x) = 4\cos^3 x - 3\cos x$.


  linarith [Real.cos_three_mul 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