Аналіз I, Глава 4.3

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:

• Basic properties of absolute value and exponentiation on the rational numbers (here we use the Mathlib rational numbers ℚ rather than the Section 4.2 rational numbers).

Note: to avoid notational conflict, we are using the standard Mathlib definitions of absolute value and exponentiation. As such, it is possible to solve several of the exercises here rather easily using the Mathlib API for these operations. However, the spirit of the exercises is to solve these instead using the API provided in this section, as well as more basic Mathlib API for the rational numbers that does not reference either absolute value or exponentiation.

def Rat.close (ε x y : ℚ) : Prop

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

Equations

• ε.close x y = (|x - y| ≤ ε)

@[reducible, inline]

abbrev Section_4_3.abs (x : ℚ) : ℚ

Визначення 4.3.1 (Absolute value)

Equations

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

theorem Section_4_3.abs_of_pos {x : ℚ} (hx : x > 0) : abs x = x

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

Визначення 4.3.1 (Absolute value)

theorem Section_4_3.abs_of_zero : abs 0 = 0

Визначення 4.3.1 (Absolute value)

theorem Section_4_3.abs_eq_abs (x : ℚ) : abs x = |x|

(Не із книги) 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|

theorem Section_4_3.dist_eq (x y : ℚ) : dist x y = |x - y|

Визначення 4.2 (Distance). We avoid the Mathlib notion of distance here because it is real-valued.

theorem Section_4_3.abs_nonneg (x : ℚ) : |x| ≥ 0

Твердження 4.3.3(a) / Вправа 4.3.1

theorem Section_4_3.abs_eq_zero_iff (x : ℚ) : |x| = 0 ↔ x = 0

Твердження 4.3.3(a) / Вправа 4.3.1

theorem Section_4_3.abs_add (x y : ℚ) : |x + y| ≤ |x| + |y|

Твердження 4.3.3(b) / Вправа 4.3.1

theorem Section_4_3.abs_le_iff (x y : ℚ) : -y ≤ x ∧ x ≤ y ↔ |x| ≤ y

Твердження 4.3.3(c) / Вправа 4.3.1

theorem Section_4_3.le_abs (x : ℚ) : -|x| ≤ x ∧ x ≤ |x|

Твердження 4.3.3(c) / Вправа 4.3.1

theorem Section_4_3.abs_mul (x y : ℚ) : |x * y| = |x| * |y|

Твердження 4.3.3(d) / Вправа 4.3.1

theorem Section_4_3.abs_neg (x : ℚ) : |(-x)| = |x|

Твердження 4.3.3(d) / Вправа 4.3.1

theorem Section_4_3.dist_nonneg (x y : ℚ) : dist x y ≥ 0

Твердження 4.3.3(e) / Вправа 4.3.1

theorem Section_4_3.dist_eq_zero_iff (x y : ℚ) : dist x y = 0 ↔ x = y

Твердження 4.3.3(e) / Вправа 4.3.1

theorem Section_4_3.dist_symm (x y : ℚ) : dist x y = dist y x

Твердження 4.3.3(f) / Вправа 4.3.1

theorem Section_4_3.dist_le (x y z : ℚ) : dist x z ≤ dist x y + dist y z

Твердження 4.3.3(f) / Вправа 4.3.1

theorem Section_4_3.close_iff (ε x y : ℚ) : ε.close x y ↔ |x - y| ≤ ε

Визначення 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

Твердження 4.3.7(a) / Вправа 4.3.2

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

Твердження 4.3.7(b) / Вправа 4.3.2

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

Твердження 4.3.7(c) / Вправа 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)

Твердження 4.3.7(d) / Вправа 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)

Твердження 4.3.7(d) / Вправа 4.3.2

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

Твердження 4.3.7(e) / Вправа 4.3.2, slightly strengthened

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

Твердження 4.3.7(f) / Вправа 4.3.2

theorem Section_4_3.close_mul_right {ε x y z : ℚ} (hε : ε ≥ 0) (hxy : ε.close x y) : (ε * |z|).close (x * z) (y * z)

Твердження 4.3.7(g) / Вправа 4.3.2

theorem Section_4_3.close_mul_mul {ε δ x y z w : ℚ} (hε : ε ≥ 0) (hxy : ε.close x y) (hzw : δ.close z w) : (ε * |z| + δ * |x| + ε * δ).close (x * z) (y * w)

Твердження 4.3.7(h) / Вправа 4.3.2

theorem Section_4_3.pow_zero (x : ℚ) : x ^ 0 = 1

Визначення 4.3.9 (exponentiation). Here we use the Mathlib definition.

theorem Section_4_3.pow_succ (x : ℚ) (n : ℕ) : x ^ (n + 1) = x ^ n * x

Визначення 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)

Твердження 4.3.10 (Properties of exponentiation, I) / Вправа 4.3.3

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

Твердження 4.3.10(a) (Properties of exponentiation, I) / Вправа 4.3.3

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

Твердження 4.3.10(a) (Properties of exponentiation, I) / Вправа 4.3.3

theorem Section_4_3.pow_eq_zero (x : ℚ) (n : ℕ) : x ^ n = 0 ↔ x = 0

Твердження 4.3.10(b) (Properties of exponentiation, I) / Вправа 4.3.3

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

Твердження 4.3.10(c) (Properties of exponentiation, I) / Вправа 4.3.3

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

Твердження 4.3.10(c) (Properties of exponentiation, I) / Вправа 4.3.3

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

Твердження 4.3.10(c) (Properties of exponentiation, I) / Вправа 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

Твердження 4.3.10(c) (Properties of exponentiation, I) / Вправа 4.3.3

theorem Section_4_3.pow_abs (x : ℚ) (n : ℕ) : |x| ^ n = |x ^ n|

Твердження 4.3.10(d) (Properties of exponentiation, I) / Вправа 4.3.3

theorem Section_4_3.zpow_neg (x : ℚ) (n : ℕ) : x ^ (-↑n) = 1 / x ^ n

Визначення 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 : ℤ) : x ^ n * x ^ m = x ^ (n + m)

Твердження 4.3.12(a) (Properties of exponentiation, II) / Вправа 4.3.4

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

Твердження 4.3.12(a) (Properties of exponentiation, II) / Вправа 4.3.4

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

Твердження 4.3.12(a) (Properties of exponentiation, II) / Вправа 4.3.4

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

Твердження 4.3.12(b) (Properties of exponentiation, II) / Вправа 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

Твердження 4.3.12(b) (Properties of exponentiation, II) / Вправа 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

Твердження 4.3.12(c) (Properties of exponentiation, II) / Вправа 4.3.4

theorem Section_4_3.zpow_abs (x : ℚ) (n : ℤ) (hx : x ≠ 0) : |x| ^ n = |x ^ n|

Твердження 4.3.12(d) (Properties of exponentiation, II) / Вправа 4.3.4

theorem Section_4_3.two_pow_geq (N : ℕ) : 2 ^ N ≥ N

Вправа 4.3.5