mathlib3 documentation

mathlib-archive / oxford_invariants.2021summer.week3_p1

The Oxford Invariants Puzzle Challenges - Summer 2021, Week 3, Problem 1 #

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

Original statement #

Let n ≥ 3, a₁, ..., aₙ be strictly positive integers such that aᵢ ∣ aᵢ₋₁ + aᵢ₊₁ for i = 2, ..., n - 1. Show that $\sum_{i=1}^{n-1}\dfrac{a_0a_n}{a_ia_{i+1}} ∈ \mathbb N$.

Comments #

Mathlib is based on type theory, so saying that a rational is a natural doesn't make sense. Instead, we ask that there exists b : ℕ whose cast to α is the sum we want.

In mathlib, starts at 0. To make the indexing cleaner, we use a₀, ..., aₙ₋₁ instead of a₁, ..., aₙ. Similarly, it's nicer to not use subtraction of naturals, so we replace aᵢ ∣ aᵢ₋₁ + aᵢ₊₁ by aᵢ₊₁ ∣ aᵢ + aᵢ₊₂.

We don't actually have to work in or . We can be even more general by stating the result for any linearly ordered field.

Instead of having n naturals, we use a function a : ℕ → ℕ.

In the proof itself, we replace n : ℕ, 1 ≤ n by n + 1.

The statement is actually true for n = 0, 1 (n = 1, 2 before the reindexing) as the sum is simply 0 and 1 respectively. So the version we prove is slightly more general.

Overall, the indexing is a bit of a mess to understand. But, trust Lean, it works.

Formalised statement #

Let n : ℕ, a : ℕ → ℕ, ∀ i ≤ n, 0 < a i, ∀ i, i + 2 ≤ n → aᵢ₊₁ ∣ aᵢ + aᵢ₊₂ (read as "implies"). Then there exists b : ℕ such that b as an element of any linearly ordered field equals $\sum_{i=0}^{n-1} (a_0 a_n) / (a_i a_{i+1})$.

Proof outline #

The case n = 0 is trivial.

For n + 1, we prove the result by induction but by adding aₙ₊₁ ∣ aₙ * b - a₀ to the induction hypothesis, where b is the previous sum, $\sum_{i=0}^{n-1} (a_0 a_n) / (a_i a_{i+1})$, as a natural.

theorem oxford_invariants.week3_p1 {α : Type u_1} [linear_ordered_field α] (n : ) (a : ) (a_pos : (i : ), i n 0 < a i) (ha : (i : ), i + 2 n a (i + 1) a i + a (i + 2)) :
(b : ), b = (finset.range n).sum (λ (i : ), (a 0) * (a n) / ((a i) * (a (i + 1))))