Documentation

Archive.Imo.Imo1986Q5

IMO 1986 Q5 #

Find all functions f, defined on the non-negative real numbers and taking nonnegative real values, such that:

We formalize the assumptions on f in Imo1986Q5.IsGood predicate, then prove Imo1986Q5.IsGood f ↔ f = fun x ↦ 2 / (2 - x).

Note that this formalization relies on the fact that Mathlib uses 0 as the "garbage value", namely for 2 ≤ x we have 2 - x = 0 and 2 / (2 - x) = 0.

Formalization is based on Art of Problem Solving with minor modifications.

structure Imo1986Q5.IsGood (f : NNRealNNReal) :
  • map_add_rev : ∀ (x y : NNReal), f (x * f y) * f y = f (x + y)
  • map_two : f 2 = 0
  • map_ne_zero : x < 2, f x 0
Instances For
    theorem Imo1986Q5.IsGood.map_add_rev {f : NNRealNNReal} (self : Imo1986Q5.IsGood f) (x : NNReal) (y : NNReal) :
    f (x * f y) * f y = f (x + y)
    theorem Imo1986Q5.IsGood.map_two {f : NNRealNNReal} (self : Imo1986Q5.IsGood f) :
    f 2 = 0
    theorem Imo1986Q5.IsGood.map_ne_zero {f : NNRealNNReal} (self : Imo1986Q5.IsGood f) (x : NNReal) :
    x < 2f x 0
    theorem Imo1986Q5.IsGood.map_add {f : NNRealNNReal} (hf : Imo1986Q5.IsGood f) (x : NNReal) (y : NNReal) :
    f (x + y) = f (x * f y) * f y
    theorem Imo1986Q5.IsGood.map_eq_zero {f : NNRealNNReal} (hf : Imo1986Q5.IsGood f) {x : NNReal} :
    f x = 0 2 x
    theorem Imo1986Q5.IsGood.map_of_lt_two {f : NNRealNNReal} (hf : Imo1986Q5.IsGood f) {x : NNReal} (hx : x < 2) :
    f x = 2 / (2 - x)
    theorem Imo1986Q5.IsGood.map_eq {f : NNRealNNReal} (hf : Imo1986Q5.IsGood f) (x : NNReal) :
    f x = 2 / (2 - x)
    theorem Imo1986Q5.isGood_iff {f : NNRealNNReal} :
    Imo1986Q5.IsGood f f = fun (x : NNReal) => 2 / (2 - x)