bookshelf/Bookshelf/Apostol/Chapter_I_03.lean

644 lines
22 KiB
Plaintext
Raw Normal View History

2023-05-08 19:37:02 +00:00
import Common.Real.Set
2023-05-04 22:37:54 +00:00
/-! # Apostol.Chapter_I_03
2023-04-15 15:58:10 +00:00
A Set of Axioms for the Real-Number System
-/
2023-05-04 22:37:54 +00:00
namespace Apostol.Chapter_I_03
2023-04-10 17:33:22 +00:00
#check Archimedean
#check Real.exists_isLUB
2023-05-04 22:37:54 +00:00
/-! ## The least-upper-bound axiom (completeness axiom) -/
2023-04-10 17:33:22 +00:00
/--
2023-05-04 22:37:54 +00:00
A property holds for the negation of elements in set `S` **iff** it also holds
for the elements of the negation of `S`.
2023-04-10 17:33:22 +00:00
-/
lemma set_neg_prop_iff_neg_set_prop (S : Set ) (p : → Prop)
: (∀ y, y ∈ S → p (-y)) ↔ (∀ y, y ∈ -S → p y) := by
apply Iff.intro
· intro h y hy
rw [← neg_neg y, Set.neg_mem_neg] at hy
have := h (-y) hy
simp at this
exact this
· intro h y hy
rw [← Set.neg_mem_neg] at hy
exact h (-y) hy
/--
The upper bounds of the negation of a set is the negation of the lower bounds of
the set.
-/
lemma upper_bounds_neg_eq_neg_lower_bounds (S : Set )
: upperBounds (-S) = -lowerBounds S := by
suffices (∀ x, x ∈ upperBounds (-S) ↔ x ∈ -(lowerBounds S)) from
Set.ext this
intro x
apply Iff.intro
· intro hx
unfold lowerBounds
show -x ∈ { x | ∀ ⦃a : ℝ⦄, a ∈ S → x ≤ a }
show ∀ ⦃a : ℝ⦄, a ∈ S → (-x) ≤ a
intro a ha; rw [neg_le]; revert ha a
rw [set_neg_prop_iff_neg_set_prop S (fun a => a ≤ x)]
exact hx
· intro hx
unfold upperBounds
show ∀ ⦃a : ℝ⦄, a ∈ -S → a ≤ x
rw [← set_neg_prop_iff_neg_set_prop S (fun a => a ≤ x)]
intro y hy; rw [neg_le]; revert hy y
exact hx
/--
The negation of the upper bounds of a set is the lower bounds of the negation of
the set.
-/
lemma neg_upper_bounds_eq_lower_bounds_neg (S : Set )
: -upperBounds S = lowerBounds (-S) := by
suffices (∀ x, x ∈ -upperBounds S ↔ x ∈ lowerBounds (-S)) from
Set.ext this
intro x
apply Iff.intro
· intro hx
unfold lowerBounds
show ∀ ⦃a : ℝ⦄, a ∈ -S → x ≤ a
rw [← set_neg_prop_iff_neg_set_prop S (fun a => x ≤ a)]
intro y hy; rw [le_neg]; revert hy y
exact hx
· intro hx
unfold upperBounds
show -x ∈ { x | ∀ ⦃a : ℝ⦄, a ∈ S → a ≤ x }
show ∀ ⦃a : ℝ⦄, a ∈ S → a ≤ (-x)
intro a ha; rw [le_neg]; revert ha a
rw [set_neg_prop_iff_neg_set_prop S (fun a => x ≤ a)]
exact hx
/--
2023-05-04 22:37:54 +00:00
An element `x` is the least element of the negation of a set **iff** `-x` is the
greatest element of the set.
2023-04-10 17:33:22 +00:00
-/
lemma is_least_neg_set_eq_is_greatest_set_neq (S : Set )
: IsLeast (-S) x = IsGreatest S (-x) := by
unfold IsLeast IsGreatest
rw [← neg_upper_bounds_eq_lower_bounds_neg S]
rfl
/--
2023-05-04 22:37:54 +00:00
At least with respect to ``, `x` is the least upper bound of set `-S` **iff**
`-x` is the greatest lower bound of `S`.
2023-04-10 17:33:22 +00:00
-/
theorem is_lub_neg_set_iff_is_glb_set_neg (S : Set )
: IsLUB (-S) x = IsGLB S (-x) :=
calc IsLUB (-S) x
2023-04-10 21:30:29 +00:00
_ = IsLeast (upperBounds (-S)) x := rfl
_ = IsLeast (-lowerBounds S) x := by rw [upper_bounds_neg_eq_neg_lower_bounds S]
_ = IsGreatest (lowerBounds S) (-x) := by rw [is_least_neg_set_eq_is_greatest_set_neq]
_ = IsGLB S (-x) := rfl
2023-04-10 17:33:22 +00:00
2023-05-04 22:37:54 +00:00
/-- #### Theorem I.27
2023-04-10 17:33:22 +00:00
Every nonempty set `S` that is bounded below has a greatest lower bound; that
is, there is a real number `L` such that `L = inf S`.
-/
theorem exists_isGLB (S : Set ) (hne : S.Nonempty) (hbdd : BddBelow S)
: ∃ x, IsGLB S x := by
-- First we show the negation of a nonempty set bounded below is a nonempty
-- set bounded above. In that case, we can then apply the completeness axiom
-- to argue the existence of a supremum.
have hne' : (-S).Nonempty := Set.nonempty_neg.mpr hne
have hbdd' : ∃ x, ∀ (y : ), y ∈ -S → y ≤ x := by
rw [bddBelow_def] at hbdd
let ⟨lb, lbp⟩ := hbdd
refine ⟨-lb, ?_⟩
rw [← set_neg_prop_iff_neg_set_prop S (fun y => y ≤ -lb)]
intro y hy
exact neg_le_neg (lbp y hy)
rw [←bddAbove_def] at hbdd'
-- Once we have found a supremum for `-S`, we argue the negation of this value
-- is the same as the infimum of `S`.
2023-05-04 22:37:54 +00:00
let ⟨ub, ubp⟩ := Real.exists_isLUB (-S) hne' hbdd'
2023-04-10 17:33:22 +00:00
exact ⟨-ub, (is_lub_neg_set_iff_is_glb_set_neg S).mp ubp⟩
/--
Every real should be less than or equal to the absolute value of its ceiling.
-/
lemma leq_nat_abs_ceil_self (x : ) : x ≤ Int.natAbs ⌈x⌉ := by
by_cases h : x ≥ 0
· let k : := ⌈x⌉
unfold Int.natAbs
have k' : k = ⌈x⌉ := rfl
rw [←k']
have : k ≥ 0 := by -- Hint for match below
2023-04-10 17:33:22 +00:00
rw [k', ge_iff_le]
exact Int.ceil_nonneg (ge_iff_le.mp h)
match k with
| Int.ofNat m => calc x
_ ≤ ⌈x⌉ := Int.le_ceil x
_ = Int.ofNat m := by rw [←k']
· have h' : ((Int.natAbs ⌈x⌉) : ) ≥ 0 := by simp
calc x
_ ≤ 0 := le_of_lt (lt_of_not_le h)
_ ≤ ↑(Int.natAbs ⌈x⌉) := GE.ge.le h'
2023-05-04 22:37:54 +00:00
/-! ## The Archimedean property of the real-number system -/
2023-05-04 22:37:54 +00:00
/-- #### Theorem I.29
2023-04-10 17:33:22 +00:00
For every real `x` there exists a positive integer `n` such that `n > x`.
-/
theorem exists_pnat_geq_self (x : ) : ∃ n : +, ↑n > x := by
let n : + := ⟨Int.natAbs ⌈x⌉ + 1, by simp⟩
have : x < n := calc x
2023-04-10 17:33:22 +00:00
_ ≤ Int.natAbs ⌈x⌉ := leq_nat_abs_ceil_self x
_ < ↑↑(Int.natAbs ⌈x⌉ + 1) := by simp
_ = n := rfl
exact ⟨n, this⟩
2023-04-10 17:33:22 +00:00
2023-05-04 22:37:54 +00:00
/-- #### Theorem I.30
2023-04-10 17:33:22 +00:00
If `x > 0` and if `y` is an arbitrary real number, there exists a positive
integer `n` such that `nx > y`.
This is known as the *Archimedean Property of the Reals*.
-/
theorem exists_pnat_mul_self_geq_of_pos {x y : }
: x > 0 → ∃ n : +, n * x > y := by
intro hx
let ⟨n, p⟩ := exists_pnat_geq_self (y / x)
have p' := mul_lt_mul_of_pos_right p hx
rw [div_mul, div_self (show x ≠ 0 from LT.lt.ne' hx), div_one] at p'
exact ⟨n, p'⟩
2023-05-04 22:37:54 +00:00
/-- #### Theorem I.31
2023-04-10 17:33:22 +00:00
If three real numbers `a`, `x`, and `y` satisfy the inequalities
`a ≤ x ≤ a + y / n` for every integer `n ≥ 1`, then `x = a`.
-/
theorem forall_pnat_leq_self_leq_frac_imp_eq {x y a : }
: (∀ n : +, a ≤ x ∧ x ≤ a + (y / n)) → x = a := by
intro h
match @trichotomous LT.lt _ x a with
| Or.inr (Or.inl r) => -- x = a
exact r
| Or.inl r => -- x < a
2023-04-10 17:33:22 +00:00
have z : a < a := lt_of_le_of_lt (h 1).left r
simp at z
| Or.inr (Or.inr r) => -- x > a
2023-04-10 17:33:22 +00:00
let ⟨c, hc⟩ := exists_pos_add_of_lt' r
let ⟨n, hn⟩ := @exists_pnat_mul_self_geq_of_pos c y hc.left
have hn := mul_lt_mul_of_pos_left hn $
have hp : 0 < (↑↑n : ) := by simp
show 0 < ((↑↑n)⁻¹ : ) from inv_pos.mpr hp
rw [
inv_mul_eq_div,
← mul_assoc, mul_comm (n⁻¹ : ),
← one_div,
mul_one_div
] at hn
2023-04-10 17:33:22 +00:00
simp at hn
have := calc a + y / ↑↑n
_ < a + c := add_lt_add_left hn a
2023-04-10 17:33:22 +00:00
_ = x := hc.right
_ ≤ a + y / ↑↑n := (h n).right
simp at this
/--
If three real numbers `a`, `x`, and `y` satisfy the inequalities
`a - y / n ≤ x ≤ a` for every integer `n ≥ 1`, then `x = a`.
-/
theorem forall_pnat_frac_leq_self_leq_imp_eq {x y a : }
: (∀ n : +, a - (y / n) ≤ x ∧ x ≤ a) → x = a := by
intro h
match @trichotomous LT.lt _ x a with
| Or.inr (Or.inl r) => -- x = a
exact r
| Or.inl r => -- x < a
let ⟨c, hc⟩ := exists_pos_add_of_lt' r
let ⟨n, hn⟩ := @exists_pnat_mul_self_geq_of_pos c y hc.left
have hn := mul_lt_mul_of_pos_left hn $
have hp : 0 < (↑↑n : ) := by simp
show 0 < ((↑↑n)⁻¹ : ) from inv_pos.mpr hp
rw [
inv_mul_eq_div,
← mul_assoc, mul_comm (n⁻¹ : ),
← one_div,
mul_one_div
] at hn
simp at hn
have := calc a - y / ↑↑n
_ > a - c := sub_lt_sub_left hn a
_ = x := sub_eq_of_eq_add (Eq.symm hc.right)
_ ≥ a - y / ↑↑n := (h n).left
simp at this
| Or.inr (Or.inr r) => -- x > a
have z : x < x := lt_of_le_of_lt (h 1).right r
simp at z
2023-05-04 22:37:54 +00:00
/-! ## Fundamental properties of the supremum and infimum -/
/--
Every member of a set `S` is less than or equal to some value `ub` if and only
if `ub` is an upper bound of `S`.
-/
lemma mem_upper_bounds_iff_forall_le {S : Set }
: ub ∈ upperBounds S ↔ ∀ x ∈ S, x ≤ ub := by
apply Iff.intro
· intro h _ hx
exact (h hx)
· exact id
/--
If a set `S` has a least upper bound, it follows every member of `S` is less
than or equal to that value.
-/
lemma forall_lub_imp_forall_le {S : Set }
: IsLUB S ub → ∀ x ∈ S, x ≤ ub := by
intro h
rw [← mem_upper_bounds_iff_forall_le]
exact h.left
2023-04-14 13:54:39 +00:00
/--
Any member of the upper bounds of a set must be greater than or equal to the
least member of that set.
-/
lemma mem_imp_ge_lub {x : } (h : IsLUB S s) : x ∈ upperBounds S → x ≥ s := by
intro hx
exact h.right hx
2023-05-04 22:37:54 +00:00
/-- #### Theorem I.32a
2023-04-10 17:33:22 +00:00
Let `h` be a given positive number and let `S` be a set of real numbers. If `S`
has a supremum, then for some `x` in `S` we have `x > sup S - h`.
-/
theorem sup_imp_exists_gt_sup_sub_delta {S : Set } {s h : } (hp : h > 0)
: IsLUB S s → ∃ x ∈ S, x > s - h := by
intro hb
-- Suppose all members of our set was less than `s - h`. Then `s` couldn't be
-- the *least* upper bound.
by_contra nb
suffices s - h ∈ upperBounds S by
have h' : h < h := calc h
_ ≤ 0 := (le_sub_self_iff s).mp (hb.right this)
_ < h := hp
simp at h'
rw [not_exists] at nb
have nb' : ∀ x ∈ S, x ≤ s - h := by
intro x hx
exact le_of_not_gt (not_and.mp (nb x) hx)
rwa [← mem_upper_bounds_iff_forall_le] at nb'
/--
Every member of a set `S` is greater than or equal to some value `lb` if and
only if `lb` is a lower bound of `S`.
-/
lemma mem_lower_bounds_iff_forall_ge {S : Set }
: lb ∈ lowerBounds S ↔ ∀ x ∈ S, x ≥ lb := by
apply Iff.intro
· intro h _ hx
exact (h hx)
· exact id
/--
If a set `S` has a greatest lower bound, it follows every member of `S` is
greater than or equal to that value.
-/
lemma forall_glb_imp_forall_ge {S : Set }
: IsGLB S lb → ∀ x ∈ S, x ≥ lb := by
intro h
rw [← mem_lower_bounds_iff_forall_ge]
exact h.left
2023-04-10 17:33:22 +00:00
2023-04-14 13:54:39 +00:00
/--
Any member of the lower bounds of a set must be less than or equal to the
greatest member of that set.
-/
lemma mem_imp_le_glb {x : } (h : IsGLB S s) : x ∈ lowerBounds S → x ≤ s := by
intro hx
exact h.right hx
2023-05-04 22:37:54 +00:00
/-- #### Theorem I.32b
2023-04-10 17:33:22 +00:00
Let `h` be a given positive number and let `S` be a set of real numbers. If `S`
has an infimum, then for some `x` in `S` we have `x < inf S + h`.
-/
theorem inf_imp_exists_lt_inf_add_delta {S : Set } {s h : } (hp : h > 0)
: IsGLB S s → ∃ x ∈ S, x < s + h := by
intro hb
-- Suppose all members of our set was greater than `s + h`. Then `s` couldn't
-- be the *greatest* lower bound.
by_contra nb
suffices s + h ∈ lowerBounds S by
have h' : h < h := calc h
_ ≤ 0 := (add_le_iff_nonpos_right s).mp (hb.right this)
_ < h := hp
simp at h'
rw [not_exists] at nb
have nb' : ∀ x ∈ S, x ≥ s + h := by
intro x hx
exact le_of_not_gt (not_and.mp (nb x) hx)
rwa [← mem_lower_bounds_iff_forall_ge] at nb'
2023-05-04 22:37:54 +00:00
/-- #### Theorem I.33a (Additive Property)
Given nonempty subsets `A` and `B` of ``, let `C` denote the set
`C = {a + b : a ∈ A, b ∈ B}`. If each of `A` and `B` has a supremum, then `C`
has a supremum, and `sup C = sup A + sup B`.
-/
theorem sup_minkowski_sum_eq_sup_add_sup (A B : Set ) (a b : )
(hA : A.Nonempty) (hB : B.Nonempty)
(ha : IsLUB A a) (hb : IsLUB B b)
: IsLUB (Real.minkowski_sum A B) (a + b) := by
let C := Real.minkowski_sum A B
-- First we show `a + b` is an upper bound of `C`.
have hub : a + b ∈ upperBounds C := by
rw [mem_upper_bounds_iff_forall_le]
intro x hx
have ⟨a', ⟨ha', ⟨b', ⟨hb', hxab⟩⟩⟩⟩: ∃ a ∈ A, ∃ b ∈ B, x = a + b := hx
have hs₁ : a' ≤ a := (forall_lub_imp_forall_le ha) a' ha'
have hs₂ : b' ≤ b := (forall_lub_imp_forall_le hb) b' hb'
exact calc x
_ = a' + b' := hxab
_ ≤ a + b := add_le_add hs₁ hs₂
-- Now we show `a + b` is the *least* upper bound of `C`. We know a least
-- upper bound `c` exists; show that `c = a + b`.
2023-05-04 22:37:54 +00:00
have ⟨c, hc⟩ := Real.exists_isLUB C
(Real.nonempty_minkowski_sum_iff_nonempty_add_nonempty.mpr ⟨hA, hB⟩)
⟨a + b, hub⟩
suffices (∀ n : +, c ≤ a + b ∧ a + b ≤ c + (1 / n)) by
rwa [← forall_pnat_leq_self_leq_frac_imp_eq this] at hc
intro n
apply And.intro
· exact hc.right hub
· have hd : 1 / (2 * n) > (0 : ) := by norm_num
have ⟨a', ha'⟩ := sup_imp_exists_gt_sup_sub_delta hd ha
have ⟨b', hb'⟩ := sup_imp_exists_gt_sup_sub_delta hd hb
have hab' : a + b < a' + b' + 1 / n := by
have ha'' := add_lt_add_right ha'.right (1 / (2 * ↑↑n))
have hb'' := add_lt_add_right hb'.right (1 / (2 * ↑↑n))
rw [sub_add_cancel] at ha'' hb''
have hr := add_lt_add ha'' hb''
ring_nf at hr
ring_nf
rwa [add_assoc, add_comm b' (↑↑n)⁻¹, ← add_assoc]
have hc' : a' + b' ≤ c := by
refine forall_lub_imp_forall_le hc (a' + b') ?_
show ∃ a ∈ A, ∃ b ∈ B, a' + b' = a + b
exact ⟨a', ⟨ha'.left, ⟨b', ⟨hb'.left, rfl⟩⟩⟩⟩
calc a + b
_ ≤ a' + b' + 1 / n := le_of_lt hab'
_ ≤ c + 1 / n := add_le_add_right hc' (1 / n)
2023-05-04 22:37:54 +00:00
/-- #### Theorem I.33b (Additive Property)
Given nonempty subsets `A` and `B` of ``, let `C` denote the set
`C = {a + b : a ∈ A, b ∈ B}`. If each of `A` and `B` has an infimum, then `C`
has an infimum, and `inf C = inf A + inf B`.
-/
theorem inf_minkowski_sum_eq_inf_add_inf (A B : Set )
(hA : A.Nonempty) (hB : B.Nonempty)
(ha : IsGLB A a) (hb : IsGLB B b)
: IsGLB (Real.minkowski_sum A B) (a + b) := by
let C := Real.minkowski_sum A B
-- First we show `a + b` is a lower bound of `C`.
have hlb : a + b ∈ lowerBounds C := by
rw [mem_lower_bounds_iff_forall_ge]
intro x hx
have ⟨a', ⟨ha', ⟨b', ⟨hb', hxab⟩⟩⟩⟩: ∃ a ∈ A, ∃ b ∈ B, x = a + b := hx
have hs₁ : a' ≥ a := (forall_glb_imp_forall_ge ha) a' ha'
have hs₂ : b' ≥ b := (forall_glb_imp_forall_ge hb) b' hb'
exact calc x
_ = a' + b' := hxab
_ ≥ a + b := add_le_add hs₁ hs₂
-- Now we show `a + b` is the *greatest* lower bound of `C`. We know a
-- greatest lower bound `c` exists; show that `c = a + b`.
have ⟨c, hc⟩ := exists_isGLB C
(Real.nonempty_minkowski_sum_iff_nonempty_add_nonempty.mpr ⟨hA, hB⟩)
⟨a + b, hlb⟩
suffices (∀ n : +, c - (1 / n) ≤ a + b ∧ a + b ≤ c) by
rwa [← forall_pnat_frac_leq_self_leq_imp_eq this] at hc
intro n
apply And.intro
· have hd : 1 / (2 * n) > (0 : ) := by norm_num
have ⟨a', ha'⟩ := inf_imp_exists_lt_inf_add_delta hd ha
have ⟨b', hb'⟩ := inf_imp_exists_lt_inf_add_delta hd hb
have hab' : a' + b' - 1 / n < a + b := by
have ha'' := sub_lt_sub_right ha'.right (1 / (2 * ↑↑n))
have hb'' := sub_lt_sub_right hb'.right (1 / (2 * ↑↑n))
rw [add_sub_cancel] at ha'' hb''
have hr := add_lt_add ha'' hb''
ring_nf at hr
ring_nf
rwa [← add_sub_assoc, add_sub_right_comm]
have hc' : c ≤ a' + b' := by
refine forall_glb_imp_forall_ge hc (a' + b') ?_
show ∃ a ∈ A, ∃ b ∈ B, a' + b' = a + b
exact ⟨a', ⟨ha'.left, ⟨b', ⟨hb'.left, rfl⟩⟩⟩⟩
calc c - 1 / n
_ ≤ a' + b' - 1 / n := sub_le_sub_right hc' (1 / n)
_ ≤ a + b := le_of_lt hab'
· exact hc.right hlb
2023-05-04 22:37:54 +00:00
/-- #### Theorem I.34
Given two nonempty subsets `S` and `T` of `` such that `s ≤ t` for every `s` in
`S` and every `t` in `T`. Then `S` has a supremum, and `T` has an infimum, and
they satisfy the inequality `sup S ≤ inf T`.
-/
theorem forall_mem_le_forall_mem_imp_sup_le_inf (S T : Set )
(hS : S.Nonempty) (hT : T.Nonempty)
(p : ∀ s ∈ S, ∀ t ∈ T, s ≤ t)
: ∃ (s : ), IsLUB S s ∧ ∃ (t : ), IsGLB T t ∧ s ≤ t := by
-- Show a supremum of `S` and an infimum of `T` exists (since each set bounds
2023-04-14 13:54:39 +00:00
-- above and below the other, respectively).
let ⟨s, hs⟩ := hS
let ⟨t, ht⟩ := hT
have ps : t ∈ upperBounds S := by
intro x hx
exact p x hx t ht
have pt : s ∈ lowerBounds T := by
intro x hx
exact p s hs x hx
2023-04-14 13:54:39 +00:00
have ⟨S_lub, hS_lub⟩ := Real.exists_isLUB S hS ⟨t, ps⟩
2023-05-08 19:18:12 +00:00
have ⟨T_glb, hT_glb⟩ := exists_isGLB T hT ⟨s, pt⟩
2023-04-14 13:54:39 +00:00
refine ⟨S_lub, ⟨hS_lub, ⟨T_glb, ⟨hT_glb, ?_⟩⟩⟩⟩
-- Assume `T_glb < S_lub`. Then `∃ c, T_glb + c < S_lub` which in turn implies
-- existence of some `x ∈ S` such that `T_glb < S_lub - c / 2 < x < S_lub`.
by_contra nr
rw [not_le] at nr
have ⟨c, hc⟩ := exists_pos_add_of_lt' nr
have c_div_two_gt_zero : c / 2 > 0 := by
have hr := div_lt_div_of_lt (show (0 : ) < 2 by simp) hc.left
rwa [zero_div] at hr
have T_glb_lt_S_lub_sub_c_div_two : T_glb < S_lub - c / 2 := by
have hr := congrFun (congrArg HSub.hSub hc.right) (c / 2)
rw [add_sub_assoc, sub_half c] at hr
calc T_glb
_ < T_glb + c / 2 := (lt_add_iff_pos_right T_glb).mpr c_div_two_gt_zero
_ = S_lub - c / 2 := hr
-- Since `x ∈ S`, `p` implies `x ≤ t` for all `t ∈ T`. So `x ≤ T_glb`. But the
-- above implies `T_glb < x`.
have ⟨x, hx⟩ := sup_imp_exists_gt_sup_sub_delta c_div_two_gt_zero hS_lub
have : x < x := calc x
_ ≤ T_glb := mem_imp_le_glb hT_glb (p x hx.left)
_ < S_lub - c / 2 := T_glb_lt_S_lub_sub_c_div_two
_ < x := hx.right
simp at this
2023-04-10 17:33:22 +00:00
2023-05-04 22:37:54 +00:00
/-! ## Exercises -/
/-- #### 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-08 19:18:12 +00:00
theorem exercise_1 (x y : ) (h : x < y) : ∃ z, x < z ∧ z < y := by
2023-05-04 22:37:54 +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
/-- #### Exercise 2
If `x` is an arbitrary real number, prove that there are integers `m` and `n`
such that `m < x < n`.
-/
2023-05-08 19:18:12 +00:00
theorem exercise_2 (x : ) : ∃ m n : , m < x ∧ x < n := by
2023-05-04 22:37:54 +00:00
refine ⟨x - 1, ⟨x + 1, ⟨?_, ?_⟩⟩⟩ <;> norm_num
/-- #### Exercise 3
If `x > 0`, prove that there is a positive integer `n` such that `1 / n < x`.
-/
2023-05-08 19:18:12 +00:00
theorem exercise_3 (x : ) (h : x > 0) : ∃ n : +, 1 / n < x := by
have ⟨n, hn⟩ := @exists_pnat_mul_self_geq_of_pos x 1 h
2023-05-04 22:37:54 +00:00
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
/-- #### 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-08 19:18:12 +00:00
theorem exercise_4 (x : ) : ∃! n : , n ≤ x ∧ x < n + 1 := by
2023-05-04 22:37:54 +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
/-- #### 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-08 19:18:12 +00:00
theorem exercise_5 (x : ) : ∃! n : , x ≤ n ∧ n < x + 1 := by
2023-05-04 22:37:54 +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
/-! #### 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.
###### TODO
-/
/-! #### 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.
###### TODO
-/
/-! #### Exercise 8
Is the sum or product of two irrational numbers always irrational?
###### TODO
-/
/-! #### 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.
###### TODO
-/
/-! #### 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:
(a) An integer cannot be both even and odd.
(b) Every integer is either even or odd.
(c) The sum or product of two even integers is even. What can you say about the
sum or product of two odd integers?
(d) If `n²` is even, so is `n`. If `a² = 2b²`, where `a` and `b` are integers,
then both `a` and `b` are even.
(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.
###### TODO
-/
def is_even (n : ) := ∃ m : , n = 2 * m
def is_odd (n : ) := is_even (n + 1)
/-! #### 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.]
###### TODO
-/
/-! #### 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 numbers satisfies
the Archimedean property but not the least-upper-bound property. This shows that
the Archimedean property does not imply the least-upper-bound axiom.
###### TODO
-/
end Apostol.Chapter_I_03