From 1724adf00d78ce93da8e9734ba2ce9ab70687d4c Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Sat, 22 Apr 2023 13:11:50 -0600
Subject: [PATCH] Move area related concepts into one-variable-calculus.

---
 one-variable-calculus/Apostol.lean            |   5 +-
 one-variable-calculus/Apostol/Chapters.lean   |   1 +
 .../Apostol/{ => Chapters}/Chapter_I_3.lean   |   0
 .../Apostol/{ => Chapters}/Chapter_I_3.tex    |   0
 .../Apostol/Exercises/Exercises_1_7.lean      |   2 +-
 .../Apostol/Exercises/Exercises_I_3_12.lean   |   2 +-
 one-variable-calculus/Apostol/Real.lean       |   3 +
 .../Apostol/Real/Function.lean                |   1 +
 .../Apostol}/Real/Function/Step.lean          |   4 +-
 .../Apostol/Real/Geometry.lean                |   3 +
 .../Geometry/Area.lean}                       |   8 +-
 .../Apostol}/Real/Geometry/Basic.lean         |  12 +-
 .../Apostol/Real/Geometry/Rectangle.lean      | 126 ++++++++++++++++++
 one-variable-calculus/Apostol/Real/Set.lean   |   1 +
 .../Apostol}/Real/Set/Partition.lean          |   2 +-
 shared/Bookshelf/Real.lean                    |   2 -
 shared/Bookshelf/Real/Basic.lean              |  13 +-
 shared/Bookshelf/Real/Function.lean           |   1 -
 shared/Bookshelf/Real/Geometry.lean           |   2 -
 shared/Bookshelf/Real/Geometry/Rectangle.lean |  44 ------
 shared/Bookshelf/Real/Rational.lean           |   4 +-
 shared/Bookshelf/Real/Set.lean                |   3 +-
 22 files changed, 170 insertions(+), 69 deletions(-)
 create mode 100644 one-variable-calculus/Apostol/Chapters.lean
 rename one-variable-calculus/Apostol/{ => Chapters}/Chapter_I_3.lean (100%)
 rename one-variable-calculus/Apostol/{ => Chapters}/Chapter_I_3.tex (100%)
 create mode 100644 one-variable-calculus/Apostol/Real.lean
 create mode 100644 one-variable-calculus/Apostol/Real/Function.lean
 rename {shared/Bookshelf => one-variable-calculus/Apostol}/Real/Function/Step.lean (94%)
 create mode 100644 one-variable-calculus/Apostol/Real/Geometry.lean
 rename one-variable-calculus/Apostol/{Chapter_1_6.lean => Real/Geometry/Area.lean} (97%)
 rename {shared/Bookshelf => one-variable-calculus/Apostol}/Real/Geometry/Basic.lean (77%)
 create mode 100644 one-variable-calculus/Apostol/Real/Geometry/Rectangle.lean
 create mode 100644 one-variable-calculus/Apostol/Real/Set.lean
 rename {shared/Bookshelf => one-variable-calculus/Apostol}/Real/Set/Partition.lean (99%)
 delete mode 100644 shared/Bookshelf/Real/Function.lean
 delete mode 100644 shared/Bookshelf/Real/Geometry.lean
 delete mode 100644 shared/Bookshelf/Real/Geometry/Rectangle.lean

diff --git a/one-variable-calculus/Apostol.lean b/one-variable-calculus/Apostol.lean
index 5f2550f..d500f82 100644
--- a/one-variable-calculus/Apostol.lean
+++ b/one-variable-calculus/Apostol.lean
@@ -1,2 +1,3 @@
-import Apostol.Chapter_I_3
-import Apostol.Exercises
\ No newline at end of file
+import Apostol.Chapters
+import Apostol.Exercises
+import Apostol.Real
\ No newline at end of file
diff --git a/one-variable-calculus/Apostol/Chapters.lean b/one-variable-calculus/Apostol/Chapters.lean
new file mode 100644
index 0000000..b132282
--- /dev/null
+++ b/one-variable-calculus/Apostol/Chapters.lean
@@ -0,0 +1 @@
+import Apostol.Chapters.Chapter_I_3
\ No newline at end of file
diff --git a/one-variable-calculus/Apostol/Chapter_I_3.lean b/one-variable-calculus/Apostol/Chapters/Chapter_I_3.lean
similarity index 100%
rename from one-variable-calculus/Apostol/Chapter_I_3.lean
rename to one-variable-calculus/Apostol/Chapters/Chapter_I_3.lean
diff --git a/one-variable-calculus/Apostol/Chapter_I_3.tex b/one-variable-calculus/Apostol/Chapters/Chapter_I_3.tex
similarity index 100%
rename from one-variable-calculus/Apostol/Chapter_I_3.tex
rename to one-variable-calculus/Apostol/Chapters/Chapter_I_3.tex
diff --git a/one-variable-calculus/Apostol/Exercises/Exercises_1_7.lean b/one-variable-calculus/Apostol/Exercises/Exercises_1_7.lean
index 0791f1a..6eb4f6f 100644
--- a/one-variable-calculus/Apostol/Exercises/Exercises_1_7.lean
+++ b/one-variable-calculus/Apostol/Exercises/Exercises_1_7.lean
@@ -60,7 +60,7 @@ Exercises 1.7
 -- Prove that a triangle whose vertices are lattice points cannot be
 -- equilateral.
 --
--- [Hint: Assume there is such a triangle and ocmpute its area in two ways,
+-- [Hint: Assume there is such a triangle and compute its area in two ways,
 -- using exercises 2 and 4.]
 -- ----------------------------------------
 
diff --git a/one-variable-calculus/Apostol/Exercises/Exercises_I_3_12.lean b/one-variable-calculus/Apostol/Exercises/Exercises_I_3_12.lean
index 5fc75ca..286397a 100644
--- a/one-variable-calculus/Apostol/Exercises/Exercises_I_3_12.lean
+++ b/one-variable-calculus/Apostol/Exercises/Exercises_I_3_12.lean
@@ -9,7 +9,7 @@ import Mathlib.Data.Real.Basic
 import Mathlib.Data.Real.Sqrt
 import Mathlib.Tactic.LibrarySearch
 
-import Apostol.Chapter_I_3
+import Apostol.Chapters.Chapter_I_3
 import Bookshelf.Real.Rational
 
 -- ========================================
diff --git a/one-variable-calculus/Apostol/Real.lean b/one-variable-calculus/Apostol/Real.lean
new file mode 100644
index 0000000..90f9546
--- /dev/null
+++ b/one-variable-calculus/Apostol/Real.lean
@@ -0,0 +1,3 @@
+import Apostol.Real.Function
+import Apostol.Real.Geometry
+import Apostol.Real.Set
\ No newline at end of file
diff --git a/one-variable-calculus/Apostol/Real/Function.lean b/one-variable-calculus/Apostol/Real/Function.lean
new file mode 100644
index 0000000..10a38e7
--- /dev/null
+++ b/one-variable-calculus/Apostol/Real/Function.lean
@@ -0,0 +1 @@
+import Apostol.Real.Function.Step
\ No newline at end of file
diff --git a/shared/Bookshelf/Real/Function/Step.lean b/one-variable-calculus/Apostol/Real/Function/Step.lean
similarity index 94%
rename from shared/Bookshelf/Real/Function/Step.lean
rename to one-variable-calculus/Apostol/Real/Function/Step.lean
index 455351e..abf9e65 100644
--- a/shared/Bookshelf/Real/Function/Step.lean
+++ b/one-variable-calculus/Apostol/Real/Function/Step.lean
@@ -1,8 +1,8 @@
 import Mathlib.Data.Fin.Basic
 import Mathlib.Tactic.NormNum
 
+import Apostol.Real.Set.Partition
 import Bookshelf.Real.Basic
-import Bookshelf.Real.Set.Partition
 
 namespace Real.Function
 
@@ -35,4 +35,4 @@ def set_def (f : Step) : Set ℝ² := sorry
 
 -- TODO: Fill out
 
-end Real.Function.Step
+end Real.Function.Step
\ No newline at end of file
diff --git a/one-variable-calculus/Apostol/Real/Geometry.lean b/one-variable-calculus/Apostol/Real/Geometry.lean
new file mode 100644
index 0000000..20bd0f7
--- /dev/null
+++ b/one-variable-calculus/Apostol/Real/Geometry.lean
@@ -0,0 +1,3 @@
+import Apostol.Real.Geometry.Area
+import Apostol.Real.Geometry.Basic
+import Apostol.Real.Geometry.Rectangle
\ No newline at end of file
diff --git a/one-variable-calculus/Apostol/Chapter_1_6.lean b/one-variable-calculus/Apostol/Real/Geometry/Area.lean
similarity index 97%
rename from one-variable-calculus/Apostol/Chapter_1_6.lean
rename to one-variable-calculus/Apostol/Real/Geometry/Area.lean
index 239ee11..8ac3183 100644
--- a/one-variable-calculus/Apostol/Chapter_1_6.lean
+++ b/one-variable-calculus/Apostol/Real/Geometry/Area.lean
@@ -3,10 +3,10 @@ Chapter 1.6
 
 The concept of area as a set function
 -/
-import Bookshelf.Real.Function.Step
-import Bookshelf.Real.Geometry.Rectangle
+import Apostol.Real.Function.Step
+import Apostol.Real.Geometry.Rectangle
 
-namespace Real
+namespace Real.Geometry.Area
 
 /--
 All *measurable sets*, i.e. sets in the plane to which an area can be assigned.
@@ -153,4 +153,4 @@ axiom exhaustion_exists_unique_imp_area_eq (Q : Set ℝ²)
         (∀ x : ℝ, forall_subset_between_step_imp_le_between_area x Q → x = k))
     → area (exhaustion_exists_unique_imp_measurable Q ⟨k, h⟩) = k
 
-end Real
+end Real.Geometry.Area
diff --git a/shared/Bookshelf/Real/Geometry/Basic.lean b/one-variable-calculus/Apostol/Real/Geometry/Basic.lean
similarity index 77%
rename from shared/Bookshelf/Real/Geometry/Basic.lean
rename to one-variable-calculus/Apostol/Real/Geometry/Basic.lean
index 53dcc99..7e35c25 100644
--- a/shared/Bookshelf/Real/Geometry/Basic.lean
+++ b/one-variable-calculus/Apostol/Real/Geometry/Basic.lean
@@ -5,13 +5,17 @@ import Bookshelf.Real.Basic
 namespace Real
 
 /--
-The undirected angle at `p2` between the line segments to `p1` and `p3`.
+The undirected angle at `p₂` between the line segments to `p₁` and `p₃`. If
+either of those points equals `p₂`, this is `π / 2`.
 
 PORT: `geometry.euclidean.angle`
 -/
-axiom angle (p₁ p₂ p₃ : ℝ²) (h : p₁ ≠ p₂ ∧ p₂ ≠ p₃ ∧ p₃ ≠ p₁): ℝ
+axiom angle (p₁ p₂ p₃ : ℝ²) : ℝ
 
-notation "∠" => angle
+noncomputable def port_geometry_euclidean_angle (p₁ p₂ p₃ : ℝ²) :=
+  if p₁ = p₂ ∨ p₂ = p₃ then π / 2 else angle p₁ p₂ p₃
+
+notation "∠" => port_geometry_euclidean_angle
 
 /--
 Determine the distance between two points in `ℝ²`.
@@ -47,4 +51,4 @@ theorem congruent_similar {S T : Set ℝ²} : congruent S T → similar S T := b
   conv at hs => intro x y hxy; arg 1; rw [← one_mul (dist x y)]
   exact ⟨f, ⟨hf, ⟨1, hs⟩⟩⟩
 
-end Real
+end Real
\ No newline at end of file
diff --git a/one-variable-calculus/Apostol/Real/Geometry/Rectangle.lean b/one-variable-calculus/Apostol/Real/Geometry/Rectangle.lean
new file mode 100644
index 0000000..aec4728
--- /dev/null
+++ b/one-variable-calculus/Apostol/Real/Geometry/Rectangle.lean
@@ -0,0 +1,126 @@
+import Apostol.Real.Geometry.Basic
+
+namespace Real
+
+/--
+A `Rectangle` is characterized by three distinct points and the angle formed
+between line segments originating from the "bottom left" point.
+-/
+structure Rectangle where
+  top_left : ℝ²
+  bottom_left : ℝ²
+  bottom_right : ℝ²
+  forms_right_angle : ∠ top_left bottom_left bottom_right = π / 2
+
+namespace Rectangle
+
+/--
+The top-right corner of the rectangle, oriented with respect to the other
+vertices.
+-/
+def top_right (r : Rectangle) : ℝ² :=
+  ( r.top_left.fst + r.bottom_right.fst - r.bottom_left.fst
+  , r.top_left.snd + r.bottom_right.snd - r.bottom_left.snd
+  )
+
+/--
+A `Rectangle` is the locus of points bounded by its edges.
+-/
+def set_def (r : Rectangle) : Set ℝ² :=
+  sorry
+
+theorem dist_top_eq_dist_bottom (r : Rectangle)
+  : dist r.top_left r.top_right = dist r.bottom_left r.bottom_right := by
+  unfold top_right dist
+  repeat rw [add_comm, sub_right_comm, add_sub_cancel']
+
+theorem dist_left_eq_dist_right (r : Rectangle)
+  : dist r.top_left r.bottom_left = dist r.top_right r.bottom_right := by
+  unfold top_right dist
+  repeat rw [
+    sub_sub_eq_add_sub,
+    add_comm,
+    sub_add_eq_sub_sub,
+    sub_right_comm,
+    add_sub_cancel'
+  ]
+  
+/--
+Computes the width of a `Rectangle`.
+-/
+noncomputable def width (r : Rectangle) : ℝ :=
+  dist r.bottom_left r.bottom_right
+
+/--
+Computes the height of a `Rectangle`.
+-/
+noncomputable def height (r : Rectangle) : ℝ :=
+  dist r.bottom_left r.top_left
+
+end Rectangle
+
+/--
+A `Point` is a `Rectangle` in which all points coincide.
+-/
+abbrev Point := Subtype (fun r : Rectangle =>
+  r.top_left = r.bottom_left ∧ r.bottom_left = r.bottom_right)
+
+namespace Point
+
+/--
+A `Point` is the set consisting of just itself.
+-/
+def set_def (p : Point) : Set ℝ² :=
+  { x : ℝ² | x = p.val.top_left }
+
+/--
+The width of a `Point` is `0`.
+-/
+theorem width_eq_zero (p : Point) : p.val.width = 0 := by
+  unfold Rectangle.width
+  rw [p.property.right]
+  unfold dist
+  simp
+
+/--
+The height of a `Point` is `0`.
+-/
+theorem height_eq_zero (p : Point) : p.val.height = 0 := by
+  unfold Rectangle.height
+  rw [p.property.left]
+  unfold dist
+  simp
+
+end Point
+
+/--
+A `LineSegment` is a `Rectangle` in which two of the three points coincide.
+-/
+abbrev LineSegment := Subtype (fun r : Rectangle =>
+  (r.top_left = r.bottom_left ∧ r.bottom_left ≠ r.bottom_right) ∨
+  (r.top_left ≠ r.bottom_left ∧ r.bottom_left = r.bottom_right))
+
+namespace LineSegment
+
+def set_def (s : LineSegment) : Set ℝ² :=
+  sorry
+
+theorem width_or_height_eq_zero (s : LineSegment)
+  : s.val.width = 0 ∨ s.val.height = 0 := by
+  apply Or.elim s.property
+  · intro h
+    refine Or.inr ?_
+    unfold Rectangle.height
+    rw [h.left]
+    unfold dist
+    simp
+  · intro h
+    refine Or.inl ?_
+    unfold Rectangle.width
+    rw [h.right]
+    unfold dist
+    simp
+
+end LineSegment
+
+end Real
\ No newline at end of file
diff --git a/one-variable-calculus/Apostol/Real/Set.lean b/one-variable-calculus/Apostol/Real/Set.lean
new file mode 100644
index 0000000..cb51552
--- /dev/null
+++ b/one-variable-calculus/Apostol/Real/Set.lean
@@ -0,0 +1 @@
+import Apostol.Real.Set.Partition
\ No newline at end of file
diff --git a/shared/Bookshelf/Real/Set/Partition.lean b/one-variable-calculus/Apostol/Real/Set/Partition.lean
similarity index 99%
rename from shared/Bookshelf/Real/Set/Partition.lean
rename to one-variable-calculus/Apostol/Real/Set/Partition.lean
index a30f029..181c8b1 100644
--- a/shared/Bookshelf/Real/Set/Partition.lean
+++ b/one-variable-calculus/Apostol/Real/Set/Partition.lean
@@ -42,4 +42,4 @@ instance : Membership ℝ Partition where
 
 end Partition
 
-end Real
+end Real
\ No newline at end of file
diff --git a/shared/Bookshelf/Real.lean b/shared/Bookshelf/Real.lean
index b9ab721..e118fed 100644
--- a/shared/Bookshelf/Real.lean
+++ b/shared/Bookshelf/Real.lean
@@ -1,6 +1,4 @@
 import Bookshelf.Real.Basic
-import Bookshelf.Real.Function
-import Bookshelf.Real.Geometry
 import Bookshelf.Real.Rational
 import Bookshelf.Real.Sequence
 import Bookshelf.Real.Set
diff --git a/shared/Bookshelf/Real/Basic.lean b/shared/Bookshelf/Real/Basic.lean
index db92ca5..abec47e 100644
--- a/shared/Bookshelf/Real/Basic.lean
+++ b/shared/Bookshelf/Real/Basic.lean
@@ -2,4 +2,15 @@ import Mathlib.Data.Real.Basic
 
 notation "ℝ²" => ℝ × ℝ
 
-notation "ℝ³" => ℝ² × ℝ
\ No newline at end of file
+notation "ℝ³" => ℝ² × ℝ
+
+namespace Real
+
+/--
+The area of a unit circle.
+-/
+axiom pi : ℝ
+
+notation "π" => pi
+
+end Real
\ No newline at end of file
diff --git a/shared/Bookshelf/Real/Function.lean b/shared/Bookshelf/Real/Function.lean
deleted file mode 100644
index c2a3e36..0000000
--- a/shared/Bookshelf/Real/Function.lean
+++ /dev/null
@@ -1 +0,0 @@
-import Bookshelf.Real.Function.Step
diff --git a/shared/Bookshelf/Real/Geometry.lean b/shared/Bookshelf/Real/Geometry.lean
deleted file mode 100644
index 2fc3101..0000000
--- a/shared/Bookshelf/Real/Geometry.lean
+++ /dev/null
@@ -1,2 +0,0 @@
-import Bookshelf.Real.Geometry.Basic
-import Bookshelf.Real.Geometry.Rectangle
diff --git a/shared/Bookshelf/Real/Geometry/Rectangle.lean b/shared/Bookshelf/Real/Geometry/Rectangle.lean
deleted file mode 100644
index 8350fa8..0000000
--- a/shared/Bookshelf/Real/Geometry/Rectangle.lean
+++ /dev/null
@@ -1,44 +0,0 @@
-import Bookshelf.Real.Geometry.Basic
-
-namespace Real
-
-/--
-A `Rectangle` is characterized by three distinct points and the angle formed
-between line segments originating from the "bottom left" point.
--/
-structure Rectangle where
-  top_left : ℝ²
-  bottom_left : ℝ²
-  bottom_right : ℝ²
-  distinct_vertices :
-    top_left ≠ bottom_left ∧ bottom_left ≠ bottom_right ∧ bottom_right ≠ top_left
-  forms_right_angle :
-    ∠ top_left bottom_left bottom_right distinct_vertices = π / 2
-
-namespace Rectangle
-
-/--
-A calculation of the missing point.
--/
-def top_right (r : Rectangle) : ℝ² :=
-  sorry
-
-/--
-A `Rectangle` is the locus of points bounded by its edges.
--/
-def set_def (r : Rectangle) : Set ℝ² :=
-  sorry
-
-/--
-Computes the width of a `Rectangle`.
--/
-noncomputable def width (r : Rectangle) : ℝ :=
-  dist r.bottom_left r.top_left
-
-/--
-Computes the height of a `Rectangle`.
--/
-noncomputable def height (r : Rectangle) : ℝ :=
-  dist r.bottom_left r.bottom_right
-
-end Real.Rectangle
diff --git a/shared/Bookshelf/Real/Rational.lean b/shared/Bookshelf/Real/Rational.lean
index 1f2817f..fb69634 100644
--- a/shared/Bookshelf/Real/Rational.lean
+++ b/shared/Bookshelf/Real/Rational.lean
@@ -4,11 +4,11 @@ import Bookshelf.Real.Basic
 Assert that a real number is rational.
 
 Note this does *not* require the found rational to be in reduced form. Members
-of `ℚ` expect this (by proving the numerator and denominator are coprime).
+of `ℚ` expect this (by proving the numerator and denominator are co-prime).
 -/
 def rational (x : ℝ) := ∃ a : ℤ, ∃ b : ℕ, b ≠ 0 ∧ x = a / b
 
 /--
 Assert that a real number is irrational.
 -/
-def irrational (x : ℝ) := ¬ rational x
\ No newline at end of file
+def irrational (x : ℝ) := ¬ rational x
diff --git a/shared/Bookshelf/Real/Set.lean b/shared/Bookshelf/Real/Set.lean
index 9f936f3..e939cfe 100644
--- a/shared/Bookshelf/Real/Set.lean
+++ b/shared/Bookshelf/Real/Set.lean
@@ -1,3 +1,2 @@
 import Bookshelf.Real.Set.Basic
-import Bookshelf.Real.Set.Interval
-import Bookshelf.Real.Set.Partition
+import Bookshelf.Real.Set.Interval
\ No newline at end of file