Wedge Product Inequality
Let $n \ge 2$ be an integer. Find the smallest real $c$ such that for any real numbers $a_1,a_2,...,a_n$ and $b_1,b_2,...,b_n$ satisfying $\sum_{i=1}^n{a_i}=\sum_{i=1}^n{b_i}=1$ the following holds: $$c\sum_{1\le i<j \le n}{(a_ib_j-a_jb_i)^2}\ge \sum_{i=1}^n{(a_i-b_i)^2}.$$
import Mathlib.Data.Real.Basic
import Mathlib.Data.Fintype.BigOperators
import Mathlib.Order.Interval.Finset.Nat
def answer (n : ℕ) : ℝ := sorry
def S (n : ℕ) : Set ℝ := { c | ∀ a b : ℕ → ℝ,
(∑ i ∈ Finset.Icc 1 n, a i = 1) → (∑ i ∈ Finset.Icc 1 n, b i = 1) →
(c * ∑ i ∈ Finset.Ico 1 n, ∑ j ∈ Finset.Ioc i n, (a i * b j - b i * a j) ^ 2 ≥
∑ i ∈ Finset.Icc 1 n, (a i - b i) ^ 2) }
theorem solution (n : ℕ) (hn : n ≥ 2) : IsLeast (S n) (answer n) := sorry
Submit Solution
Login to submit a solution.
Recent Submissions
| # | User | Time (UTC) | Status |
|---|---|---|---|
| 267 | Kitsune | Long time ago | PASSED |
| 266 | Kitsune | Long time ago | Compilation error |