We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 0618bff commit 30831dbCopy full SHA for 30831db
1 file changed
Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/ChebyshevGauss.lean
@@ -63,7 +63,8 @@ private theorem sum_exp {n : ℕ} {k : ℤ} (hn : n ≠ 0) (hk : ¬ (2 * n : ℤ
63
show (n * (k / n * π * I)) = k * (π * I) by field [show (n : ℂ) ≠ 0 by aesop],
64
Complex.exp_int_mul, Complex.exp_pi_mul_I]
65
66
-/-- Weighted sum of `P (x)` where `x` goes over `cos ((2 * i + 1) / (2 * n) * π)` for `0 ≤ i < n`. -/
+/-- Weighted sum of `P (x)` where `x` goes over `cos ((2 * i + 1) / (2 * n) * π)` for
67
+ `0 ≤ i < n`. -/
68
noncomputable def sumZeroes (n : ℕ) (P : ℝ[X]) : ℝ :=
69
(π / n) * ∑ i ∈ range n, P.eval (cos ((2 * i + 1) / (2 * n) * π))
70
0 commit comments