Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1977P5

module

public import Mathlib.Algebra.BigOperators.Fin
public import Mathlib.Algebra.Order.Star.Real
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Tactic.FieldSimp
public import Mathlib.Tactic.FinCases
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 1977, Problem 5

The positive reals v, w, x, y, z satisfy 0 < h ≤ v, w, x, y, z ≤ k.
Show that

  (v + w + x + y + z)(1/v + 1/w + 1/x + 1/y + 1/z) ≤ 25 + 6(√(h/k) - √(k/h))².

When do we have equality?
-/

namespace Usa1977P5

theorem usa1977_p5
    (h k v w x y z : ℝ)
    (hh : 0 < h)
    (hv : h ≤ v ∧ v ≤ k) (hw : h ≤ w ∧ w ≤ k) (hx : h ≤ x ∧ x ≤ k)
    (hy : h ≤ y ∧ y ≤ k) (hz : h ≤ z ∧ z ≤ k) :
    (v + w + x + y + z) * (1 / v + 1 / w + 1 / x + 1 / y + 1 / z) ≤
      25 + 6 * (√(h / k) - √(k / h)) ^ 2 := sorry

end Usa1977P5

File author(s): Kimi K3

This problem has a complete formalized solution.