Analysis I, Section 4.4: gaps in the rational numbers

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

• Irrationality of √2, and related facts about the rational numbers

Many of the results here can be established more quickly by relying more heavily on the Mathlib API; one can set oneself the exercise of doing so.

Tips from past users

Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.

• (Add tip here)

theorem Rat.between_int (x : ℚ) : ∃! n : ℤ, ↑n ≤ x ∧ x < ↑n + 1

Proposition 4.4.1 (Interspersing of integers by rationals) / Exercise 4.4.1

theorem Nat.exists_gt (x : ℚ) : ∃ (n : ℕ), ↑n > x

theorem Rat.exists_between_rat {x y : ℚ} (h : x < y) : ∃ (z : ℚ), x < z ∧ z < y

Proposition 4.4.3 (Interspersing of rationals)

theorem Nat.no_infinite_descent : ¬∃ (a : ℕ → ℕ), ∀ (n : ℕ), a (n + 1) < a n

Exercise 4.4.2

def Int.infinite_descent : Decidable (∃ (a : ℕ → ℤ), ∀ (n : ℕ), a (n + 1) < a n)

Equations

• Int.infinite_descent = sorry

theorem Nat.even_or_odd'' (n : ℕ) : Even n ∨ Odd n

theorem Nat.not_even_and_odd (n : ℕ) : ¬(Even n ∧ Odd n)

theorem Rat.not_exist_sqrt_two : ¬∃ (x : ℚ), x ^ 2 = 2

Proposition 4.4.4 / Exercise 4.4.3

theorem Rat.exist_approx_sqrt_two {ε : ℚ} (hε : ε > 0) : ∃ x ≥ 0, x ^ 2 < 2 ∧ 2 < (x + ε) ^ 2

Proposition 4.4.5