Documentation

Archive.Imo.Imo2024Q6

IMO 2024 Q6 #

A function f: ℚ → ℚ is called aquaesulian if the following property holds: for every x, y ∈ ℚ, f(x + f(y)) = f(x) + y or f(f(x) + y) = x + f(y).

Show that there exists an integer c such that for any aquaesulian function f there are at most c different rational numbers of the form f(r)+f(-r) for some rational number r, and find the smallest possible value of c.

We follow Solution 1 from the official solutions. A key observation is that f(-f(-x)) = x. We then consider a pair of distinct nonzero values of f(x)+f(-x), and a series of manipulations together with the previous observation result in a contradiction, so there are at most two values of f(x)+f(-x). All this works over any AddCommGroup; over , we then show that ⌊x⌋ - Int.fract x achieves two different values of f(x)+f(-x).

def Imo2024Q6.General.Aquaesulian {G : Type u_1} [AddCommGroup G] (f : GG) :

The condition on functions in the problem (for a general AddCommGroup and in symmetric form).

Equations
Instances For
    theorem Imo2024Q6.General.Aquaesulian.apply_apply_add {G : Type u_1} [AddCommGroup G] {f : GG} (h : Imo2024Q6.General.Aquaesulian f) (x : G) :
    f (f x + x) = f x + x
    theorem Imo2024Q6.General.Aquaesulian.eq_of_apply_eq_inl {G : Type u_1} [AddCommGroup G] {f : GG} (h : Imo2024Q6.General.Aquaesulian f) {x₁ : G} {x₂ : G} (he : f x₁ = f x₂) (hc : f (f x₁ + x₂) = f x₂ + x₁) :
    x₁ = x₂
    @[simp]
    @[simp]
    theorem Imo2024Q6.General.Aquaesulian.apply_neg_apply_add {G : Type u_1} [AddCommGroup G] {f : GG} (h : Imo2024Q6.General.Aquaesulian f) (x : G) :
    f (-f x) + x = 0
    @[simp]
    theorem Imo2024Q6.General.Aquaesulian.apply_neg_apply {G : Type u_1} [AddCommGroup G] {f : GG} (h : Imo2024Q6.General.Aquaesulian f) (x : G) :
    f (-f x) = -x
    theorem Imo2024Q6.General.Aquaesulian.apply_neg_apply_neg {G : Type u_1} [AddCommGroup G] {f : GG} (h : Imo2024Q6.General.Aquaesulian f) (x : G) :
    f (-f (-x)) = x
    theorem Imo2024Q6.General.Aquaesulian.apply_neg_of_apply_eq {G : Type u_1} [AddCommGroup G] {f : GG} (h : Imo2024Q6.General.Aquaesulian f) {x₁ : G} {x₂ : G} (hx : f x₁ = x₂) :
    f (-x₂) = -x₁
    theorem Imo2024Q6.General.Aquaesulian.apply_neg_eq_neg_iff {G : Type u_1} [AddCommGroup G] {f : GG} (h : Imo2024Q6.General.Aquaesulian f) {x₁ : G} {x₂ : G} :
    f (-x₂) = -x₁ f x₁ = x₂
    theorem Imo2024Q6.General.Aquaesulian.pair_lemma {G : Type u_1} [AddCommGroup G] {f : GG} (h : Imo2024Q6.General.Aquaesulian f) {x : G} {u : G} {v : G} (huv : u v) (hx : f x = u f u = x) (hy : f x = v f v = x) :
    f x = v f x = u
    theorem Imo2024Q6.General.Aquaesulian.g_two {G : Type u_1} [AddCommGroup G] {f : GG} (h : Imo2024Q6.General.Aquaesulian f) {x : G} {y : G} {u : G} {v : G} (huv : u v) (hx : f x + f (-x) = u) (hy : f y + f (-y) = v) :
    f (x + y) = -f (-x) + -f (-y) + v f (x + y) = -f (-x) + -f (-y) + u
    theorem Imo2024Q6.General.Aquaesulian.u_eq_zero {G : Type u_1} [AddCommGroup G] {f : GG} (h : Imo2024Q6.General.Aquaesulian f) {x : G} {y : G} {u : G} {v : G} (huv : u v) (hx : f x + f (-x) = u) (hy : f y + f (-y) = v) (hxyv : f (x + y) = -f (-x) + -f (-y) + v) :
    u = 0
    theorem Imo2024Q6.General.Aquaesulian.u_eq_zero_or_v_eq_zero {G : Type u_1} [AddCommGroup G] {f : GG} (h : Imo2024Q6.General.Aquaesulian f) {x : G} {y : G} {u : G} {v : G} (huv : u v) (hx : f x + f (-x) = u) (hy : f y + f (-y) = v) :
    u = 0 v = 0
    theorem Imo2024Q6.General.Aquaesulian.card_le_two {G : Type u_1} [AddCommGroup G] {f : GG} (h : Imo2024Q6.General.Aquaesulian f) :
    Cardinal.mk (Set.range fun (x : G) => f x + f (-x)) 2

    The condition on functions in the problem (for and in the original form).

    Equations
    Instances For
      theorem Imo2024Q6.Aquaesulian.card_le_two {f : } (h : Imo2024Q6.Aquaesulian f) :
      Cardinal.mk (Set.range fun (x : ) => f x + f (-x)) 2

      An example of a function achieving the maximum number of values of f(r)+f(-r).

      Equations
      Instances For
        theorem Imo2024Q6.floor_fExample (x : ) :
        Imo2024Q6.fExample x = if Int.fract x = 0 then x else x - 1
        theorem imo2024q6 :
        (∀ (f : ), Imo2024Q6.Aquaesulian fCardinal.mk (Set.range fun (x : ) => f x + f (-x)) 2) ∀ (c : ), (∀ (f : ), Imo2024Q6.Aquaesulian fCardinal.mk (Set.range fun (x : ) => f x + f (-x)) c)2 c

        The answer 2 is to be determined by the solver of the original problem.