Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1994P4

module

public import Mathlib.Algebra.BigOperators.Field
public import Mathlib.Algebra.BigOperators.Module
public import Mathlib.Algebra.CharP.Defs
public import Mathlib.Algebra.Order.Star.Real

public section


/-!
# USA Mathematical Olympiad 1994, Problem 4

xᵢ is an infinite sequence of positive reals such that for all n,
x₁ + x₂ + ... + xₙ ≥ √n. Show that
x₁² + x₂² + ... + xₙ² > (1 + 1/2 + 1/3 + ... + 1/n) / 4 for all n.
-/

namespace Usa1994P4

theorem usa1994_p4 (x : ℕ → ℝ) (hx : ∀ i, 0 < x i)
    (h : ∀ n : ℕ, Real.sqrt (n : ℝ) ≤ ∑ i ∈ Finset.range n, x i)
    (n : ℕ) (hn : 1 ≤ n) :
    (∑ i ∈ Finset.range n, (1 : ℝ) / (i + 1)) / 4 < ∑ i ∈ Finset.range n, (x i) ^ 2 := sorry

end Usa1994P4

File author(s): Kimi K3

This problem has a complete formalized solution.