Polynomial.Chebyshev.U_real_cos
theorem Polynomial.Chebyshev.U_real_cos :
∀ (θ : ℝ) (n : ℕ), Polynomial.eval θ.cos (Polynomial.Chebyshev.U ℝ n) * θ.sin = ((↑n + 1) * θ).sin
The theorem `Polynomial.Chebyshev.U_real_cos` states that for any real number `θ` and any natural number `n`, the evaluation of the `n`-th Chebyshev polynomial of the second kind at `cos θ` times `sin θ` equals to the sine of `(n + 1) * θ`. In mathematical terms, this would be expressed as: $\sin((n + 1)\theta) = \text{Polynomial.Chebyshev.U}(\cos \theta) \cdot \sin \theta$. This theorem establishes a mathematical relationship between the Chebyshev polynomials and trigonometric functions.
More concisely: The `n`-th Chebyshev polynomial of the second kind evaluated at the product of cosine and sine of a real number `θ` is equal to the sine of `(n + 1) * θ`. In Lean 4, this is expressed as `Polynomial.Chebyshev.U (cos θ) * sin θ = sin ((n + 1) * θ)` for any natural number `n`.
|
Polynomial.Chebyshev.U_complex_cos
theorem Polynomial.Chebyshev.U_complex_cos :
∀ (θ : ℂ) (n : ℕ), Polynomial.eval θ.cos (Polynomial.Chebyshev.U ℂ n) * θ.sin = ((↑n + 1) * θ).sin
The theorem `Polynomial.Chebyshev.U_complex_cos` states that for all complex numbers `θ` and natural numbers `n`, the evaluation of the `n`-th Chebyshev polynomial of the second kind at `cos θ`, multiplied by `sin θ`, equals the sine of `((n + 1) * θ)`. In mathematical terms, if $U_n$ is the `n`-th Chebyshev polynomial of the second kind, this statement can be written as $U_n(\cos(\theta)) \cdot \sin(\theta) = \sin((n + 1) \cdot \theta)$.
More concisely: For all complex numbers θ and natural numbers n, $U\_n(\cos \theta) \cdot \sin \theta = \sin ((n + 1) \cdot \theta)$, where $U\_n$ is the n-th Chebyshev polynomial of the second kind.
|
Polynomial.Chebyshev.T_complex_cos
theorem Polynomial.Chebyshev.T_complex_cos :
∀ (θ : ℂ) (n : ℕ), Polynomial.eval θ.cos (Polynomial.Chebyshev.T ℂ n) = (↑n * θ).cos
The theorem `Polynomial.Chebyshev.T_complex_cos` states that for all complex numbers `θ` and for all natural numbers `n`, the evaluation of the `n`-th Chebyshev polynomial of the first kind at the cosine of `θ` is equal to the cosine of `n * θ`. In other words, if you substitute `cos θ` into the `n`-th Chebyshev polynomial, you will obtain `cos (n * θ)`.
More concisely: For all complex numbers θ and natural numbers n, T\_n(cos θ) = cos(n * θ), where T\_n is the n-th Chebyshev polynomial of the first kind.
|
Polynomial.Chebyshev.T_real_cos
theorem Polynomial.Chebyshev.T_real_cos :
∀ (θ : ℝ) (n : ℕ), Polynomial.eval θ.cos (Polynomial.Chebyshev.T ℝ n) = (↑n * θ).cos
The theorem `Polynomial.Chebyshev.T_real_cos` states that for all real numbers `θ` and for all natural numbers `n`, evaluating the `n`-th Chebyshev polynomial of the first kind at `cos(θ)` returns the value `cos(n*θ)`. In other words, the cosine of `n` times an angle is equal to the value of the `n`-th Chebyshev polynomial evaluated at the cosine of the angle.
More concisely: For all real numbers θ and natural numbers n, T\_n(cos(θ)) = cos(nθ), where T\_n is the n-th Chebyshev polynomial of the first kind.
|