IMO 2008 Q2 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. (a) Prove that lean x^2 / (x-1)^2 + y^2 / (y-1)^2 + z^2 / (z-1)^2 ≥ 1 for all real numbers x,y, z, each different from 1, and satisfying xyz = 1.

(b) Prove that equality holds above for infinitely many triples of rational numbers x, y, z, each different from 1, and satisfying xyz = 1.

Solution #

(a) Since xyz = 1, we can apply the substitution x = a/b, y = b/c, z = c/a. Then we define m = c-b, n = b-a and rewrite the inequality as LHS - 1 ≥ 0 using c, m and n. We factor LHS - 1 as a square, which finishes the proof.

(b) We present a set W of rational triples. We prove that W is a subset of the set of rational solutions to the equation, and that W is infinite.

source

theorem imo2008_q2.subst_abc {x y z : ℝ} (h : x * y * z = 1) :

∃ (a b c : ℝ), a ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0 ∧ x = a / b ∧ y = b / c ∧ z = c / a

source

theorem imo2008_q2.imo2008_q2a (x y z : ℝ) (h : x * y * z = 1) (hx : x ≠ 1) (hy : y ≠ 1) (hz : z ≠ 1) :

x ^ 2 / (x - 1) ^ 2 + y ^ 2 / (y - 1) ^ 2 + z ^ 2 / (z - 1) ^ 2 ≥ 1

source

def imo2008_q2.rational_solutions :

set (ℚ × ℚ × ℚ)

Equations

imo2008_q2.rational_solutions = {s : ℚ × ℚ × ℚ | ∃ (x y z : ℚ), s = (x, y, z) ∧ x ≠ 1 ∧ y ≠ 1 ∧ z ≠ 1 ∧ x * y * z = 1 ∧ x ^ 2 / (x - 1) ^ 2 + y ^ 2 / (y - 1) ^ 2 + z ^ 2 / (z - 1) ^ 2 = 1}

source

theorem imo2008_q2.imo2008_q2b :

imo2008_q2.rational_solutions.infinite