From a8f12f2ec0b1514f4935e4c6fec1ead76c3920a1 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Wed, 3 May 2023 13:09:41 -0600 Subject: [PATCH] Clean up unused/not to be proven. --- .../Apostol/Exercises_1_7.lean | 98 ------------------- .../Apostol/Exercises_I_3_12.lean | 71 +++----------- 2 files changed, 15 insertions(+), 154 deletions(-) delete mode 100644 OneVariableCalculus/Apostol/Exercises_1_7.lean diff --git a/OneVariableCalculus/Apostol/Exercises_1_7.lean b/OneVariableCalculus/Apostol/Exercises_1_7.lean deleted file mode 100644 index 3bae1d6..0000000 --- a/OneVariableCalculus/Apostol/Exercises_1_7.lean +++ /dev/null @@ -1,98 +0,0 @@ -/- -Exercises 1.7 --/ -import OneVariableCalculus.Real.Geometry.Area -import OneVariableCalculus.Real.Geometry.Rectangle - -open Real -open Real.Geometry.Area - --- ======================================== --- The properties of area in this set of exercises are to be deduced from the --- axioms for area stated in the foregoing section. --- ======================================== - --- ---------------------------------------- --- Exercise 1 --- --- Prove that each of the following sets is measurable and has zero area: --- (a) A set consisting of a single point. --- (b) A set consisting of a finite number of points in a plane. --- (c) The union of a finite collection of line segments in a plane. --- ---------------------------------------- - -example (p : Point) - : p.set_def ∈ π“œ - ∧ ((h : p.set_def ∈ π“œ) β†’ area h = 0) := - sorry - -example (S : Set Point) (hf : Set.Finite S) - : (⋃ p ∈ S, p.set_def) ∈ π“œ - ∧ ((h : (⋃ p ∈ S, p.set_def) ∈ π“œ) β†’ area h = 0) := - sorry - -example (S : Set LineSegment) (hf : Set.Finite S) - : (⋃ s ∈ S, s.set_def) ∈ π“œ - ∧ ((h : (⋃ s ∈ S, s.set_def) ∈ π“œ) β†’ area h = 0) := - sorry - --- ---------------------------------------- --- Exercise 2 --- --- Every right triangular region is measurable because it can be obtained as the --- intersection of two rectangles. Prove that every triangular region is --- measurable and that its area is one half the product of its base and --- altitude. --- ---------------------------------------- - --- # TODO - --- ---------------------------------------- --- Exercise 3 --- --- Prove that every trapezoid and every parallelogram is measurable and derive --- the usual formulas for their areas. --- ---------------------------------------- - --- # TODO - --- ---------------------------------------- --- Exercise 4 --- --- A point `(x, y)` in the plane is called a *lattice point* if both coordinates --- `x` and `y` are integers. Let `P` be a polygon whose vertices are lattice --- points inside the polygon and `B` denotes the number on the boundary. --- --- (a) Prove that the formula is valid for rectangles with sides parallel to the --- coordinate axes. --- (b) Prove that the formula is valid for right triangles and parallelograms. --- (c) Use induction on the number of edges to construct a proof for general --- polygons. --- ---------------------------------------- - --- # TODO - --- ---------------------------------------- --- Exercise 5 --- --- Prove that a triangle whose vertices are lattice points cannot be --- equilateral. --- --- [Hint: Assume there is such a triangle and compute its area in two ways, --- using exercises 2 and 4.] --- ---------------------------------------- - --- # TODO - --- ---------------------------------------- --- Exercise 6 --- --- Let `A = {1, 2, 3, 4, 5}`, and let `π“œ` denote the class of all subsets of --- `A`. (There are `32` altogether, counting `A` itself and the empty set `βˆ…`.) --- For each set `S` in `π“œ`, let `n(S)` denote the number of distinct elements in --- `S`. If `S = {1, 2, 3, 4}` and `T = {3, 4, 5}`, compute `n(S βˆͺ T)`, --- `n(S ∩ T)`, `n(S - T)`, and `n(T - S)`. Prove that the set function `n` --- satisfies the first three axioms for area. --- ---------------------------------------- - --- # TODO diff --git a/OneVariableCalculus/Apostol/Exercises_I_3_12.lean b/OneVariableCalculus/Apostol/Exercises_I_3_12.lean index 985fd26..ce41d99 100644 --- a/OneVariableCalculus/Apostol/Exercises_I_3_12.lean +++ b/OneVariableCalculus/Apostol/Exercises_I_3_12.lean @@ -19,7 +19,7 @@ import OneVariableCalculus.Apostol.Chapter_I_3 -- at least one real `z` satisfying `x < z < y`. -- ======================================== -example (x y : ℝ) (h : x < y) : βˆƒ z, x < z ∧ z < y := by +theorem exercise1 (x y : ℝ) (h : x < y) : βˆƒ z, x < z ∧ z < y := by have ⟨z, hz⟩ := exists_pos_add_of_lt' h refine ⟨x + z / 2, ⟨?_, ?_⟩⟩ Β· have hz' : z / 2 > 0 := by @@ -38,7 +38,7 @@ example (x y : ℝ) (h : x < y) : βˆƒ z, x < z ∧ z < y := by -- such that `m < x < n`. -- ======================================== -example (x : ℝ) : βˆƒ m n : ℝ, m < x ∧ x < n := by +theorem exercise2 (x : ℝ) : βˆƒ m n : ℝ, m < x ∧ x < n := by refine ⟨x - 1, ⟨x + 1, ⟨?_, ?_⟩⟩⟩ <;> norm_num -- ======================================== @@ -47,7 +47,7 @@ example (x : ℝ) : βˆƒ m n : ℝ, m < x ∧ x < n := by -- If `x > 0`, prove that there is a positive integer `n` such that `1 / n < x`. -- ======================================== -example (x : ℝ) (h : x > 0) : βˆƒ n : β„•+, 1 / n < x := by +theorem exercise3 (x : ℝ) (h : x > 0) : βˆƒ n : β„•+, 1 / n < x := by 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) @@ -63,7 +63,7 @@ example (x : ℝ) (h : x > 0) : βˆƒ n : β„•+, 1 / n < x := by -- `⌊5 / 2βŒ‹ = 2`, `⌊-8/3βŒ‹ = -3`. -- ======================================== -example (x : ℝ) : βˆƒ! n : β„€, n ≀ x ∧ x < n + 1 := by +theorem exercise4 (x : ℝ) : βˆƒ! n : β„€, n ≀ x ∧ x < n + 1 := by let n := Int.floor x refine ⟨n, ⟨?_, ?_⟩⟩ Β· exact ⟨Int.floor_le x, Int.lt_floor_add_one x⟩ @@ -78,7 +78,7 @@ example (x : ℝ) : βˆƒ! n : β„€, n ≀ x ∧ x < n + 1 := by -- `n` which satisfies `x ≀ n < x + 1`. -- ======================================== -example (x : ℝ) : βˆƒ! n : β„€, x ≀ n ∧ n < x + 1 := by +theorem exercise5 (x : ℝ) : βˆƒ! n : β„€, x ≀ n ∧ n < x + 1 := by let n := Int.ceil x refine ⟨n, ⟨?_, ?_⟩⟩ Β· exact ⟨Int.le_ceil x, Int.ceil_lt_add_one x⟩ @@ -101,8 +101,7 @@ example (x : ℝ) : βˆƒ! n : β„€, x ≀ n ∧ n < x + 1 := by -- are *dense* in the real-number system. -- ======================================== -example (x y : ℝ) (h : x < y) : βˆƒ r : β„š, x < r ∧ r < y := by - sorry +-- # TODO -- ======================================== -- Exercise 7 @@ -111,25 +110,7 @@ example (x y : ℝ) (h : x < y) : βˆƒ r : β„š, x < r ∧ r < y := by -- `xy`, `x / y`, and `y / x` are all irrational. -- ======================================== -example (x : β„š) (hx : x β‰  0) (y : ℝ) (hy : irrational y) - : irrational (x + y) := - sorry - -example (x : β„š) (hx : x β‰  0) (y : ℝ) (hy : irrational y) - : irrational (x - y) := - sorry - -example (x : β„š) (hx : x β‰  0) (y : ℝ) (hy : irrational y) - : irrational (x * y) := - sorry - -example (x : β„š) (hx : x β‰  0) (y : ℝ) (hy : irrational y) - : y β‰  0 β†’ irrational (x / y) := - sorry - -example (x : β„š) (hx : x β‰  0) (y : ℝ) (hy : irrational y) - : irrational (y / x) := - sorry +-- # TODO -- ======================================== -- Exercise 8 @@ -137,10 +118,7 @@ example (x : β„š) (hx : x β‰  0) (y : ℝ) (hy : irrational y) -- Is the sum or product of two irrational numbers always irrational? -- ======================================== --- No. Here is a counterexample. - -example (hx : x = Real.sqrt 2): irrational x ∧ rational (x * x) := by - sorry +-- # TODO -- ======================================== -- Exercise 9 @@ -150,8 +128,7 @@ example (hx : x = Real.sqrt 2): irrational x ∧ rational (x * x) := by -- infinitely many. -- ======================================== -example (x y : ℝ) (h : x < y) : βˆƒ z : ℝ, irrational z ∧ x < z ∧ z < y := by - sorry +-- # TODO -- ======================================== -- Exercise 10 @@ -171,34 +148,27 @@ def is_odd (n : β„€) := is_even (n + 1) -- (a) An integer cannot be both even and odd. -- ---------------------------------------- -example (n : β„€) : is_even n = Β¬ is_odd n := sorry +-- # TODO -- ---------------------------------------- -- (b) Every integer is either even or odd. -- ---------------------------------------- -example (n : β„€) : is_even n ∨ is_odd n := sorry +-- # TODO -- ---------------------------------------- -- (c) The sum or product of two even integers is even. What can you say about -- the sum or product of two odd integers? -- ---------------------------------------- -example (m n : β„€) : is_even m ∧ is_even n β†’ is_even (m * n) := sorry - -example (m n : β„€) : - (βˆƒ m n : β„€, is_odd m ∧ is_odd n ∧ is_even (m * n)) ∧ - (βˆƒ m n : β„€, is_odd m ∧ is_odd n ∧ is_odd (m * n)) := - sorry +-- # TODO -- ---------------------------------------- -- (d) If `nΒ²` is even, so is `n`. If `aΒ² = 2bΒ²`, where `a` and `b` are -- integers, then both `a` and `b` are even. -- ---------------------------------------- -example (n : β„€) (h : is_even (n ^ 2)) : is_even n := sorry - -example (a b : β„€) (h : a ^ 2 = 2 * b ^ 2) : is_even a ∧ is_even b := sorry +-- # TODO -- ======================================== -- Exercise 11 @@ -210,7 +180,7 @@ example (a b : β„€) (h : a ^ 2 = 2 * b ^ 2) : is_even a ∧ is_even b := sorry -- contradiction.] -- ======================================== -example : Β¬ βˆƒ n : ℝ, rational n β†’ n ^ 2 = 2 := sorry +-- # TODO -- ======================================== -- Exercise 12 @@ -222,15 +192,4 @@ example : Β¬ βˆƒ n : ℝ, rational n β†’ n ^ 2 = 2 := sorry -- least-upper-bound axiom. -- ======================================== -/-- -Shows the set of rational numbers satisfies the Archimedean property. --/ -theorem exists_pnat_mul_self_geq_of_pos {x y : β„š} - : x > 0 β†’ βˆƒ n : β„•+, n * x > y := sorry - -/-- -Show the Archimedean property does not imply the least-upper-bound axiom. --/ -example (S : Set β„š) (hne : S.Nonempty) (hbdd : BddAbove S) - : Β¬ βˆƒ x, IsLUB S x := - sorry \ No newline at end of file +-- # TODO