T_complex_cosh — Mathlib

English

The n-th Chebyshev polynomial of the first kind satisfies T_n(cosh θ) = cosh(n θ).

Русский

Чебышёв первый: T_n(cosh θ) = cosh(n θ).

LaTeX

$$$(T \mathbb{C} n).eval (\cosh \theta) = \cosh (n \theta)$$$

Lean4

/-- The `n`-th Chebyshev polynomial of the first kind evaluates on `cosh θ` to the
value `cosh (n * θ)`. -/
@[simp]
theorem T_complex_cosh (n : ℤ) : (T ℂ n).eval (cosh θ) = cosh (n * θ) :=
  calc
    (T ℂ n).eval (cosh θ)
    _ = (T ℂ n).eval (cos (θ * I)) := by rw [cos_mul_I]
    _ = cos (n * (θ * I)) := (T_complex_cos (θ * I) n)
    _ = cos (n * θ * I) := by rw [mul_assoc]
    _ = cosh (n * θ) := cos_mul_I (n * θ)

Похожие утверждения