Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2016P4

module

public import Mathlib.Tactic
import Mathlib.Analysis.SpecialFunctions.Log.Base

public section


/-!
# USA Mathematical Olympiad 2016 P4
Find all functions f : ℝ → ℝ such that for all x, y ∈ ℝ:
(f(x)+xy) · f(x-3y) + (f(y)+xy) · f(3x-y) = (f(x+y))^2

-/

namespace Usa2016P4
def f_good (f : ℝ → ℝ) : Prop :=  ∀ x y, (f x + x*y) * f (x - 3*y) + (f y + x * y) * f (3*x - y) = (f (x+y))^2

/- determine -/ abbrev solution_set : Set (ℝ → ℝ) := sorry

theorem usa2016_p4 (f : ℝ → ℝ) : f ∈ solution_set ↔ f_good f := sorry

end Usa2016P4

File author(s): Pacmanboss256

This problem has a complete formalized solution.