Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1993P5

module

public import Mathlib.Algebra.Order.Star.Real

public section


/-!
# USA Mathematical Olympiad 1993, Problem 5

A sequence xₙ of positive reals satisfies xₙ₋₁xₙ₊₁ ≤ xₙ².
Let aₙ be the average of the terms x₀, x₁, ..., xₙ and bₙ be the average
of the terms x₁, x₂, ..., xₙ.
Show that aₙbₙ₋₁ ≥ aₙ₋₁bₙ.
-/

namespace Usa1993P5

/-- `a_avg x n` is the average of the terms `x 0, x 1, ..., x n`. -/
noncomputable def a_avg (x : ℕ → ℝ) (n : ℕ) : ℝ := (∑ i ∈ Finset.range (n + 1), x i) / (n + 1)

/-- `b_avg x n` is the average of the terms `x 1, x 2, ..., x n`. -/
noncomputable def b_avg (x : ℕ → ℝ) (n : ℕ) : ℝ := (∑ i ∈ Finset.range n, x (i + 1)) / n

theorem usa1993_p5 (x : ℕ → ℝ) (hx : ∀ n, 0 < x n)
    (h : ∀ n, x n * x (n + 2) ≤ x (n + 1) ^ 2)
    (n : ℕ) (hn : 2 ≤ n) :
    a_avg x n * b_avg x (n - 1) ≥ a_avg x (n - 1) * b_avg x n := sorry

end Usa1993P5

File author(s): Kimi K3

This problem has a complete formalized solution.