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}.$$

Replace sorry in the template below with your solution. See Answer Bank for acceptible answer declarations. Mathlib version used by the checker is v4.29.0.

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