Analysis I, Section 2.3

This file is a translation of Section 2.3 of Analysis I to Lean 4. All numbering refers to the original text.

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:

• Definition of multiplication and exponentiation for the "Chapter 2" natural numbers, Chapter2.Nat

Note: at the end of this chapter, the Chapter2.Nat class will be deprecated in favor of the standard Mathlib class _root_.Nat, or ℕ. However, we will develop the properties of Chapter2.Nat "by hand" for pedagogical purposes.

namespace Chapter2

Definition 2.3.1 (Multiplication of natural numbers)

abbrev Nat.mul (n m : Nat) : Nat := Nat.recurse (fun _ prod ↦ prod + m) 0 ninstance Nat.instMul : Mul Nat where mul := mul

Definition 2.3.1 (Multiplication of natural numbers)

theorem Nat.zero_mul (m: Nat) : 0 * m = 0 := recurse_zero (fun _ prod ↦ prod+m) _

Definition 2.3.1 (Multiplication of natural numbers)

theorem Nat.succ_mul (n m: Nat) : (n++) * m = n * m + m := recurse_succ (fun _ prod ↦ prod+m) _ _theorem Nat.one_mul' (m: Nat) : 1 * m = 0 + m := bym:Nat⊢ 1 * m = 0 + m rw [←zero_succ, succ_mul, zero_mul]All goals completed! 🐙theorem Nat.one_mul (m: Nat) : 1 * m = m := bym:Nat⊢ 1 * m = m rw [one_mul', zero_add]All goals completed! 🐙theorem Nat.two_mul (m: Nat) : 2 * m = 0 + m + m := bym:Nat⊢ 2 * m = 0 + m + m rw [←one_succ, succ_mul, one_mul']All goals completed! 🐙/-- This lemma will be useful to prove Lemma 2.3.2. -/ lemma declaration uses 'sorry'Nat.mul_zero (n: Nat) : n * 0 = 0 := byn:Nat⊢ n * 0 = 0 sorryAll goals completed! 🐙/-- This lemma will be useful to prove Lemma 2.3.2. -/ lemma declaration uses 'sorry'Nat.mul_succ (n m:Nat) : n * m++ = n * m + n := byn:Natm:Nat⊢ n * m++ = n * m + n sorryAll goals completed! 🐙/-- Lemma 2.3.2 (Multiplication is commutative) / Exercise 2.3.1 -/ lemma declaration uses 'sorry'Nat.mul_comm (n m: Nat) : n * m = m * n := byn:Natm:Nat⊢ n * m = m * n sorryAll goals completed! 🐙theorem Nat.mul_one (m: Nat) : m * 1 = m := bym:Nat⊢ m * 1 = m rw [mul_comm, one_mul]All goals completed! 🐙/-- Lemma 2.3.3 (Positive natural numbers have no zero divisors) / Exercise 2.3.2 -/ lemma declaration uses 'sorry'Nat.mul_eq_zero_iff (n m: Nat) : n * m = 0 ↔ n = 0 ∨ m = 0 := byn:Natm:Nat⊢ n * m = 0 ↔ n = 0 ∨ m = 0 sorryAll goals completed! 🐙lemma declaration uses 'sorry'Nat.pos_mul_pos {n m: Nat} (h₁: n.isPos) (h₂: m.isPos) : (n * m).isPos := byn:Natm:Nath₁:n.isPosh₂:m.isPos⊢ (n * m).isPos sorryAll goals completed! 🐙

Proposition 2.3.4 (Distributive law)

theorem Nat.mul_add (a b c: Nat) : a * (b + c) = a * b + a * c := bya:Natb:Natc:Nat⊢ a * (b + c) = a * b + a * c -- This proof is written to follow the structure of the original text. revert ca:Natb:Nat⊢ ∀ (c : Nat), a * (b + c) = a * b + a * c; apply inductionhbasea:Natb:Nat⊢ a * (b + 0) = a * b + a * 0hinda:Natb:Nat⊢ ∀ (n : Nat), a * (b + n) = a * b + a * n → a * (b + n++) = a * b + a * n++ .hbasea:Natb:Nat⊢ a * (b + 0) = a * b + a * 0 rw [add_zero]hbasea:Natb:Nat⊢ a * b = a * b + a * 0 rw [mul_zero, add_zero]All goals completed! 🐙 intro c habchinda:Natb:Natc:Nathabc:a * (b + c) = a * b + a * c⊢ a * (b + c++) = a * b + a * c++ rw [add_succ, mul_succ]hinda:Natb:Natc:Nathabc:a * (b + c) = a * b + a * c⊢ a * (b + c) + a = a * b + a * c++ rw [mul_succ, ←add_assoc, ←habc]All goals completed! 🐙

Proposition 2.3.4 (Distributive law)

theorem Nat.add_mul (a b c: Nat) : (a + b)*c = a*c + b*c := bya:Natb:Natc:Nat⊢ (a + b) * c = a * c + b * c simp only [mul_comm, mul_add]All goals completed! 🐙

Proposition 2.3.5 (Multiplication is associative) / Exercise 2.3.3

theorem declaration uses 'sorry'Nat.mul_assoc (a b c: Nat) : (a * b) * c = a * (b * c) := bya:Natb:Natc:Nat⊢ a * b * c = a * (b * c) sorryAll goals completed! 🐙

(Not from textbook) Nat is a commutative semiring.

instance Nat.instCommSemiring : CommSemiring Nat where left_distrib := mul_add right_distrib := add_mul zero_mul := zero_mul mul_zero := mul_zero mul_assoc := mul_assoc one_mul := one_mul mul_one := mul_one mul_comm := mul_comm

Proposition 2.3.6 (Multiplication preserves order)

theorem Nat.mul_lt_mul_of_pos_right {a b c: Nat} (h: a < b) (hc: c.isPos) : a * c < b * c := bya:Natb:Natc:Nath:a < bhc:c.isPos⊢ a * c < b * c -- This proof is written to follow the structure of the original text. rw [lt_iff_add_pos] at ha:Natb:Natc:Nath:∃ d, d.isPos ∧ b = a + dhc:c.isPos⊢ a * c < b * c obtain ⟨ d, hdpos, hd ⟩ := hintro.introa:Natb:Natc:Nathc:c.isPosd:Nathdpos:d.isPoshd:b = a + d⊢ a * c < b * c apply_fun (· * c) at hdintro.introa:Natb:Natc:Nathc:c.isPosd:Nathdpos:d.isPoshd:b * c = (a + d) * c⊢ a * c < b * c rw [add_mul] at hdintro.introa:Natb:Natc:Nathc:c.isPosd:Nathdpos:d.isPoshd:b * c = a * c + d * c⊢ a * c < b * c have hdcpos : (d * c).isPos := pos_mul_pos hdpos hcintro.introa:Natb:Natc:Nathc:c.isPosd:Nathdpos:d.isPoshd:b * c = a * c + d * chdcpos:(d * c).isPos⊢ a * c < b * c rw [lt_iff_add_pos]intro.introa:Natb:Natc:Nathc:c.isPosd:Nathdpos:d.isPoshd:b * c = a * c + d * chdcpos:(d * c).isPos⊢ ∃ d, d.isPos ∧ b * c = a * c + d use d*cAll goals completed! 🐙

Proposition 2.3.6 (Multiplication preserves order)

theorem Nat.mul_gt_mul_of_pos_right {a b c: Nat} (h: a > b) (hc: c.isPos) : a * c > b * c := mul_lt_mul_of_pos_right h hc

Proposition 2.3.6 (Multiplication preserves order)

theorem Nat.mul_lt_mul_of_pos_left {a b c: Nat} (h: a < b) (hc: c.isPos) : c * a < c * b := bya:Natb:Natc:Nath:a < bhc:c.isPos⊢ c * a < c * b simp [mul_comm]a:Natb:Natc:Nath:a < bhc:c.isPos⊢ a * c < b * c exact mul_lt_mul_of_pos_right h hcAll goals completed! 🐙

Proposition 2.3.6 (Multiplication preserves order)

theorem Nat.mul_gt_mul_of_pos_left {a b c: Nat} (h: a > b) (hc: c.isPos) : c * a > c * b := mul_lt_mul_of_pos_left h hc/-- Corollary 2.3.7 (Cancellation law) -/ lemma Nat.mul_cancel_right {a b c: Nat} (h: a * c = b * c) (hc: c.isPos) : a = b := bya:Natb:Natc:Nath:a * c = b * chc:c.isPos⊢ a = b -- This proof is written to follow the structure of the original text. have := trichotomous a ba:Natb:Natc:Nath:a * c = b * chc:c.isPosthis:a < b ∨ a = b ∨ a > b⊢ a = b rcases this with hlt | heq | hgtinla:Natb:Natc:Nath:a * c = b * chc:c.isPoshlt:a < b⊢ a = binr.inla:Natb:Natc:Nath:a * c = b * chc:c.isPosheq:a = b⊢ a = binr.inra:Natb:Natc:Nath:a * c = b * chc:c.isPoshgt:a > b⊢ a = b .inla:Natb:Natc:Nath:a * c = b * chc:c.isPoshlt:a < b⊢ a = b replace hlt := mul_lt_mul_of_pos_right hlt hcinla:Natb:Natc:Nath:a * c = b * chc:c.isPoshlt:a * c < b * c⊢ a = b replace hlt := ne_of_lt _ _ hltinla:Natb:Natc:Nath:a * c = b * chc:c.isPoshlt:a * c ≠ b * c⊢ a = b contradictionAll goals completed! 🐙 .inr.inla:Natb:Natc:Nath:a * c = b * chc:c.isPosheq:a = b⊢ a = b assumptionAll goals completed! 🐙 replace hgt := mul_gt_mul_of_pos_right hgt hcinr.inra:Natb:Natc:Nath:a * c = b * chc:c.isPoshgt:a * c > b * c⊢ a = b replace hgt := ne_of_gt _ _ hgtinr.inra:Natb:Natc:Nath:a * c = b * chc:c.isPoshgt:a * c ≠ b * c⊢ a = b contradictionAll goals completed! 🐙

(Not from textbook) Nat is an ordered semiring.

instance declaration uses 'sorry'Nat.isOrderedRing : IsOrderedRing Nat where zero_le_one := by⊢ 0 ≤ 1 sorryAll goals completed! 🐙 mul_le_mul_of_nonneg_left := by⊢ ∀ (a b c : Nat), a ≤ b → 0 ≤ c → c * a ≤ c * b sorryAll goals completed! 🐙 mul_le_mul_of_nonneg_right := by⊢ ∀ (a b c : Nat), a ≤ b → 0 ≤ c → a * c ≤ b * c sorryAll goals completed! 🐙

Proposition 2.3.9 (Euclid's division lemma) / Exercise 2.3.5

theorem declaration uses 'sorry'Nat.exists_div_mod (n :Nat) {q: Nat} (hq: q.isPos) : ∃ m r: Nat, 0 ≤ r ∧ r < q ∧ n = m * q + r := byn:Natq:Nathq:q.isPos⊢ ∃ m r, 0 ≤ r ∧ r < q ∧ n = m * q + r sorryAll goals completed! 🐙

Definition 2.3.11 (Exponentiation for natural numbers)

abbrev Nat.pow (m n: Nat) : Nat := Nat.recurse (fun _ prod ↦ prod * m) 1 ninstance Nat.instPow : HomogeneousPow Nat where pow := Nat.pow

Definition 2.3.11 (Exponentiation for natural numbers)

theorem Nat.zero_pow_zero : (0:Nat) ^ 0 = 1 := recurse_zero (fun _ prod ↦ prod * 0) _

Definition 2.3.11 (Exponentiation for natural numbers)

theorem Nat.pow_succ (m n: Nat) : (m:Nat) ^ n++ = m^n * m := recurse_succ (fun _ prod ↦ prod * m) _ _

Exercise 2.3.4

theorem declaration uses 'sorry'Nat.sq_add_eq (a b: Nat) : (a + b) ^ (2 : Nat) = a ^ (2 : Nat) + 2 * a * b + b ^ (2 : Nat) := bya:Natb:Nat⊢ (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 sorryAll goals completed! 🐙end Chapter2