U_complex_cosh — Mathlib

English

The n-th Chebyshev polynomial of the second kind satisfies U_n(cosh θ) sinh θ = sinh((n+1) θ).

Русский

Умножение: U_n(cosh θ) sinh θ = sinh((n+1) θ).

LaTeX

$$(U \mathbb{C} n).eval (\cosh θ) \cdot \sinh θ = \sinh ((n + 1) \theta)$$

Lean4

/-- The `n`-th Chebyshev polynomial of the second kind evaluates on `cosh θ` to the
value `sinh ((n + 1) * θ) / sinh θ`. -/
@[simp]
theorem U_complex_cosh (n : ℤ) : (U ℂ n).eval (cosh θ) * sinh θ = sinh ((n + 1) * θ) :=
  calc
    (U ℂ n).eval (cosh θ) * sinh θ
    _ = (U ℂ n).eval (cos (θ * I)) * sin (θ * I) * (-I) := by simp [cos_mul_I, sin_mul_I, mul_assoc]
    _ = sin ((n + 1) * (θ * I)) * (-I) := by rw [U_complex_cos]
    _ = sin ((n + 1) * θ * I) * (-I) := by rw [mul_assoc]
    _ = sinh ((n + 1) * θ) := by rw [sin_mul_I ((n + 1) * θ), mul_assoc, mul_neg, I_mul_I, neg_neg, mul_one]

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