Documentation

Archive.OxfordInvariants.Summer2021.Week3P1

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

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 OxfordInvariants.Week3P1 {α : Type u_1} [LinearOrderedField α] (n : ) (a : ) (a_pos : in, 0 < a i) (ha : ∀ (i : ), i + 2 na (i + 1) a i + a (i + 2)) :
∃ (b : ), b = iFinset.range n, (a 0) * (a n) / ((a i) * (a (i + 1)))