Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2017P6

module

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

public section


/-!
# 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.