Cauchy-like Inequality

Prove that for any real numbers $a_1,a_2,\cdots,a_n$ and $b_1,b_2,\cdots,b_n$ satisfying $\sum_{i=1}^n{a_i^2}=\sum_{i=1}^n{b_i^2}=1$ and $\sum_{i=1}^n{a_ib_i}=0$, the following holds:
$$(\sum_{i=1}^n{a_i})^2+(\sum_{i=1}^n{b_i})^2\le n$$.

_Replace_ `sorry` _in the template below with your solution. Mathlib version used by the checker is v4.28.0_.

import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.Order.Interval.Finset.Nat

theorem solution (n : ℕ) (a b : ℕ → ℝ) (ha : ∑ i ∈ Finset.Icc 1 n, (a i) ^ 2 = 1)
    (hb : ∑ i ∈ Finset.Icc 1 n, (b i) ^ 2 = 1) (hab : ∑ i ∈ Finset.Icc 1 n, (a i) * (b i) = 0) :
    (∑ i ∈ Finset.Icc 1 n, a i) ^ 2 + (∑ i ∈ Finset.Icc 1 n, b i) ^ 2 ≤ n := sorry

Submit Solution

Login to submit a solution.

Recent Submissions