Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2017P6

import Mathlib.Algebra.BigOperators.Field
import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Data.Real.Basic
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring

/-!
# USA Mathematical Olympiad 2017, Problem 6

Find the minimum possible value of
`a / (b³ + 4) + b / (c³ + 4) + c / (d³ + 4) + d / (a³ + 4)`
given that `a, b, c, d` are nonnegative real numbers such that `a + b + c + d = 4`.
-/

namespace Usa2017P6

noncomputable def f (x : Fin 4 → ℝ) : ℝ :=
  ∑ i, x i / (x (i + 1) ^ 3 + 4)

def Conditions (x : Fin 4 → ℝ) : Prop :=
  0 ≤ x ∧ ∑ i, x i = 4

noncomputable /- determine -/ abbrev solution : ℝ := sorry

theorem usa2017_p6 : IsLeast (f '' {x | Conditions x}) solution := sorry

end Usa2017P6

File author(s): Jeremy Tan

This problem has a complete formalized solution.