mathlib3 documentation

mathlib-archive / imo.imo1981_q3

IMO 1981 Q3 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Determine the maximum value of m ^ 2 + n ^ 2, where m and n are integers in {1, 2, ..., 1981} and (n ^ 2 - m * n - m ^ 2) ^ 2 = 1.

The trick to this problem is that m and n have to be consecutive Fibonacci numbers, because you can reduce any solution to a smaller one using the Fibonacci recurrence.

structure imo1981_q3.problem_predicate (N : ) (m n : ) :
Prop
theorem imo1981_q3.problem_predicate_iff (N : ) (m n : ) :
imo1981_q3.problem_predicate N m n m set.Ioc 0 N n set.Ioc 0 N (n ^ 2 - m * n - m ^ 2) ^ 2 = 1
Equations
theorem imo1981_q3.nat_predicate.reduction {N m n : } (h1 : imo1981_q3.nat_predicate N m n) (h2 : 1 < n) :
theorem imo1981_q3.nat_predicate.n_pos {N m n : } (h1 : imo1981_q3.nat_predicate N m n) :
0 < n
theorem imo1981_q3.nat_predicate.m_pos {N m n : } (h1 : imo1981_q3.nat_predicate N m n) :
0 < m
theorem imo1981_q3.nat_predicate.imp_fib {N n : } (m : ) :
theorem imo1981_q3.m_n_bounds {N K : } (HK : N < nat.fib K + nat.fib (K + 1)) {m n : } (h1 : imo1981_q3.nat_predicate N m n) :
m nat.fib K n nat.fib (K + 1)
theorem imo1981_q3.k_bound {N K : } (HK : N < nat.fib K + nat.fib (K + 1)) {M : } (HM : M = nat.fib K ^ 2 + nat.fib (K + 1) ^ 2) {m n : } (h1 : imo1981_q3.problem_predicate N m n) :
m ^ 2 + n ^ 2 M
theorem imo1981_q3.solution_bound {N K : } (HK : N < nat.fib K + nat.fib (K + 1)) {M : } (HM : M = nat.fib K ^ 2 + nat.fib (K + 1) ^ 2) {k : } :
theorem imo1981_q3.solution_greatest {N K : } (HK : N < nat.fib K + nat.fib (K + 1)) {M : } (HM : M = nat.fib K ^ 2 + nat.fib (K + 1) ^ 2) (H : imo1981_q3.problem_predicate N (nat.fib K) (nat.fib (K + 1))) :