Partial Sum of Squares Inequality

Let $a$ be a sequence of real numbers such that $a_1+a_2+\cdots+a_n\ge\sqrt{n}$ for any $n$. Prove that $$a_1^2+a_2^2+\cdots+a_n^2>\frac{1}{4}(1+\frac{1}{2}+\cdots+\frac{1}{n})$$ for any $n$.

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

import Mathlib.Data.Real.Sqrt

theorem solution (a : ℕ → ℝ) (ha : ∀ n ≥ 1, (∑ i ∈ Finset.Icc 1 n, a i) ≥ √n) :
    ∀ n ≥ 1, (∑ i ∈ Finset.Icc 1 n, (a i) ^ 2) >
      (1 : ℝ) / 4 * (∑ i ∈ Finset.Icc 1 n, (1 : ℝ) / i) := sorry

Submit Solution

Login to submit a solution.

Recent Submissions