2023-04-15 15:58:10 +00:00
|
|
|
|
/-
|
2023-04-20 19:32:22 +00:00
|
|
|
|
Exercises I 3.12
|
2023-04-15 15:58:10 +00:00
|
|
|
|
|
|
|
|
|
A Set of Axioms for the Real-Number System
|
|
|
|
|
-/
|
2023-04-21 13:17:21 +00:00
|
|
|
|
import Mathlib.Algebra.Order.Floor
|
|
|
|
|
import Mathlib.Data.PNat.Basic
|
|
|
|
|
import Mathlib.Data.Real.Basic
|
|
|
|
|
import Mathlib.Data.Real.Sqrt
|
|
|
|
|
import Mathlib.Tactic.LibrarySearch
|
|
|
|
|
|
|
|
|
|
import Bookshelf.Real.Rational
|
2023-04-26 21:44:52 +00:00
|
|
|
|
import OneVariableCalculus.Apostol.Chapter_I_3
|
2023-04-15 15:58:10 +00:00
|
|
|
|
|
|
|
|
|
-- ========================================
|
|
|
|
|
-- Exercise 1
|
|
|
|
|
--
|
|
|
|
|
-- If `x` and `y` are arbitrary real numbers with `x < y`, prove that there is
|
|
|
|
|
-- at least one real `z` satisfying `x < z < y`.
|
|
|
|
|
-- ========================================
|
|
|
|
|
|
2023-05-03 19:09:41 +00:00
|
|
|
|
theorem exercise1 (x y : ℝ) (h : x < y) : ∃ z, x < z ∧ z < y := by
|
2023-04-21 13:17:21 +00:00
|
|
|
|
have ⟨z, hz⟩ := exists_pos_add_of_lt' h
|
|
|
|
|
refine ⟨x + z / 2, ⟨?_, ?_⟩⟩
|
|
|
|
|
· have hz' : z / 2 > 0 := by
|
|
|
|
|
have hr := div_lt_div_of_lt (show (0 : ℝ) < 2 by simp) hz.left
|
|
|
|
|
rwa [zero_div] at hr
|
|
|
|
|
exact (lt_add_iff_pos_right x).mpr hz'
|
|
|
|
|
· have hz' : z / 2 < z := div_lt_self hz.left (show 1 < 2 by norm_num)
|
|
|
|
|
calc x + z / 2
|
|
|
|
|
_ < x + z := (add_lt_add_iff_left x).mpr hz'
|
|
|
|
|
_ = y := hz.right
|
2023-04-15 15:58:10 +00:00
|
|
|
|
|
|
|
|
|
-- ========================================
|
|
|
|
|
-- Exercise 2
|
|
|
|
|
--
|
|
|
|
|
-- If `x` is an arbitrary real number, prove that there are integers `m` and `n`
|
|
|
|
|
-- such that `m < x < n`.
|
|
|
|
|
-- ========================================
|
|
|
|
|
|
2023-05-03 19:09:41 +00:00
|
|
|
|
theorem exercise2 (x : ℝ) : ∃ m n : ℝ, m < x ∧ x < n := by
|
2023-04-21 13:17:21 +00:00
|
|
|
|
refine ⟨x - 1, ⟨x + 1, ⟨?_, ?_⟩⟩⟩ <;> norm_num
|
2023-04-15 15:58:10 +00:00
|
|
|
|
|
|
|
|
|
-- ========================================
|
|
|
|
|
-- Exercise 3
|
|
|
|
|
--
|
|
|
|
|
-- If `x > 0`, prove that there is a positive integer `n` such that `1 / n < x`.
|
|
|
|
|
-- ========================================
|
|
|
|
|
|
2023-05-03 19:09:41 +00:00
|
|
|
|
theorem exercise3 (x : ℝ) (h : x > 0) : ∃ n : ℕ+, 1 / n < x := by
|
2023-04-21 13:17:21 +00:00
|
|
|
|
have ⟨n, hn⟩ := @Real.exists_pnat_mul_self_geq_of_pos x 1 h
|
|
|
|
|
refine ⟨n, ?_⟩
|
|
|
|
|
have hr := mul_lt_mul_of_pos_right hn (show 0 < 1 / ↑↑n by norm_num)
|
|
|
|
|
conv at hr => arg 2; rw [mul_comm, ← mul_assoc]; simp
|
|
|
|
|
rwa [one_mul] at hr
|
2023-04-15 15:58:10 +00:00
|
|
|
|
|
|
|
|
|
-- ========================================
|
|
|
|
|
-- Exercise 4
|
|
|
|
|
--
|
|
|
|
|
-- If `x` is an arbitrary real number, prove that there is exactly one integer
|
|
|
|
|
-- `n` which satisfies the inequalities `n ≤ x < n + 1`. This `n` is called the
|
|
|
|
|
-- greatest integer in `x` and is denoted by `⌊x⌋`. For example, `⌊5⌋ = 5`,
|
|
|
|
|
-- `⌊5 / 2⌋ = 2`, `⌊-8/3⌋ = -3`.
|
|
|
|
|
-- ========================================
|
|
|
|
|
|
2023-05-03 19:09:41 +00:00
|
|
|
|
theorem exercise4 (x : ℝ) : ∃! n : ℤ, n ≤ x ∧ x < n + 1 := by
|
2023-04-21 13:17:21 +00:00
|
|
|
|
let n := Int.floor x
|
|
|
|
|
refine ⟨n, ⟨?_, ?_⟩⟩
|
|
|
|
|
· exact ⟨Int.floor_le x, Int.lt_floor_add_one x⟩
|
|
|
|
|
· intro y hy
|
|
|
|
|
rw [← Int.floor_eq_iff] at hy
|
|
|
|
|
exact Eq.symm hy
|
2023-04-15 15:58:10 +00:00
|
|
|
|
|
|
|
|
|
-- ========================================
|
|
|
|
|
-- Exercise 5
|
|
|
|
|
--
|
|
|
|
|
-- If `x` is an arbitrary real number, prove that there is exactly one integer
|
|
|
|
|
-- `n` which satisfies `x ≤ n < x + 1`.
|
|
|
|
|
-- ========================================
|
|
|
|
|
|
2023-05-03 19:09:41 +00:00
|
|
|
|
theorem exercise5 (x : ℝ) : ∃! n : ℤ, x ≤ n ∧ n < x + 1 := by
|
2023-04-21 13:17:21 +00:00
|
|
|
|
let n := Int.ceil x
|
|
|
|
|
refine ⟨n, ⟨?_, ?_⟩⟩
|
|
|
|
|
· exact ⟨Int.le_ceil x, Int.ceil_lt_add_one x⟩
|
|
|
|
|
· simp only
|
|
|
|
|
intro y hy
|
|
|
|
|
suffices y - 1 < x ∧ x ≤ y by
|
|
|
|
|
rw [← Int.ceil_eq_iff] at this
|
|
|
|
|
exact Eq.symm this
|
|
|
|
|
apply And.intro
|
|
|
|
|
· have := (sub_lt_sub_iff_right 1).mpr hy.right
|
|
|
|
|
rwa [add_sub_cancel] at this
|
|
|
|
|
· exact hy.left
|
2023-04-15 15:58:10 +00:00
|
|
|
|
|
|
|
|
|
-- ========================================
|
|
|
|
|
-- Exercise 6
|
|
|
|
|
--
|
|
|
|
|
-- If `x` and `y` are arbitrary real numbers, `x < y`, prove that there exists
|
|
|
|
|
-- at least one rational number `r` satisfying `x < r < y`, and hence infinitely
|
|
|
|
|
-- many. This property is often described by saying that the rational numbers
|
|
|
|
|
-- are *dense* in the real-number system.
|
|
|
|
|
-- ========================================
|
|
|
|
|
|
2023-05-03 19:09:41 +00:00
|
|
|
|
-- # TODO
|
2023-04-15 15:58:10 +00:00
|
|
|
|
|
|
|
|
|
-- ========================================
|
|
|
|
|
-- Exercise 7
|
|
|
|
|
--
|
|
|
|
|
-- If `x` is rational, `x ≠ 0`, and `y` irrational, prove that `x + y`, `x - y`,
|
|
|
|
|
-- `xy`, `x / y`, and `y / x` are all irrational.
|
|
|
|
|
-- ========================================
|
|
|
|
|
|
2023-05-03 19:09:41 +00:00
|
|
|
|
-- # TODO
|
2023-04-15 15:58:10 +00:00
|
|
|
|
|
|
|
|
|
-- ========================================
|
|
|
|
|
-- Exercise 8
|
|
|
|
|
--
|
|
|
|
|
-- Is the sum or product of two irrational numbers always irrational?
|
|
|
|
|
-- ========================================
|
|
|
|
|
|
2023-05-03 19:09:41 +00:00
|
|
|
|
-- # TODO
|
2023-04-15 15:58:10 +00:00
|
|
|
|
|
|
|
|
|
-- ========================================
|
|
|
|
|
-- Exercise 9
|
|
|
|
|
--
|
|
|
|
|
-- If `x` and `y` are arbitrary real numbers, `x < y`, prove that there exists
|
|
|
|
|
-- at least one irrational number `z` satisfying `x < z < y`, and hence
|
|
|
|
|
-- infinitely many.
|
|
|
|
|
-- ========================================
|
|
|
|
|
|
2023-05-03 19:09:41 +00:00
|
|
|
|
-- # TODO
|
2023-04-15 15:58:10 +00:00
|
|
|
|
|
|
|
|
|
-- ========================================
|
|
|
|
|
-- Exercise 10
|
|
|
|
|
--
|
|
|
|
|
-- An integer `n` is called *even* if `n = 2m` for some integer `m`, and *odd*
|
|
|
|
|
-- if `n + 1` is even. Prove the following statements:
|
|
|
|
|
--
|
2023-04-21 13:17:21 +00:00
|
|
|
|
-- (e) Every rational number can be expressed in the form `a / b`, where `a` and
|
|
|
|
|
-- `b` are integers, at least one of which is odd.
|
|
|
|
|
-- ========================================
|
|
|
|
|
|
|
|
|
|
def is_even (n : ℤ) := ∃ m : ℤ, n = 2 * m
|
|
|
|
|
|
|
|
|
|
def is_odd (n : ℤ) := is_even (n + 1)
|
|
|
|
|
|
|
|
|
|
-- ----------------------------------------
|
2023-04-15 15:58:10 +00:00
|
|
|
|
-- (a) An integer cannot be both even and odd.
|
2023-04-21 13:17:21 +00:00
|
|
|
|
-- ----------------------------------------
|
|
|
|
|
|
2023-05-03 19:09:41 +00:00
|
|
|
|
-- # TODO
|
2023-04-21 13:17:21 +00:00
|
|
|
|
|
|
|
|
|
-- ----------------------------------------
|
2023-04-15 15:58:10 +00:00
|
|
|
|
-- (b) Every integer is either even or odd.
|
2023-04-21 13:17:21 +00:00
|
|
|
|
-- ----------------------------------------
|
|
|
|
|
|
2023-05-03 19:09:41 +00:00
|
|
|
|
-- # TODO
|
2023-04-21 13:17:21 +00:00
|
|
|
|
|
|
|
|
|
-- ----------------------------------------
|
2023-04-15 15:58:10 +00:00
|
|
|
|
-- (c) The sum or product of two even integers is even. What can you say about
|
|
|
|
|
-- the sum or product of two odd integers?
|
2023-04-21 13:17:21 +00:00
|
|
|
|
-- ----------------------------------------
|
|
|
|
|
|
2023-05-03 19:09:41 +00:00
|
|
|
|
-- # TODO
|
2023-04-21 13:17:21 +00:00
|
|
|
|
|
|
|
|
|
-- ----------------------------------------
|
2023-04-15 15:58:10 +00:00
|
|
|
|
-- (d) If `n²` is even, so is `n`. If `a² = 2b²`, where `a` and `b` are
|
|
|
|
|
-- integers, then both `a` and `b` are even.
|
2023-04-21 13:17:21 +00:00
|
|
|
|
-- ----------------------------------------
|
|
|
|
|
|
2023-05-03 19:09:41 +00:00
|
|
|
|
-- # TODO
|
2023-04-15 15:58:10 +00:00
|
|
|
|
|
|
|
|
|
-- ========================================
|
|
|
|
|
-- Exercise 11
|
|
|
|
|
--
|
|
|
|
|
-- Prove that there is no rational number whose square is `2`.
|
|
|
|
|
--
|
|
|
|
|
-- [Hint: Argue by contradiction. Assume `(a / b)² = 2`, where `a` and `b` are
|
|
|
|
|
-- integers, at least one of which is odd. Use parts of Exercise 10 to deduce a
|
|
|
|
|
-- contradiction.]
|
|
|
|
|
-- ========================================
|
|
|
|
|
|
2023-05-03 19:09:41 +00:00
|
|
|
|
-- # TODO
|
2023-04-15 15:58:10 +00:00
|
|
|
|
|
|
|
|
|
-- ========================================
|
|
|
|
|
-- Exercise 12
|
|
|
|
|
--
|
|
|
|
|
-- The Archimedean property of the real-number system was deduced as a
|
|
|
|
|
-- consequence of the least-upper-bound axiom. Prove that the set of rational
|
2023-04-21 13:17:21 +00:00
|
|
|
|
-- numbers satisfies the Archimedean property but not the least-upper-bound
|
2023-04-15 15:58:10 +00:00
|
|
|
|
-- property. This shows that the Archimedean property does not imply the
|
|
|
|
|
-- least-upper-bound axiom.
|
|
|
|
|
-- ========================================
|
|
|
|
|
|
2023-05-03 19:09:41 +00:00
|
|
|
|
-- # TODO
|