Documentation

Analysis.Section_4_3

def Rat.Close (ε x y : ℚ) :

This definition needs to be made outside of the Section 4.3 namespace for technical reasons.

Equations

ε.Close x y = (|x - y| ≤ ε)

Instances For

@[reducible, inline]

abbrev Section_4_3.abs (x : ℚ) :

Definition 4.3.1 (Absolute value)

Equations

Section_4_3.abs x = if x > 0 then x else if x < 0 then -x else 0

Instances For

theorem Section_4_3.abs_of_pos {x : ℚ} (hx : 0 < x) :

abs x = x

theorem Section_4_3.abs_of_neg {x : ℚ} (hx : x < 0) :

abs x = -x

Definition 4.3.1 (Absolute value)

theorem Section_4_3.abs_of_zero :

abs 0 = 0

Definition 4.3.1 (Absolute value)

theorem Section_4_3.abs_eq_abs (x : ℚ) :

(Not from textbook) This definition of absolute value agrees with the Mathlib one. Henceforth we use the Mathlib absolute value.

@[reducible, inline]

abbrev Section_4_3.dist (x y : ℚ) :

Equations

Section_4_3.dist x y = |x - y|

Instances For

theorem Section_4_3.dist_eq (x y : ℚ) :

dist x y = |x - y|

Definition 4.2 (Distance). We avoid the Mathlib notion of distance here because it is real-valued.

theorem Section_4_3.abs_nonneg (x : ℚ) :

Proposition 4.3.3(a) / Exercise 4.3.1

theorem Section_4_3.abs_eq_zero_iff (x : ℚ) :

|x| = 0 ↔ x = 0

Proposition 4.3.3(a) / Exercise 4.3.1

theorem Section_4_3.abs_add (x y : ℚ) :

|x + y| ≤ |x| + |y|

Proposition 4.3.3(b) / Exercise 4.3.1

theorem Section_4_3.abs_le_iff (x y : ℚ) :

-y ≤ x ∧ x ≤ y ↔ |x| ≤ y

Proposition 4.3.3(c) / Exercise 4.3.1

theorem Section_4_3.le_abs (x : ℚ) :

-|x| ≤ x ∧ x ≤ |x|

Proposition 4.3.3(c) / Exercise 4.3.1

theorem Section_4_3.abs_mul (x y : ℚ) :

|x * y| = |x| * |y|

Proposition 4.3.3(d) / Exercise 4.3.1

theorem Section_4_3.abs_neg (x : ℚ) :

Proposition 4.3.3(d) / Exercise 4.3.1

theorem Section_4_3.dist_nonneg (x y : ℚ) :

dist x y ≥ 0

Proposition 4.3.3(e) / Exercise 4.3.1

theorem Section_4_3.dist_eq_zero_iff (x y : ℚ) :

dist x y = 0 ↔ x = y

Proposition 4.3.3(e) / Exercise 4.3.1

theorem Section_4_3.dist_symm (x y : ℚ) :

dist x y = dist y x

Proposition 4.3.3(f) / Exercise 4.3.1

theorem Section_4_3.dist_le (x y z : ℚ) :

dist x z ≤ dist x y + dist y z

Proposition 4.3.3(f) / Exercise 4.3.1

theorem Section_4_3.close_iff (ε x y : ℚ) :

ε.Close x y ↔ |x - y| ≤ ε

Definition 4.3.4 (eps-closeness). In the text the notion is undefined for ε zero or negative, but it is more convenient in Lean to assign a "junk" definition in this case. But this also allows some relaxations of hypotheses in the lemmas that follow.

theorem Section_4_3.close_refl (x : ℚ) :

Rat.Close 0 x x

theorem Section_4_3.eq_if_close (x y : ℚ) :

x = y ↔ ∀ ε > 0, ε.Close x y

Proposition 4.3.7(a) / Exercise 4.3.2

theorem Section_4_3.close_symm (ε x y : ℚ) :

ε.Close x y ↔ ε.Close y x

Proposition 4.3.7(b) / Exercise 4.3.2

theorem Section_4_3.close_trans {ε δ x y z : ℚ} (hxy : ε.Close x y) (hyz : δ.Close y z) :

(ε + δ).Close x z

Proposition 4.3.7(c) / Exercise 4.3.2

theorem Section_4_3.add_close {ε δ x y z w : ℚ} (hxy : ε.Close x y) (hzw : δ.Close z w) :

(ε + δ).Close (x + z) (y + w)

Proposition 4.3.7(d) / Exercise 4.3.2

theorem Section_4_3.sub_close {ε δ x y z w : ℚ} (hxy : ε.Close x y) (hzw : δ.Close z w) :

(ε + δ).Close (x - z) (y - w)

Proposition 4.3.7(d) / Exercise 4.3.2

theorem Section_4_3.close_mono {ε ε' x y : ℚ} (hxy : ε.Close x y) (hε : ε' ≥ ε) :

ε'.Close x y

Proposition 4.3.7(e) / Exercise 4.3.2, slightly strengthened

theorem Section_4_3.close_between {ε x y z w : ℚ} (hxy : ε.Close x y) (hxz : ε.Close x z) (hbetween : y ≤ w ∧ w ≤ z ∨ z ≤ w ∧ w ≤ y) :

ε.Close x w

Proposition 4.3.7(f) / Exercise 4.3.2

theorem Section_4_3.close_mul_right {ε x y z : ℚ} (hxy : ε.Close x y) :

(ε * |z|).Close (x * z) (y * z)

Proposition 4.3.7(g) / Exercise 4.3.2

theorem Section_4_3.close_mul_mul {ε δ x y z w : ℚ} (hxy : ε.Close x y) (hzw : δ.Close z w) :

(ε * |z| + δ * |x| + ε * δ).Close (x * z) (y * w)

Proposition 4.3.7(h) / Exercise 4.3.2

theorem Section_4_3.close_mul_mul' {ε δ x y z w : ℚ} (hxy : ε.Close x y) (hzw : δ.Close z w) :

(ε * |z| + δ * |y|).Close (x * z) (y * w)

This variant of Proposition 4.3.7(h) was not in the textbook, but can be useful in some later exercises.

theorem Section_4_3.pow_zero (x : ℚ) :

x ^ 0 = 1

Definition 4.3.9 (exponentiation). Here we use the Mathlib definition.

theorem Section_4_3.pow_succ (x : ℚ) (n : ℕ) :

x ^ (n + 1) = x ^ n * x

Definition 4.3.9 (exponentiation). Here we use the Mathlib definition.

theorem Section_4_3.pow_add (x : ℚ) (m n : ℕ) :

x ^ n * x ^ m = x ^ (n + m)

Proposition 4.3.10(a) (Properties of exponentiation, I) / Exercise 4.3.3

theorem Section_4_3.pow_mul (x : ℚ) (m n : ℕ) :

(x ^ n) ^ m = x ^ (n * m)

Proposition 4.3.10(a) (Properties of exponentiation, I) / Exercise 4.3.3

theorem Section_4_3.mul_pow (x y : ℚ) (n : ℕ) :

(x * y) ^ n = x ^ n * y ^ n

Proposition 4.3.10(a) (Properties of exponentiation, I) / Exercise 4.3.3

theorem Section_4_3.pow_eq_zero (x : ℚ) (n : ℕ) (hn : 0 < n) :

x ^ n = 0 ↔ x = 0

Proposition 4.3.10(b) (Properties of exponentiation, I) / Exercise 4.3.3

theorem Section_4_3.pow_nonneg {x : ℚ} (n : ℕ) (hx : x ≥ 0) :

x ^ n ≥ 0

Proposition 4.3.10(c) (Properties of exponentiation, I) / Exercise 4.3.3

theorem Section_4_3.pow_pos {x : ℚ} (n : ℕ) (hx : x > 0) :

x ^ n > 0

Proposition 4.3.10(c) (Properties of exponentiation, I) / Exercise 4.3.3

theorem Section_4_3.pow_ge_pow (x y : ℚ) (n : ℕ) (hxy : x ≥ y) (hy : y ≥ 0) :

x ^ n ≥ y ^ n

Proposition 4.3.10(c) (Properties of exponentiation, I) / Exercise 4.3.3

theorem Section_4_3.pow_gt_pow (x y : ℚ) (n : ℕ) (hxy : x > y) (hy : y ≥ 0) (hn : n > 0) :

x ^ n > y ^ n

Proposition 4.3.10(c) (Properties of exponentiation, I) / Exercise 4.3.3

theorem Section_4_3.pow_abs (x : ℚ) (n : ℕ) :

|x| ^ n = |x ^ n|

Proposition 4.3.10(d) (Properties of exponentiation, I) / Exercise 4.3.3

theorem Section_4_3.zpow_neg (x : ℚ) (n : ℕ) :

x ^ (-↑n) = 1 / x ^ n

Definition 4.3.11 (Exponentiation to a negative number). Here we use the Mathlib notion of integer exponentiation

theorem Section_4_3.pow_eq_zpow (x : ℚ) (n : ℕ) :

x ^ ↑n = x ^ n

theorem Section_4_3.zpow_add (x : ℚ) (n m : ℤ) (hx : x ≠ 0) :

x ^ n * x ^ m = x ^ (n + m)

Proposition 4.3.12(a) (Properties of exponentiation, II) / Exercise 4.3.4

theorem Section_4_3.zpow_mul (x : ℚ) (n m : ℤ) :

(x ^ n) ^ m = x ^ (n * m)

Proposition 4.3.12(a) (Properties of exponentiation, II) / Exercise 4.3.4

theorem Section_4_3.mul_zpow (x y : ℚ) (n : ℤ) :

(x * y) ^ n = x ^ n * y ^ n

Proposition 4.3.12(a) (Properties of exponentiation, II) / Exercise 4.3.4

theorem Section_4_3.zpow_pos {x : ℚ} (n : ℤ) (hx : x > 0) :

x ^ n > 0

Proposition 4.3.12(b) (Properties of exponentiation, II) / Exercise 4.3.4

theorem Section_4_3.zpow_ge_zpow {x y : ℚ} {n : ℤ} (hxy : x ≥ y) (hy : y > 0) (hn : n > 0) :

x ^ n ≥ y ^ n

Proposition 4.3.12(b) (Properties of exponentiation, II) / Exercise 4.3.4

theorem Section_4_3.zpow_ge_zpow_ofneg {x y : ℚ} {n : ℤ} (hxy : x ≥ y) (hy : y > 0) (hn : n < 0) :

x ^ n ≤ y ^ n

theorem Section_4_3.zpow_inj {x y : ℚ} {n : ℤ} (hx : x > 0) (hy : y > 0) (hn : n ≠ 0) (hxy : x ^ n = y ^ n) :

x = y

Proposition 4.3.12(c) (Properties of exponentiation, II) / Exercise 4.3.4

theorem Section_4_3.zpow_abs (x : ℚ) (n : ℤ) :

|x| ^ n = |x ^ n|

Proposition 4.3.12(d) (Properties of exponentiation, II) / Exercise 4.3.4

theorem Section_4_3.two_pow_geq (N : ℕ) :

2 ^ N ≥ N

Exercise 4.3.5