Documentation

EstimateTools.analysis.Section_2_3

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.

@[reducible, inline]

abbrev Chapter2.Nat.mul (n m : Nat) :

Definition 2.3.1 (Multiplication of natural numbers)

Equations

n.mul m = Chapter2.Nat.recurse (fun (x prod : Chapter2.Nat) => prod + m) 0 n

Instances For

instance Chapter2.Nat.mul_inst :

Equations

Chapter2.Nat.mul_inst = { mul := Chapter2.Nat.mul }

theorem Chapter2.zero_mul (m : Nat) :

0 * m = 0

Definition 2.3.1 (Multiplication of natural numbers)

theorem Chapter2.succ_mul (n m : Nat) :

n++ * m = n * m + m

Definition 2.3.1 (Multiplication of natural numbers)

theorem Chapter2.one_mul' (m : Nat) :

1 * m = 0 + m

theorem Chapter2.one_mul (m : Nat) :

1 * m = m

theorem Chapter2.two_mul (m : Nat) :

2 * m = 0 + m + m

theorem Chapter2.mul_comm (n m : Nat) :

n * m = m * n

Lemma 2.3.2 (Multiplication is commutative) / Exercise 2.3.1

theorem Chapter2.mul_one (m : Nat) :

m * 1 = m

theorem Chapter2.mul_zero (n : Nat) :

n * 0 = 0

theorem Chapter2.mul_succ (n m : Nat) :

n * m++ = n * m + n

theorem Chapter2.mul_eq_zero_iff (n m : Nat) :

n * m = 0 ↔ n = 0 ∨ m = 0

Lemma 2.3.3 (Positive natural numbers have no zero divisors) / Exercise 2.3.2

theorem Chapter2.pos_mul_pos {n m : Nat} (h₁ : n.isPos) (h₂ : m.isPos) :

(n * m).isPos

theorem Chapter2.mul_add (a b c : Nat) :

a * (b + c) = a * b + a * c

Proposition 2.3.4 (Distributive law)

theorem Chapter2.add_mul (a b c : Nat) :

(a + b) * c = a * c + b * c

Proposition 2.3.4 (Distributive law)

theorem Chapter2.mul_assoc (a b c : Nat) :

a * b * c = a * (b * c)

Proposition 2.3.5 (Multiplication is associative) / Exercise 2.3.3

instance Chapter2.Nat.commSemiring_inst :

CommSemiring Nat

(Not from textbook) Nat is a commutative semiring.

Equations

One or more equations did not get rendered due to their size.

theorem Chapter2.mul_lt_mul_of_pos_right {a b c : Nat} (h : a < b) (hc : c.isPos) :

a * c < b * c

Proposition 2.3.6 (Multiplication preserves order)

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

a * c > b * c

Proposition 2.3.6 (Multiplication preserves order)

theorem Chapter2.mul_lt_mul_of_pos_left {a b c : Nat} (h : a < b) (hc : c.isPos) :

c * a < c * b

Proposition 2.3.6 (Multiplication preserves order)

theorem Chapter2.mul_gt_mul_of_pos_left {a b c : Nat} (h : a > b) (hc : c.isPos) :

c * a > c * b

Proposition 2.3.6 (Multiplication preserves order)

theorem Chapter2.mul_cancel_right {a b c : Nat} (h : a * c = b * c) (hc : c.isPos) :

a = b

Corollary 2.3.7 (Cancellation law)

instance Chapter2.Nat.isOrderedRing :

IsOrderedRing Nat

(Not from textbook) Nat is an ordered semiring.

theorem Chapter2.exists_div_mod (n : Nat) {q : Nat} (hq : q.isPos) :

∃ (m : Nat) (r : Nat), 0 ≤ r ∧ r < q ∧ n = m * q + r

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

@[reducible, inline]

abbrev Chapter2.Nat.pow (m n : Nat) :

Definition 2.3.11 (Exponentiation for natural numbers)

Equations

m.pow n = Chapter2.Nat.recurse (fun (x prod : Chapter2.Nat) => prod * m) 1 n

Instances For

instance Chapter2.Nat.pow_inst :

HomogeneousPow Nat

Equations

Chapter2.Nat.pow_inst = { pow := Chapter2.Nat.pow }

theorem Chapter2.zero_pow_zero :

0 ^ 0 = 1

Definition 2.3.11 (Exponentiation for natural numbers)

theorem Chapter2.zero_pow_succ (m n : Nat) :

m ^ n++ = m ^ n * m

Definition 2.3.11 (Exponentiation for natural numbers)

theorem Chapter2.sq_add_eq (a b : Nat) :

(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2

Exercise 2.3.4