Fan–Taussky–Todd Inequality
Given an integer $n\ge 1$, real numbers $b_0, b_1, \dots, b_{n-1}$ satisfy the conditions $\sum_{i=0}^{n-1} b_i = 0$. Prove that $\sum_{i=0}^{n-1}{b_ib_{i+1}}\le \cos\frac{2\pi}{n}\sum_{i=0}^{n-1}{b_i^2}$, where $b_n = b_0$.
import Mathlib.Data.Real.Basic
import Mathlib.Data.Fintype.BigOperators
import Mathlib.Analysis.Complex.Trigonometric
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
open Real
theorem solution (n : ℕ) (hn : n > 0) (b : ℕ → ℝ) (hb : ∑ i ∈ Finset.range n, b i = 0) (hb_round : b 0 = b n) :
∑ i ∈ Finset.range n, b i * (b (i + 1)) ≤ (cos (2 * π / n)) * ∑ i ∈ Finset.range n, (b i) ^ 2 := sorry
Submit Solution
Login to submit a solution.
Recent Submissions
None yet.