Lean Online Judge

Bulgaria TST 2009 Problem ?

Let $a, b, c$ be sequences of real numbers with positive partial sums. Show that $$(\sum_{i = 1}^{n} \sum_{j = 1}^{n} \frac{a_i a_j}{c_i + c_j})(\sum_{i = 1}^{n} \sum_{j = 1}^{n} \frac{b_i b_j}{c_i + c_j}) \ge (\sum_{i = 1}^{n} \sum_{j = 1}^{n} \frac{a_i b_j}{c_i + c_j})^2.$$

Replace sorry in the template below with your solution. The Mathlib version currently used is v4.26.0.

import Mathlib.Data.Fintype.BigOperators
import Mathlib.Data.Real.Basic
import Mathlib.Order.Interval.Finset.Nat
import Mathlib.Data.Finset.Basic

theorem solution (a b c : ℕ → ℝ) (n : ℕ) (hn : n ≥ 1) (ha : ∀ i ∈ Finset.Icc 1 n, a i > 0)
    (hb : ∀ i ∈ Finset.Icc 1 n, b i > 0) (hc : ∀ i ∈ Finset.Icc 1 n, c i > 0) :
    (∑ i ∈ Finset.Icc 1 n, ∑ j ∈ Finset.Icc 1 n, a i * a j / (c i + c j)) *
    (∑ i ∈ Finset.Icc 1 n, ∑ j ∈ Finset.Icc 1 n, b i * b j / (c i + c j)) ≥
    (∑ i ∈ Finset.Icc 1 n, ∑ j ∈ Finset.Icc 1 n, a i * b j / (c i  +c j)) ^ 2 := sorry