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} \frac{a_{0} a_{n}}{a_{i} a_{i + 1}} \in 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.

Base case:
- $\sum_{i = 0}^{0} (a_{0} a_{0 + 1}) / (a_{0} a_{0 + 1})$ is a natural: $\sum_{i = 0}^{0} (a_{0} a_{0 + 1}) / (a_{0} a_{0 + 1}) = (a_{0} a_{1}) / (a_{0} a_{1}) = 1$ .
- Divisibility condition: a₀ * 1 - a₀ = 0 is clearly divisible by a₁.
Induction step:
- $\sum_{i = 0}^{n} (a_{0} a_{n + 1}) / (a_{i} a_{i + 1})$ is a natural: $\sum_{i = 0}^{n + 1} (a_{0} a_{n + 2}) / (a_{i} a_{i + 1}) = \sum_{i = 0}^{n} (a_{0} a_{n + 2}) / (a_{i} a_{i + 1}) + (a_{0} a_{n + 2}) / (a_{n + 1} a_{n + 2}) = a_{n + 2} / a_{n + 1} \times \sum_{i = 0}^{n} (a_{0} a_{n + 1}) / (a_{i} a_{i + 1}) + a_{0} / a_{n + 1} = a_{n + 2} / a_{n + 1} \times b + a_{0} / a_{n + 1} = (a_{n} + a_{n + 2}) / a_{n + 1} \times b - (a_{n} b - a_{0}) (a_{n + 1})$ which is a natural because (aₙ + aₙ₊₂)/aₙ₊₁, b and (aₙ * b - a₀)/aₙ₊₁ are (plus an annoying inequality, or the fact that the original sum is positive because its terms are).
- Divisibility condition: aₙ₊₁ * ((aₙ + aₙ₊₂)/aₙ₊₁ * b - (aₙ * b - a₀)/aₙ₊₁) - a₀ = aₙ₊₁aₙ₊₂b is divisible by aₙ₊₂.

source

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))))