Include an incomplete formulation of the axiomatic definition of area.

common/Common.lean

@@ -1,4 +1,3 @@
-import Common.Data.Real.Geometry
-import Common.Data.Real.Set
-import Common.Data.Real.Sequence
+import Common.List
+import Common.Real
 import Common.Tuple

common/Common/Data/Real/Geometry.lean

@@ -1,2 +0,0 @@
-import Common.Data.Real.Geometry.Basic
-import Common.Data.Real.Geometry.Rectangle

common/Common/Data/Real/Geometry/Rectangle.lean

@@ -1,39 +0,0 @@
-import Common.Data.Real.Geometry.Basic
-
-namespace Real
-
-/--
-A `Rectangle` is characterized by two points defining opposite corners. We
-arbitrarily choose the bottom left and top right points to perform this
-characterization.
--/
-structure Rectangle (bottom_left : ℝ²) (top_right : ℝ²)
-
-namespace Rectangle
-
-/--
-A `Rectangle` is the locus of points making up its edges.
--/
-def set_eq (r : Rectangle x y) : Set ℝ² := sorry
-
-/--
-Computes the bottom right corner of a `Rectangle`.
--/
-def bottom_right (r : Rectangle x y) : ℝ² := sorry
-
-/--
-Computes the top left corner of a `Rectangle`.
--/
-def top_left (r : Rectangle x y) : ℝ² := sorry
-
-/--
-Computes the width of a `Rectangle`.
--/
-def width (r : Rectangle x y) : ℝ := sorry
-
-/--
-Computes the height of a `Rectangle`.
--/
-def height (r : Rectangle x y) : ℝ := sorry
-
-end Real.Rectangle

common/Common/Data/Real/Sequence.lean

@@ -1,2 +0,0 @@
-import Common.Data.Real.Sequence.Arithmetic
-import Common.Data.Real.Sequence.Geometric

common/Common/List.lean

@@ -0,0 +1 @@
+import Common.List.Basic

common/Common/List/Basic.lean

@@ -0,0 +1,31 @@
+import Mathlib.Logic.Basic
+
+namespace List
+
+/--
+The length of any empty list is definitionally zero.
+-/
+theorem nil_length_eq_zero : @length α [] = 0 := rfl
+
+/--
+If the length of a list is greater than zero, it cannot be `List.nil`.
+-/
+theorem length_gt_zero_imp_not_nil : xs.length > 0 → xs ≠ [] := by
+  intro h
+  by_contra nh
+  rw [nh] at h
+  have : 0 > 0 := calc 0
+    _ = length [] := by rw [←nil_length_eq_zero]
+    _ > 0 := h
+  simp at this
+
+/--
+Given a list `xs` of length `k`, produces a list of length `k - 1` where the
+`i`th member of the resulting list is `f xs[i] xs[i + 1]`.
+-/
+def pairwise (xs : List α) (f : α → α → β) : List β :=
+  match xs.tail? with
+  | none => []
+  | some ys => zipWith f xs ys
+
+end List

common/Common/Real.lean

@@ -0,0 +1,5 @@
+import Common.Real.Basic
+import Common.Real.Function
+import Common.Real.Geometry
+import Common.Real.Sequence
+import Common.Real.Set

common/Common/Real/Basic.lean

@@ -0,0 +1,5 @@
+import Mathlib.Data.Real.Basic
+
+notation "ℝ²" => ℝ × ℝ
+
+notation "ℝ³" => ℝ² × ℝ

common/Common/Real/Function.lean

@@ -0,0 +1 @@
+import Common.Real.Function.Step

common/Common/Real/Function/Step.lean

@@ -0,0 +1,38 @@
+import Mathlib.Data.Fin.Basic
+import Mathlib.Tactic.NormNum
+
+import Common.Real.Basic
+import Common.Real.Set.Partition
+
+namespace Real.Function
+
+/--
+Any member of a subinterval of a partition `P` must also be a member of `P`.
+-/
+lemma mem_open_subinterval_imp_mem_partition {p : Partition}
+  (hI : I ∈ p.xs.pairwise (fun x₁ x₂ => i(x₁, x₂)))
+  (hy : y ∈ I) : y ∈ p := by
+  unfold List.pairwise at hI
+  have ⟨ys, hys⟩ : ∃ ys, List.tail? p.xs = some ys := sorry
+  conv at hI => arg 2; rw [hys]; simp only
+  sorry
+
+/--
+A `Step` function is a function `f` along with a proof of the existence of some
+partition `P` such that `f` is constant on every open subinterval of `P`.
+-/
+structure Step where
+  p : Partition
+  f : ∀ x ∈ p, ℝ
+  const_open_subintervals :
+    ∀ (hI : I ∈ p.xs.pairwise (fun x₁ x₂ => i(x₁, x₂))),
+      ∃ c : ℝ, ∀ (hy : y ∈ I),
+        f y (mem_open_subinterval_imp_mem_partition hI hy) = c
+
+namespace Step
+
+def set_def (f : Step) : Set ℝ² := sorry
+
+-- TODO: Fill out
+
+end Real.Function.Step

common/Common/Real/Geometry.lean

@@ -0,0 +1,2 @@
+import Common.Real.Geometry.Basic
+import Common.Real.Geometry.Rectangle

common/Common/Real/Geometry/Basic.lean

@@ -1,9 +1,18 @@
 import Mathlib.Data.Real.Sqrt
 
-notation "ℝ²" => ℝ × ℝ
+import Common.Real.Basic
 
 namespace Real
 
+/--
+The undirected angle at `p2` between the line segments to `p1` and `p3`.
+
+PORT: `geometry.euclidean.angle`
+-/
+axiom angle (p₁ p₂ p₃ : ℝ²) (h : p₁ ≠ p₂ ∧ p₂ ≠ p₃ ∧ p₃ ≠ p₁): ℝ
+
+notation "∠" => angle
+
 /--
 Determine the distance between two points in `ℝ²`.
 -/

common/Common/Real/Geometry/Rectangle.lean

@@ -0,0 +1,44 @@
+import Common.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

common/Common/Real/Sequence.lean

@@ -0,0 +1,2 @@
+import Common.Real.Sequence.Arithmetic
+import Common.Real.Sequence.Geometric

common/Common/Real/Set.lean

@@ -0,0 +1,3 @@
+import Common.Real.Set.Basic
+import Common.Real.Set.Interval
+import Common.Real.Set.Partition

common/Common/Real/Set/Interval.lean

@@ -0,0 +1,33 @@
+import Mathlib.Data.Real.Basic
+
+/--
+Representation of a closed interval.
+-/
+syntax (priority := high) "i[" term "," term "]" : term
+
+macro_rules
+  | `(i[$a, $b]) => `({ z | $a ≤ z ∧ z ≤ $b })
+
+/--
+Representation of an open interval.
+-/
+syntax (priority := high) "i(" term "," term ")" : term
+
+macro_rules
+  | `(i($a, $b)) => `({ z | $a < z ∧ z < $b })
+
+/--
+Representation of a left half-open interval.
+-/
+syntax (priority := high) "i(" term "," term "]" : term
+
+macro_rules
+  | `(i($a, $b]) => `({ z | $a < z ∧ z ≤ $b })
+
+/--
+Representation of a right half-open interval.
+-/
+syntax (priority := high) "i[" term "," term ")" : term
+
+macro_rules
+  | `(i[$a, $b)) => `({ z | $a ≤ z ∧ z < $b })

common/Common/Real/Set/Partition.lean

@@ -0,0 +1,45 @@
+import Common.List.Basic
+import Common.Real.Set.Interval
+
+namespace Real
+
+/--
+A `Partition` is some finite subset of `[a, b]` containing points `a` and `b`.
+
+It is assumed that the points of the `Partition` are distinct and sorted. The
+use of a `List` ensures finite-ness.
+-/
+structure Partition where
+  xs : List ℝ
+  has_min_length : xs.length ≥ 2
+  sorted : ∀ x ∈ xs.pairwise (fun x₁ x₂ => x₁ < x₂), x
+
+namespace Partition
+
+lemma length_partition_gt_zero (p : Partition) : p.xs.length > 0 :=
+  calc p.xs.length
+    _ ≥ 2 := p.has_min_length
+    _ > 0 := by simp
+
+/--
+The left-most subdivision point of the `Partition`.
+-/
+def a (p : Partition) : ℝ :=
+  p.xs.head (List.length_gt_zero_imp_not_nil (length_partition_gt_zero p))
+
+/--
+The right-most subdivision point of the `Partition`.
+-/
+def b (p : Partition) : ℝ :=
+  p.xs.getLast (List.length_gt_zero_imp_not_nil (length_partition_gt_zero p))
+
+/--
+Define `∈` syntax for a `Partition`. We say a real is a member of a partition
+provided it lies somewhere in closed interval `[a, b]`.
+-/
+instance : Membership ℝ Partition where
+  mem (x : ℝ) (p : Partition) := p.a ≤ x ∧ x ≤ p.b
+
+end Partition
+
+end Real

one-variable-calculus/Apostol.lean

@@ -1 +1,2 @@
 import Apostol.Chapter_I_3
+import Apostol.Exercises

one-variable-calculus/Apostol/Chapter_1_6.lean

@@ -0,0 +1,157 @@
+/-
+Chapter 1.6
+
+The concept of area as a set function
+-/
+import Common.Real.Function.Step
+import Common.Real.Geometry.Rectangle
+
+namespace Real
+
+/--
+All *measurable sets*, i.e. sets in the plane to which an area can be assigned.
+
+The existence of such a class is assumed in the axiomatic definition of area
+introduced by Apostol. He denotes this set of sets as `𝓜`.
+-/
+axiom 𝓜 : Set (Set ℝ²)
+
+/--
+A set function mapping every *measurable set* to a value denoting its area.
+
+The existence of such a function is assumed in the axiomatic definition of area
+introduced by Apostol. He denotes this function as `a`.
+-/
+axiom area : ∀ ⦃x⦄, x ∈ 𝓜 → ℝ
+
+/--
+The nonnegative property.
+
+For each set `S` in `𝓜`, we have `a(S) ≥ 0`.
+-/
+axiom area_ge_zero {S : Set ℝ²} (h : S ∈ 𝓜): area h ≥ 0
+
+/--
+The additive property (i).
+
+If `S` and `T` are in `𝓜`, then `S ∪ T` in `𝓜`.
+-/
+axiom measureable_imp_union_measurable {S T : Set ℝ²} (hS : S ∈ 𝓜) (hT : T ∈ 𝓜)
+  : S ∪ T ∈ 𝓜
+
+/--
+The additive property (ii).
+
+If `S` and `T` are in `𝓜`, then `S ∩ T` in `𝓜`.
+-/
+axiom measurable_imp_inter_measurable {S T : Set ℝ²} (hS : S ∈ 𝓜) (hT : T ∈ 𝓜)
+  : S ∩ T ∈ 𝓜
+
+/--
+The additive property (iii).
+
+If `S` and `T` are in `𝓜`, then `a(S ∪ T) = a(S) + a(T) - a(S ∩ T)`.
+-/
+axiom union_area_eq_area_add_area_sub_inter_area
+  {S T : Set ℝ²} (hS : S ∈ 𝓜) (hT : T ∈ 𝓜)
+  : area (measureable_imp_union_measurable hS hT) =
+      area hS + area hT - area (measurable_imp_inter_measurable hS hT)
+
+/--
+The difference property (i).
+
+If `S` and `T` are in `𝓜` with `S ⊆ T`, then `T - S` is in `𝓜`.
+-/
+axiom measureable_imp_diff_measurable
+  {S T : Set ℝ²} (hS : S ∈ 𝓜) (hT : T ∈ 𝓜) (h : S ⊆ T)
+  : T \ S ∈ 𝓜
+
+/--
+The difference property (ii).
+
+If `S` and `T` are in `𝓜` with `S ⊆ T`, then `a(T - S) = a(T) - a(S)`.
+-/
+axiom diff_area_eq_area_sub_area
+  {S T : Set ℝ²} (hS : S ∈ 𝓜) (hT : T ∈ 𝓜) (h : S ⊆ T)
+  : area (measureable_imp_diff_measurable hS hT h) = area hT - area hS
+
+/--
+Invariance under congruence (i).
+
+If a set `S` is in `𝓜` and if `T` is congruent to `S`, then `T` is also in `𝓜`..
+-/
+axiom measurable_congruent_imp_measurable
+  {S T : Set ℝ²} (hS : S ∈ 𝓜) (h : congruent S T)
+  : T ∈ 𝓜
+
+/--
+Invariance under congruence (ii).
+
+If a set `S` is in `𝓜` and if `T` is congruent to `S`, then `a(S) = a(T)`.
+-/
+axiom congruent_imp_area_eq_area
+  {S T : Set ℝ²} (hS : S ∈ 𝓜) (h : congruent S T)
+  : area hS = area (measurable_congruent_imp_measurable hS h)
+
+/--
+Choice of scale (i).
+
+Every rectangle `R` is in `𝓜`.
+-/
+axiom rectangle_measurable (R : Rectangle)
+  : R.set_def ∈ 𝓜
+
+/--
+Choice of scale (ii).
+
+If the edges of rectangle `R` have lengths `h` and `k`, then `a(R) = hk`.
+-/
+axiom rectangle_area_eq_mul_edge_lengths (R : Rectangle)
+  : area (rectangle_measurable R) = R.width * R.height
+
+/--
+Every step region is measurable. This follows from the choice of scale axiom,
+and the fact all step regions are equivalent to the union of a collection of
+rectangles.
+-/
+theorem step_function_measurable (S : Function.Step) : S.set_def ∈ 𝓜 := by
+  sorry
+
+/--
+Exhaustion property.
+
+Let `Q` be a set that can be enclosed between two step regions `S` and `T`, so
+that (1.1) `S ⊆ Q ⊆ T`. If there is one and only one number `k` which satisfies
+the inequalities `a(S) ≤ k ≤ a(T)` for all step regions `S` and `T` satisfying
+(1.1), then `Q` is measurable and `a(Q) = k`.
+-/
+def forall_subset_between_step_imp_le_between_area (k : ℝ) (Q : Set ℝ²) :=
+  ∀ S T : Function.Step,
+    (hS : S.set_def ⊆ Q) →
+    (hT : Q ⊆ T.set_def) →
+    area (step_function_measurable S) ≤ k ∧ k ≤ area (step_function_measurable T)
+
+/--
+Exhaustion property (i).
+
+If there exists some `k` satisfying the description in the above `def`, then `Q`
+is measurable.
+-/
+axiom exhaustion_exists_unique_imp_measurable (Q : Set ℝ²)
+  : (∃ k : ℝ, forall_subset_between_step_imp_le_between_area k Q ∧
+      (∀ x : ℝ, forall_subset_between_step_imp_le_between_area x Q → x = k))
+  → Q ∈ 𝓜
+
+/--
+Exhaustion property (ii).
+
+If there exists some `k` satisfying the description in the above `def`, then `Q`
+satisfies `a(Q) = k`.
+-/
+axiom exhaustion_exists_unique_imp_area_eq (Q : Set ℝ²)
+  : ∃ k : ℝ,
+      (h : forall_subset_between_step_imp_le_between_area k Q ∧
+        (∀ 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

one-variable-calculus/Apostol/Chapter_I_3.lean

@@ -3,7 +3,7 @@ Chapter I 3
 
 A Set of Axioms for the Real-Number System
 -/
-import Common.Data.Real.Set
+import Common.Real.Set
 
 #check Archimedean
 #check Real.exists_isLUB

one-variable-calculus/Apostol/Exercises.lean

@@ -0,0 +1 @@
+import Apostol.Exercises.Exercises_I_3_12