Documentation

IMOSLLean4.Main.IMO2011.A3

IMO 2011 A3 #

Let $R$ be an integral domain of characteristic not equal to $2$. Find all pairs $(f, g)$ of functions $f, g : R → R$ such that for any $x, y ∈ R$, $$ g(f(x + y)) = f(x) + (2x + y) g(y). $$

Answer #

$(f, g) = (0, 0)$ and $(f(x), g(x)) = (x^2 + C, x)$ for some $C ∈ R$.

Solution #

We follow the official solution, but linearity of $g$ uses the proof in the comment section to avoid Ravi substitution. We still need the equations $g(f(x)) = f(-x)$ and $f(-a) = f(-b) + (a - b) g(a + b)$. Many steps of the problem generalize; we do not even require associativity on $R$.

source
def IMOSL.IMO2011A3.good {R : Type u_1} [NonUnitalNonAssocSemiring R] (f g : R → R) :
Prop

A pair of functions f, g : R → R is called good if g(f(x + y)) = f(x) + (2x + y) g(y) for any x, y : R.

Equations
Instances For
    source
    theorem IMOSL.IMO2011A3.mul_self_add_const_is_good {R : Type u_1} [NonUnitalNonAssocCommSemiring R] (C : R) :
    good (fun (x : R) => x * x + C) id

    The pair (x ↦ x^2 + C, x ↦ x) is good for any C : R.

    source
    theorem IMOSL.IMO2011A3.zero_is_good {R : Type u_1} [NonUnitalNonAssocSemiring R] :
    good (fun (x : R) => 0) fun (x : R) => 0

    The pair (0, 0) is good.

    source
    theorem IMOSL.IMO2011A3.good.gf_eq_f_neg {R : Type u_1} [NonUnitalNonAssocRing R] {f g : R → R} (h : good f g) (x : R) :
    g (f x) = f (-x)

    We have g(f(x)) = -x for any x : R.

    source
    theorem IMOSL.IMO2011A3.good.f_neg_eq_f_neg_add {R : Type u_1} [NonUnitalNonAssocRing R] {f g : R → R} (h : good f g) (a b : R) :
    f (-a) = f (-b) + (a - b) * g (a + b)

    We have f(-a) = f(-b) + (a - b) g(a + b) for any a, b : R.

    source
    theorem IMOSL.IMO2011A3.good.f_eq_x_mul_g_add_f_zero {R : Type u_1} [NonUnitalNonAssocRing R] {f g : R → R} (h : good f g) (x : R) :
    f (-x) = x * g x + f 0

    We have f(-x) = x g(x) + f(0) for any x : R.

    source
    theorem IMOSL.IMO2011A3.good.f_sub_self_mul_g_diff {R : Type u_1} [NonUnitalNonAssocRing R] {f g : R → R} (h : good f g) (x y : R) :
    f x - x * g x - (f y - y * g y) = 2 • (y * g x - x * g y)

    We have (f(x) - xg(x)) - (f(y) - yg(y)) = 2(yg(x) - xg(y)) for any x, y : R.

    source
    theorem IMOSL.IMO2011A3.good.two_nsmul_mul_g_sub_g_zero {R : Type u_1} [NonUnitalNonAssocRing R] {f g : R → R} (h : good f g) (x y : R) :
    2 • (y * (g x - g 0)) = 2 • (x * (g y - g 0))

    We have 2y(g(x) - g(0)) = 2x(g(y) - g(0)) for any x, y : R.

    source
    theorem IMOSL.IMO2011A3.good.g_right_linear {R : Type u_1} [NonAssocRing R] (hR2 : IsLeftRegular 2) {f g : R → R} (h : good f g) :
    ∃ (A : R), ∃ (B : R), ∀ (x : R), g x = x * A + B

    If 2 is not a zero divisor in R, then g is (right) linear.

    source
    theorem IMOSL.IMO2011A3.good.solve_of_NoZeroDivisors_two_ne_zero {R : Type u_1} [NonAssocRing R] [IsLeftCancelMulZero R] (hR2 : 2 ≠ 0) {f g : R → R} (h : good f g) :
    (∃ (C : R), f = fun (x : R) => x * x + C) ∧ g = id ∨ (f = fun (x : R) => 0) ∧ g = fun (x : R) => 0

    If R is a domain and 2 ≠ 0 in R, then (f, g) is either (x ↦ x^2 + C, x ↦ x) for some C : R or (0, 0).

    source
    theorem IMOSL.IMO2011A3.final_solution {R : Type u_1} [NonAssocCommRing R] [IsLeftCancelMulZero R] (hR2 : 2 ≠ 0) {f g : R → R} :
    good f g ↔ (∃ (C : R), f = fun (x : R) => x * x + C) ∧ g = id ∨ (f = fun (x : R) => 0) ∧ g = fun (x : R) => 0

    Final solution