Absolute value and exponentiation
Analysis I, Section 4.3: Absolute value and exponentiation
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.
Tips from past users
Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.
-
(Add tip here)
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_3Definition 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: 0 < x) : abs x = x := x:ℚhx:0 < x⊢ abs x = x All goals completed! 🐙Definition 4.3.1 (Absolute value)
theorem abs_of_neg {x: ℚ} (hx: x < 0) : abs x = -x := x:ℚhx:x < 0⊢ abs x = -x All goals completed! 🐙(Not from textbook) This definition of absolute value agrees with the Mathlib one. Henceforth we use the Mathlib absolute value.
theorem abs_eq_abs (x: ℚ) : abs x = |x| := x:ℚ⊢ abs x = |x|
All goals completed! 🐙abbrev dist (x y : ℚ) := |x - y|Definition 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| := rflProposition 4.3.3(a) / Exercise 4.3.1
theorem abs_nonneg (x: ℚ) : |x| ≥ 0 := x:ℚ⊢ |x| ≥ 0 All goals completed! 🐙Proposition 4.3.3(a) / Exercise 4.3.1
theorem abs_eq_zero_iff (x: ℚ) : |x| = 0 ↔ x = 0 := x:ℚ⊢ |x| = 0 ↔ x = 0 All goals completed! 🐙Proposition 4.3.3(b) / Exercise 4.3.1
theorem abs_add (x y:ℚ) : |x + y| ≤ |x| + |y| := x:ℚy:ℚ⊢ |x + y| ≤ |x| + |y| All goals completed! 🐙Proposition 4.3.3(c) / Exercise 4.3.1
theorem abs_le_iff (x y:ℚ) : -y ≤ x ∧ x ≤ y ↔ |x| ≤ y := x:ℚy:ℚ⊢ -y ≤ x ∧ x ≤ y ↔ |x| ≤ y All goals completed! 🐙Proposition 4.3.3(c) / Exercise 4.3.1
theorem le_abs (x:ℚ) : -|x| ≤ x ∧ x ≤ |x| := x:ℚ⊢ -|x| ≤ x ∧ x ≤ |x| All goals completed! 🐙Proposition 4.3.3(d) / Exercise 4.3.1
theorem abs_mul (x y:ℚ) : |x * y| = |x| * |y| := x:ℚy:ℚ⊢ |x * y| = |x| * |y| All goals completed! 🐙Proposition 4.3.3(d) / Exercise 4.3.1
theorem abs_neg (x:ℚ) : |-x| = |x| := x:ℚ⊢ |(-x)| = |x| All goals completed! 🐙Proposition 4.3.3(e) / Exercise 4.3.1
theorem dist_nonneg (x y:ℚ) : dist x y ≥ 0 := x:ℚy:ℚ⊢ dist x y ≥ 0 All goals completed! 🐙Proposition 4.3.3(e) / Exercise 4.3.1
theorem dist_eq_zero_iff (x y:ℚ) : dist x y = 0 ↔ x = y := x:ℚy:ℚ⊢ dist x y = 0 ↔ x = y
All goals completed! 🐙Proposition 4.3.3(f) / Exercise 4.3.1
theorem dist_symm (x y:ℚ) : dist x y = dist y x := x:ℚy:ℚ⊢ dist x y = dist y x All goals completed! 🐙Proposition 4.3.3(f) / Exercise 4.3.1
theorem 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! 🐙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 close_iff (ε x y:ℚ): ε.Close x y ↔ |x - y| ≤ ε := ε:ℚx:ℚy:ℚ⊢ ε.Close x y ↔ |x - y| ≤ ε All goals completed! 🐙Examples 4.3.6
example : (0.1:ℚ).Close (0.99:ℚ) (1.01:ℚ) := ⊢ Rat.Close 0.1 0.99 1.01 All goals completed! 🐙Examples 4.3.6
example : ¬ (0.01:ℚ).Close (0.99:ℚ) (1.01:ℚ) := ⊢ ¬Rat.Close 1e-2 0.99 1.01 All goals completed! 🐙Examples 4.3.6
example (ε : ℚ) (hε : ε > 0) : ε.Close 2 2 := ε:ℚhε:ε > 0⊢ ε.Close 2 2 All goals completed! 🐙theorem close_refl (x:ℚ) : (0:ℚ).Close x x := x:ℚ⊢ Rat.Close 0 x x All goals completed! 🐙Proposition 4.3.7(a) / Exercise 4.3.2
theorem eq_if_close (x y:ℚ) : x = y ↔ ∀ ε:ℚ, ε > 0 → ε.Close x y := x:ℚy:ℚ⊢ x = y ↔ ∀ ε > 0, ε.Close x y All goals completed! 🐙Proposition 4.3.7(b) / Exercise 4.3.2
theorem close_symm (ε x y:ℚ) : ε.Close x y ↔ ε.Close y x := ε:ℚx:ℚy:ℚ⊢ ε.Close x y ↔ ε.Close y x All goals completed! 🐙Proposition 4.3.7(c) / Exercise 4.3.2
theorem close_trans {ε δ x y z:ℚ} (hxy: ε.Close x y) (hyz: δ.Close y z) :
(ε + δ).Close x z := ε:ℚδ:ℚx:ℚy:ℚz:ℚhxy:ε.Close x yhyz:δ.Close y z⊢ (ε + δ).Close x z All goals completed! 🐙Proposition 4.3.7(d) / Exercise 4.3.2
theorem 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! 🐙Proposition 4.3.7(d) / Exercise 4.3.2
theorem 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! 🐙Proposition 4.3.7(e) / Exercise 4.3.2, slightly strengthened
theorem close_mono {ε ε' x y:ℚ} (hxy: ε.Close x y) (hε: ε' ≥ ε) :
ε'.Close x y := ε:ℚε':ℚx:ℚy:ℚhxy:ε.Close x yhε:ε' ≥ ε⊢ ε'.Close x y All goals completed! 🐙Proposition 4.3.7(f) / Exercise 4.3.2
theorem 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 := ε:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhxz:ε.Close x zhbetween:y ≤ w ∧ w ≤ z ∨ z ≤ w ∧ w ≤ y⊢ ε.Close x w All goals completed! 🐙Proposition 4.3.7(g) / Exercise 4.3.2
theorem close_mul_right {ε x y z:ℚ} (hxy: ε.Close x y) :
(ε*|z|).Close (x * z) (y * z) := ε:ℚx:ℚy:ℚz:ℚhxy:ε.Close x y⊢ (ε * |z|).Close (x * z) (y * z) All goals completed! 🐙Proposition 4.3.7(h) / Exercise 4.3.2
theorem close_mul_mul {ε δ x y z w:ℚ} (hxy: ε.Close x y) (hzw: δ.Close z w) :
(ε*|z|+δ*|x|+ε*δ).Close (x * z) (y * w) := ε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.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
-- non-negativity of ε and δ are implied and don't need to be provided as
-- explicit hypotheses.
ε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z whε:_fvar.6597 ≥ 0 := le_trans (abs_nonneg ?_mvar.6709) _fvar.6603⊢ (ε * |z| + δ * |x| + ε * δ).Close (x * z) (y * w)
ε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z whε:_fvar.6597 ≥ 0 := le_trans (abs_nonneg ?_mvar.6709) _fvar.6603a:ℚ := _fvar.6600 - _fvar.6599⊢ (ε * |z| + δ * |x| + ε * δ).Close (x * z) (y * w)
have ha : y = x + a := ε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z w⊢ (ε * |z| + δ * |x| + ε * δ).Close (x * z) (y * w) All goals completed! 🐙
have haε: |a| ≤ ε := ε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z w⊢ (ε * |z| + δ * |x| + ε * δ).Close (x * z) (y * w) rwa [close_symm, close_iffε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:|y - x| ≤ εhzw:δ.Close z whε:ε ≥ 0a:ℚ := _fvar.6600 - _fvar.6599ha:y = x + a⊢ |a| ≤ ε at hxy
ε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z whε:_fvar.6597 ≥ 0 := le_trans (abs_nonneg ?_mvar.6709) _fvar.6603a:ℚ := _fvar.6600 - _fvar.6599ha:_fvar.6600 = _fvar.6599 + _fvar.6764 := ?_mvar.6923haε:|_fvar.6764| ≤ _fvar.6597 := ?_mvar.8623b:ℚ := _fvar.6602 - _fvar.6601⊢ (ε * |z| + δ * |x| + ε * δ).Close (x * z) (y * w)
have hb : w = z + b := ε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z w⊢ (ε * |z| + δ * |x| + ε * δ).Close (x * z) (y * w) All goals completed! 🐙
have hbδ: |b| ≤ δ := ε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z w⊢ (ε * |z| + δ * |x| + ε * δ).Close (x * z) (y * w) rwa [close_symm, close_iffε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:|w - z| ≤ δhε:ε ≥ 0a:ℚ := _fvar.6600 - _fvar.6599ha:y = x + ahaε:|a| ≤ εb:ℚ := _fvar.6602 - _fvar.6601hb:w = z + b⊢ |b| ≤ δ at hzw
have : y*w = x * z + a * z + x * b + a * b := ε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z w⊢ (ε * |z| + δ * |x| + ε * δ).Close (x * z) (y * w) All goals completed! 🐙
ε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z whε:_fvar.6597 ≥ 0 := le_trans (abs_nonneg ?_mvar.6709) _fvar.6603a:ℚ := _fvar.6600 - _fvar.6599ha:_fvar.6600 = _fvar.6599 + _fvar.6764 := ?_mvar.6923haε:|_fvar.6764| ≤ _fvar.6597 := ?_mvar.8623b:ℚ := _fvar.6602 - _fvar.6601hb:_fvar.6602 = _fvar.6601 + _fvar.10741 := ?_mvar.10927hbδ:|_fvar.10741| ≤ _fvar.6598 := ?_mvar.12659this:_fvar.6600 * _fvar.6602 =
_fvar.6599 * _fvar.6601 + _fvar.6764 * _fvar.6601 + _fvar.6599 * _fvar.10741 + _fvar.6764 * _fvar.10741 :=
?_mvar.14162⊢ |y * w - x * z| ≤ ε * |z| + δ * |x| + ε * δ
calc
_ = |a * z + b * x + a * b| := ε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z whε:_fvar.6597 ≥ 0 := le_trans (abs_nonneg (_fvar.6599 - _fvar.6600)) _fvar.6603a:ℚ := _fvar.6600 - _fvar.6599ha:_fvar.6600 = _fvar.6599 + _fvar.6764 := close_mul_mul._proof_1haε:|_fvar.6764| ≤ _fvar.6597 :=
Eq.mp (congrArg (fun _a => _a) (propext (close_iff _fvar.6597 _fvar.6600 _fvar.6599)))
(Eq.mp (congrArg (fun _a => _a) (propext (close_symm _fvar.6597 _fvar.6599 _fvar.6600))) _fvar.6603)b:ℚ := _fvar.6602 - _fvar.6601hb:_fvar.6602 = _fvar.6601 + _fvar.10741 := close_mul_mul._proof_2hbδ:|_fvar.10741| ≤ _fvar.6598 :=
Eq.mp (congrArg (fun _a => _a) (propext (close_iff _fvar.6598 _fvar.6602 _fvar.6601)))
(Eq.mp (congrArg (fun _a => _a) (propext (close_symm _fvar.6598 _fvar.6601 _fvar.6602))) _fvar.6604)this:_fvar.6600 * _fvar.6602 =
_fvar.6599 * _fvar.6601 + _fvar.6764 * _fvar.6601 + _fvar.6599 * _fvar.10741 + _fvar.6764 * _fvar.10741 :=
close_mul_mul._proof_3⊢ |y * w - 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:ℚhxy:ε.Close x yhzw:δ.Close z whε:_fvar.6597 ≥ 0 := le_trans (abs_nonneg (_fvar.6599 - _fvar.6600)) _fvar.6603a:ℚ := _fvar.6600 - _fvar.6599ha:_fvar.6600 = _fvar.6599 + _fvar.6764 := close_mul_mul._proof_1haε:|_fvar.6764| ≤ _fvar.6597 :=
Eq.mp (congrArg (fun _a => _a) (propext (close_iff _fvar.6597 _fvar.6600 _fvar.6599)))
(Eq.mp (congrArg (fun _a => _a) (propext (close_symm _fvar.6597 _fvar.6599 _fvar.6600))) _fvar.6603)b:ℚ := _fvar.6602 - _fvar.6601hb:_fvar.6602 = _fvar.6601 + _fvar.10741 := close_mul_mul._proof_2hbδ:|_fvar.10741| ≤ _fvar.6598 :=
Eq.mp (congrArg (fun _a => _a) (propext (close_iff _fvar.6598 _fvar.6602 _fvar.6601)))
(Eq.mp (congrArg (fun _a => _a) (propext (close_symm _fvar.6598 _fvar.6601 _fvar.6602))) _fvar.6604)this:_fvar.6600 * _fvar.6602 =
_fvar.6599 * _fvar.6601 + _fvar.6764 * _fvar.6601 + _fvar.6599 * _fvar.10741 + _fvar.6764 * _fvar.10741 :=
close_mul_mul._proof_3⊢ |a * z + b * x| + |a * b| ≤ |a * z| + |b * x| + |a * b| All goals completed! 🐙
_ = |a| * |z| + |b| * |x| + |a| * |b| := ε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z whε:_fvar.6597 ≥ 0 := le_trans (abs_nonneg (_fvar.6599 - _fvar.6600)) _fvar.6603a:ℚ := _fvar.6600 - _fvar.6599ha:_fvar.6600 = _fvar.6599 + _fvar.6764 := close_mul_mul._proof_1haε:|_fvar.6764| ≤ _fvar.6597 :=
Eq.mp (congrArg (fun _a => _a) (propext (close_iff _fvar.6597 _fvar.6600 _fvar.6599)))
(Eq.mp (congrArg (fun _a => _a) (propext (close_symm _fvar.6597 _fvar.6599 _fvar.6600))) _fvar.6603)b:ℚ := _fvar.6602 - _fvar.6601hb:_fvar.6602 = _fvar.6601 + _fvar.10741 := close_mul_mul._proof_2hbδ:|_fvar.10741| ≤ _fvar.6598 :=
Eq.mp (congrArg (fun _a => _a) (propext (close_iff _fvar.6598 _fvar.6602 _fvar.6601)))
(Eq.mp (congrArg (fun _a => _a) (propext (close_symm _fvar.6598 _fvar.6601 _fvar.6602))) _fvar.6604)this:_fvar.6600 * _fvar.6602 =
_fvar.6599 * _fvar.6601 + _fvar.6764 * _fvar.6601 + _fvar.6599 * _fvar.10741 + _fvar.6764 * _fvar.10741 :=
close_mul_mul._proof_3⊢ |a * z| + |b * x| + |a * b| = |a| * |z| + |b| * |x| + |a| * |b| All goals completed! 🐙
_ ≤ _ := ε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z whε:_fvar.6597 ≥ 0 := le_trans (abs_nonneg (_fvar.6599 - _fvar.6600)) _fvar.6603a:ℚ := _fvar.6600 - _fvar.6599ha:_fvar.6600 = _fvar.6599 + _fvar.6764 := close_mul_mul._proof_1haε:|_fvar.6764| ≤ _fvar.6597 :=
Eq.mp (congrArg (fun _a => _a) (propext (close_iff _fvar.6597 _fvar.6600 _fvar.6599)))
(Eq.mp (congrArg (fun _a => _a) (propext (close_symm _fvar.6597 _fvar.6599 _fvar.6600))) _fvar.6603)b:ℚ := _fvar.6602 - _fvar.6601hb:_fvar.6602 = _fvar.6601 + _fvar.10741 := close_mul_mul._proof_2hbδ:|_fvar.10741| ≤ _fvar.6598 :=
Eq.mp (congrArg (fun _a => _a) (propext (close_iff _fvar.6598 _fvar.6602 _fvar.6601)))
(Eq.mp (congrArg (fun _a => _a) (propext (close_symm _fvar.6598 _fvar.6601 _fvar.6602))) _fvar.6604)this:_fvar.6600 * _fvar.6602 =
_fvar.6599 * _fvar.6601 + _fvar.6764 * _fvar.6601 + _fvar.6599 * _fvar.10741 + _fvar.6764 * _fvar.10741 :=
close_mul_mul._proof_3⊢ |a| * |z| + |b| * |x| + |a| * |b| ≤ ε * |z| + δ * |x| + ε * δ All goals completed! 🐙This variant of Proposition 4.3.7(h) was not in the textbook, but can be useful in some later exercises.
theorem close_mul_mul' {ε δ x y z w:ℚ} (hxy: ε.Close x y) (hzw: δ.Close z w) :
(ε*|z|+δ*|y|).Close (x * z) (y * w) := ε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z w⊢ (ε * |z| + δ * |y|).Close (x * z) (y * w)
All goals completed! 🐙Definition 4.3.9 (exponentiation). Here we use the Mathlib definition.
lemma pow_zero (x:ℚ) : x^0 = 1 := rflexample : (0:ℚ)^0 = 1 := pow_zero 0Definition 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 nProposition 4.3.10(a) (Properties of exponentiation, I) / Exercise 4.3.3
theorem 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! 🐙Proposition 4.3.10(a) (Properties of exponentiation, I) / Exercise 4.3.3
theorem pow_mul (x:ℚ) (m n:ℕ) : (x^n)^m = x^(n*m) := x:ℚm:ℕn:ℕ⊢ (x ^ n) ^ m = x ^ (n * m) All goals completed! 🐙Proposition 4.3.10(a) (Properties of exponentiation, I) / Exercise 4.3.3
theorem 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! 🐙Proposition 4.3.10(b) (Properties of exponentiation, I) / Exercise 4.3.3
theorem pow_eq_zero (x:ℚ) (n:ℕ) (hn : 0 < n) : x^n = 0 ↔ x = 0 := x:ℚn:ℕhn:0 < n⊢ x ^ n = 0 ↔ x = 0 All goals completed! 🐙Proposition 4.3.10(c) (Properties of exponentiation, I) / Exercise 4.3.3
theorem pow_nonneg {x:ℚ} (n:ℕ) (hx: x ≥ 0) : x^n ≥ 0 := x:ℚn:ℕhx:x ≥ 0⊢ x ^ n ≥ 0 All goals completed! 🐙Proposition 4.3.10(c) (Properties of exponentiation, I) / Exercise 4.3.3
theorem pow_pos {x:ℚ} (n:ℕ) (hx: x > 0) : x^n > 0 := x:ℚn:ℕhx:x > 0⊢ x ^ n > 0 All goals completed! 🐙Proposition 4.3.10(c) (Properties of exponentiation, I) / Exercise 4.3.3
theorem pow_ge_pow (x y:ℚ) (n:ℕ) (hxy: x ≥ y) (hy: y ≥ 0) : x^n ≥ y^n := x:ℚy:ℚn:ℕhxy:x ≥ yhy:y ≥ 0⊢ x ^ n ≥ y ^ n All goals completed! 🐙Proposition 4.3.10(c) (Properties of exponentiation, I) / Exercise 4.3.3
theorem 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 > 0⊢ x ^ n > y ^ n All goals completed! 🐙Proposition 4.3.10(d) (Properties of exponentiation, I) / Exercise 4.3.3
theorem pow_abs (x:ℚ) (n:ℕ) : |x|^n = |x^n| := x:ℚn:ℕ⊢ |x| ^ n = |x ^ n| All goals completed! 🐙Definition 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 nProposition 4.3.12(a) (Properties of exponentiation, II) / Exercise 4.3.4
theorem zpow_add (x:ℚ) (n m:ℤ) (hx: x ≠ 0): x^n * x^m = x^(n+m) := x:ℚn:ℤm:ℤhx:x ≠ 0⊢ x ^ n * x ^ m = x ^ (n + m) All goals completed! 🐙Proposition 4.3.12(a) (Properties of exponentiation, II) / Exercise 4.3.4
theorem zpow_mul (x:ℚ) (n m:ℤ) : (x^n)^m = x^(n*m) := x:ℚn:ℤm:ℤ⊢ (x ^ n) ^ m = x ^ (n * m) All goals completed! 🐙Proposition 4.3.12(a) (Properties of exponentiation, II) / Exercise 4.3.4
theorem 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! 🐙Proposition 4.3.12(b) (Properties of exponentiation, II) / Exercise 4.3.4
theorem zpow_pos {x:ℚ} (n:ℤ) (hx: x > 0) : x^n > 0 := x:ℚn:ℤhx:x > 0⊢ x ^ n > 0 All goals completed! 🐙Proposition 4.3.12(b) (Properties of exponentiation, II) / Exercise 4.3.4
theorem 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 > 0⊢ x ^ n ≥ y ^ n All goals completed! 🐙theorem 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 < 0⊢ x ^ n ≤ y ^ n
All goals completed! 🐙Proposition 4.3.12(c) (Properties of exponentiation, II) / Exercise 4.3.4
theorem 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 ^ n⊢ x = y
All goals completed! 🐙Proposition 4.3.12(d) (Properties of exponentiation, II) / Exercise 4.3.4
theorem zpow_abs (x:ℚ) (n:ℤ) : |x|^n = |x^n| := x:ℚn:ℤ⊢ |x| ^ n = |x ^ n| All goals completed! 🐙