Аналіз 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:

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.

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

def Rat.close (ε : ) (x y:) := |x-y| ε
namespace Section_4_3

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

abbrev abs (x:) : := if x > 0 then x else (if x < 0 then -x else 0)
theorem abs_of_pos {x: } (hx: x > 0) : abs x = x := x:hx:x > 0abs x = x All goals completed! 🐙

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

theorem abs_of_neg {x: } (hx: x < 0) : abs x = -x := x:hx:x < 0abs x = -x x:hx:x < 00 < x x = -x x:hx:x < 0hx':0 < xx = -x All goals completed! 🐙

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

theorem abs_of_zero : abs 0 = 0 := abs 0 = 0 All goals completed! 🐙

(Не із книги) This definition of absolute value agrees with the Mathlib one. Henceforth we use the Mathlib absolute value.

theorem declaration uses 'sorry'abs_eq_abs (x: ) : abs x = |x| := x:abs x = |x| All goals completed! 🐙
abbrev dist (x y : ) := |x - y|

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

theorem dist_eq (x y: ) : dist x y = |x-y| := rfl

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

theorem declaration uses 'sorry'abs_nonneg (x: ) : |x| 0 := x:|x| 0 All goals completed! 🐙

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

theorem declaration uses 'sorry'abs_eq_zero_iff (x: ) : |x| = 0 x = 0 := x:|x| = 0 x = 0 All goals completed! 🐙

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

theorem declaration uses 'sorry'abs_add (x y:) : |x + y| |x| + |y| := x:y:|x + y| |x| + |y| All goals completed! 🐙

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

theorem declaration uses 'sorry'abs_le_iff (x y:) : -y x x y |x| y := x:y:-y x x y |x| y All goals completed! 🐙

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

theorem declaration uses 'sorry'le_abs (x:) : -|x| x x |x| := x:-|x| x x |x| All goals completed! 🐙

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

theorem declaration uses 'sorry'abs_mul (x y:) : |x * y| = |x| * |y| := x:y:|x * y| = |x| * |y| All goals completed! 🐙

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

theorem declaration uses 'sorry'abs_neg (x:) : |-x| = |x| := x:|(-x)| = |x| All goals completed! 🐙

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

theorem declaration uses 'sorry'dist_nonneg (x y:) : dist x y 0 := x:y:dist x y 0 All goals completed! 🐙

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

theorem declaration uses 'sorry'dist_eq_zero_iff (x y:) : dist x y = 0 x = y := x:y:dist x y = 0 x = y All goals completed! 🐙

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

theorem declaration uses 'sorry'dist_symm (x y:) : dist x y = dist y x := x:y:dist x y = dist y x All goals completed! 🐙

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

theorem declaration uses 'sorry'dist_le (x y z:) : dist x z dist x y + dist y z := x:y:z:dist x z dist x y + dist y z All goals completed! 🐙

Визначення 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 close_iff (ε x y:): ε.close x y |x - y| ε := ε:x:y:ε.close x y |x - y| ε All goals completed! 🐙

Приклади 4.3.6

declaration uses 'sorry'example : (0.1:).close (0.99:) (1.01:) := Rat.close 0.1 0.99 1.01 All goals completed! 🐙

Приклади 4.3.6

declaration uses 'sorry'example : ¬ (0.01:).close (0.99:) (1.01:) := ¬Rat.close 1e-2 0.99 1.01 All goals completed! 🐙

Приклади 4.3.6

declaration uses 'sorry'example (ε : ) ( : ε > 0) : ε.close 2 2 := ε::ε > 0ε.close 2 2 All goals completed! 🐙
theorem declaration uses 'sorry'close_refl (x:) : (0:).close x x := x:Rat.close 0 x x All goals completed! 🐙

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

theorem declaration uses 'sorry'eq_if_close (x y:) : x = y ε:, ε > 0 ε.close x y := x:y:x = y ε > 0, ε.close x y All goals completed! 🐙

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

theorem declaration uses 'sorry'close_symm (ε x y:) : ε.close x y ε.close y x := ε:x:y:ε.close x y ε.close y x All goals completed! 🐙

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

theorem declaration uses 'sorry'close_trans {ε δ x y:} (hxy: ε.close x y) (hyz: δ.close y z) : (ε + δ).close x z := z:ε:δ:x:y:hxy:ε.close x yhyz:δ.close y z(ε + δ).close x z All goals completed! 🐙

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

theorem declaration uses 'sorry'add_close {ε δ x y z w:} (hxy: ε.close x y) (hzw: δ.close z w) : (ε + δ).close (x+z) (y+w) := ε:δ:x:y:z:w:hxy:ε.close x yhzw:δ.close z w(ε + δ).close (x + z) (y + w) All goals completed! 🐙

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

theorem declaration uses 'sorry'sub_close {ε δ x y z w:} (hxy: ε.close x y) (hzw: δ.close z w) : (ε + δ).close (x-z) (y-w) := ε:δ:x:y:z:w:hxy:ε.close x yhzw:δ.close z w(ε + δ).close (x - z) (y - w) All goals completed! 🐙

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

theorem declaration uses 'sorry'close_mono {ε ε' x y:} (hxy: ε.close x y) (: ε' ε) : ε'.close x y := ε:ε':x:y:hxy:ε.close x y:ε' εε'.close x y All goals completed! 🐙

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

theorem declaration uses 'sorry'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 := ε:x:y:z:w:hxy:ε.close x yhyz:ε.close x zhbetween:y w w z z w w yε.close x w All goals completed! 🐙

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

theorem declaration uses 'sorry'close_mul_right {ε x y z:} (: ε 0) (hxy: ε.close x y) : (ε*|z|).close (x * z) (y * z) := ε:x:y:z::ε 0hxy:ε.close x y(ε * |z|).close (x * z) (y * z) All goals completed! 🐙

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

theorem close_mul_mul {ε δ x y z w:} (: ε 0) (hxy: ε.close x y) (hzw: δ.close z w) : (ε*|z|+δ*|x|+ε*δ).close (x * z) (y * w) := ε:δ:x:y:z:w::ε 0hxy:ε.close x yhzw:δ.close z w(ε * |z| + δ * |x| + ε * δ).close (x * z) (y * w) -- The proof is written to follow the structure of the original text, though on formalization it was revealed that the hypothesis δ ≥ 0 was unnecessary. ε:δ:x:y:z:w::ε 0hxy:ε.close x yhzw:δ.close z wa: := y - x(ε * |z| + δ * |x| + ε * δ).close (x * z) (y * w) have ha : y = x + a := ε:δ:x:y:z:w::ε 0hxy:ε.close x yhzw:δ.close z w(ε * |z| + δ * |x| + ε * δ).close (x * z) (y * w) All goals completed! 🐙 have haε: |a| ε := ε:δ:x:y:z:w::ε 0hxy:ε.close x yhzw:δ.close z w(ε * |z| + δ * |x| + ε * δ).close (x * z) (y * w) rwa [close_symm, close_iffε:δ:x:y:z:w::ε 0hxy:|y - x| εhzw:δ.close z wa: := y - xha:y = x + a|a| ε at hxy ε:δ:x:y:z:w::ε 0hxy:ε.close x yhzw:δ.close z wa: := y - xha:y = x + ahaε:|a| εb: := w - z(ε * |z| + δ * |x| + ε * δ).close (x * z) (y * w) have hb : w = z + b := ε:δ:x:y:z:w::ε 0hxy:ε.close x yhzw:δ.close z w(ε * |z| + δ * |x| + ε * δ).close (x * z) (y * w) All goals completed! 🐙 have hbδ: |b| δ := ε:δ:x:y:z:w::ε 0hxy:ε.close x yhzw:δ.close z w(ε * |z| + δ * |x| + ε * δ).close (x * z) (y * w) rwa [close_symm, close_iffε:δ:x:y:z:w::ε 0hxy:ε.close x yhzw:|w - z| δa: := y - xha:y = x + ahaε:|a| εb: := w - zhb:w = z + b|b| δ at hzw have : y*w = x * z + a * z + x * b + a * b := ε:δ:x:y:z:w::ε 0hxy:ε.close x yhzw:δ.close z w(ε * |z| + δ * |x| + ε * δ).close (x * z) (y * w) ε:δ:x:y:z:w::ε 0hxy:ε.close x yhzw:δ.close z wa: := y - xha:y = x + ahaε:|a| εb: := w - zhb:w = z + bhbδ:|b| δ(x + a) * (z + b) = x * z + a * z + x * b + a * b; All goals completed! 🐙 ε:δ:x:y:z:w::ε 0hxy:ε.close x yhzw:δ.close z wa: := y - xha:y = x + ahaε:|a| εb: := w - zhb:w = z + bhbδ:|b| δthis:y * w = x * z + a * z + x * b + a * b|y * w - x * z| ε * |z| + δ * |x| + ε * δ calc _ = |a * z + b * x + a * b| := ε:δ:x:y:z:w::ε 0hxy:ε.close x yhzw:δ.close z wa: := y - xha:y = x + ahaε:|a| εb: := w - zhb:w = z + bhbδ:|b| δthis:y * w = x * z + a * z + x * b + a * b|y * w - x * z| = |a * z + b * x + a * b| ε:δ:x:y:z:w::ε 0hxy:ε.close x yhzw:δ.close z wa: := y - xha:y = x + ahaε:|a| εb: := w - zhb:w = z + bhbδ:|b| δthis:y * w = x * z + a * z + x * b + a * b|x * z + a * z + x * b + a * b - x * z| = |a * z + b * x + a * b|; ε:δ:x:y:z:w::ε 0hxy:ε.close x yhzw:δ.close z wa: := y - xha:y = x + ahaε:|a| εb: := w - zhb:w = z + bhbδ:|b| δthis:y * w = x * z + a * z + x * b + a * bx * z + a * z + x * b + a * b - x * z = a * z + b * x + a * b; All goals completed! 🐙 _ |a * z + b * x| + |a * b| := abs_add _ _ _ |a * z| + |b * x| + |a * b| := ε:δ:x:y:z:w::ε 0hxy:ε.close x yhzw:δ.close z wa: := y - xha:y = x + ahaε:|a| εb: := w - zhb:w = z + bhbδ:|b| δthis:y * w = x * z + a * z + x * b + a * b|a * z + b * x| + |a * b| |a * z| + |b * x| + |a * b| ε:δ:x:y:z:w::ε 0hxy:ε.close x yhzw:δ.close z wa: := y - xha:y = x + ahaε:|a| εb: := w - zhb:w = z + bhbδ:|b| δthis:y * w = x * z + a * z + x * b + a * b|a * z + b * x| |a * z| + |b * x|; All goals completed! 🐙 _ = |a| * |z| + |b| * |x| + |a| * |b| := ε:δ:x:y:z:w::ε 0hxy:ε.close x yhzw:δ.close z wa: := y - xha:y = x + ahaε:|a| εb: := w - zhb:w = z + bhbδ:|b| δthis:y * w = x * z + a * z + x * b + a * b|a * z| + |b * x| + |a * b| = |a| * |z| + |b| * |x| + |a| * |b| All goals completed! 🐙 _ _ := ε:δ:x:y:z:w::ε 0hxy:ε.close x yhzw:δ.close z wa: := y - xha:y = x + ahaε:|a| εb: := w - zhb:w = z + bhbδ:|b| δthis:y * w = x * z + a * z + x * b + a * b|a| * |z| + |b| * |x| + |a| * |b| ε * |z| + δ * |x| + ε * δ All goals completed! 🐙

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

lemma pow_zero (x:) : x^0 = 1 := rfl
example : (0:)^0 = 1 := pow_zero 0

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

lemma pow_succ (x:) (n:) : x^(n+1) = x^n * x := _root_.pow_succ x n

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

theorem declaration uses 'sorry'pow_add (x:) (m n:) : x^n * x^m = x^(n+m) := x:m:n:x ^ n * x ^ m = x ^ (n + m) All goals completed! 🐙

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

theorem declaration uses 'sorry'pow_mul (x:) (m n:) : (x^n)^m = x^(n*m) := x:m:n:(x ^ n) ^ m = x ^ (n * m) All goals completed! 🐙

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

theorem declaration uses 'sorry'mul_pow (x y:) (n:) : (x*y)^n = x^n * y^n := x:y:n:(x * y) ^ n = x ^ n * y ^ n All goals completed! 🐙

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

theorem declaration uses 'sorry'pow_eq_zero (x:) (n:) : x^n = 0 x = 0 := x:n:x ^ n = 0 x = 0 All goals completed! 🐙

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

theorem declaration uses 'sorry'pow_nonneg {x:} (n:) (hx: x 0) : x^n 0 := x:n:hx:x 0x ^ n 0 All goals completed! 🐙

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

theorem declaration uses 'sorry'pow_pos {x:} (n:) (hx: x > 0) : x^n > 0 := x:n:hx:x > 0x ^ n > 0 All goals completed! 🐙

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

theorem declaration uses 'sorry'pow_ge_pow (x y:) (n:) (hxy: x y) (hy: y 0) : x^n y^n := x:y:n:hxy:x yhy:y 0x ^ n y ^ n All goals completed! 🐙

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

theorem declaration uses 'sorry'pow_gt_pow (x y:) (n:) (hxy: x > y) (hy: y 0) (hn: n > 0) : x^n > y^n := x:y:n:hxy:x > yhy:y 0hn:n > 0x ^ n > y ^ n All goals completed! 🐙

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

theorem declaration uses 'sorry'pow_abs (x:) (n:) : |x|^n = |x^n| := x:n:|x| ^ n = |x ^ n| All goals completed! 🐙

Визначення 4.3.11 (Exponentiation to a negative number). Here we use the Mathlib notion of integer exponentiation

theorem zpow_neg (x:) (n:) : x^(-(n:)) = 1/(x^n) := x:n:x ^ (-n) = 1 / x ^ n All goals completed! 🐙
example (x:): x^(-3:) = 1/(x^3) := zpow_neg x 3example (x:): x^(-3:) = 1/(x*x*x) := x:x ^ (-3) = 1 / (x * x * x) x:x * x * x = x ^ 3; All goals completed! 🐙theorem pow_eq_zpow (x:) (n:): x^(n:) = x^n := zpow_natCast x n

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

theorem declaration uses 'sorry'zpow_add (x:) (n m:) : x^n * x^m = x^(n+m) := x:n:m:x ^ n * x ^ m = x ^ (n + m) All goals completed! 🐙

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

theorem declaration uses 'sorry'zpow_mul (x:) (n m:) : (x^n)^m = x^(n*m) := x:n:m:(x ^ n) ^ m = x ^ (n * m) All goals completed! 🐙

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

theorem declaration uses 'sorry'mul_zpow (x y:) (n:) : (x*y)^n = x^n * y^n := x:y:n:(x * y) ^ n = x ^ n * y ^ n All goals completed! 🐙

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

theorem declaration uses 'sorry'zpow_pos {x:} (n:) (hx: x > 0) : x^n > 0 := x:n:hx:x > 0x ^ n > 0 All goals completed! 🐙

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

theorem declaration uses 'sorry'zpow_ge_zpow {x y:} {n:} (hxy: x y) (hy: y > 0) (hn: n > 0): x^n y^n := x:y:n:hxy:x yhy:y > 0hn:n > 0x ^ n y ^ n All goals completed! 🐙
theorem declaration uses 'sorry'zpow_ge_zpow_ofneg {x y:} {n:} (hxy: x y) (hy: y > 0) (hn: n < 0) : x^n y^n := x:y:n:hxy:x yhy:y > 0hn:n < 0x ^ n y ^ n All goals completed! 🐙

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

theorem declaration uses 'sorry'zpow_inj {x y:} {n:} (hx: x > 0) (hy : y > 0) (hn: n 0) (hxy: x^n = y^n) : x = y := x:y:n:hx:x > 0hy:y > 0hn:n 0hxy:x ^ n = y ^ nx = y All goals completed! 🐙

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

theorem declaration uses 'sorry'zpow_abs (x:) (n:) (hx: x 0) : |x|^n = |x^n| := x:n:hx:x 0|x| ^ n = |x ^ n| All goals completed! 🐙

Вправа 4.3.5

theorem declaration uses 'sorry'two_pow_geq (N:) : 2^N N := N:2 ^ N N All goals completed! 🐙