Finish defining step functions.

Bookshelf/List/Basic.lean

@@ -28,4 +28,18 @@ def pairwise (xs : List α) (f : α → α → β) : List β :=
   | none => []
   | some ys => zipWith f xs ys
 
+/--
+If `x` is a member of the pairwise'd list, there must exist two (adjacent)
+elements of the list, say `x₁` and `x₂`, such that `x = f x₁ x₂`.
+-/
+theorem mem_pairwise_imp_exists {xs : List α} (h : x ∈ xs.pairwise f)
+  : ∃ x₁ x₂, x₁ ∈ xs ∧ x₂ ∈ xs ∧ x = f x₁ x₂ := by
+  unfold pairwise at h
+  cases h' : tail? xs with
+  | none => rw [h'] at h; cases h
+  | some ys =>
+    rw [h'] at h
+    simp only at h
+    sorry
+
 end List

OneVariableCalculus/Real/Function/Step.lean

@@ -1,25 +1,34 @@
-import Mathlib.Data.Fin.Basic
-import Mathlib.Tactic.NormNum
-
 import Bookshelf.Real.Basic
 import OneVariableCalculus.Real.Set.Partition
 
 namespace Real.Function
 
+open Partition
+
 /--
 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
+  -- By definition, a partition must always have at least two points in the
-  have ⟨ys, hys⟩ : ∃ ys, List.tail? p.xs = some ys := sorry
+  -- interval. We can disregard the empty case.
-  conv at hI => arg 2; rw [hys]; simp only
+  cases h : p.xs with
-  sorry
+  | nil => rw [h] at hI; cases hI
+  | cons x ys =>
+    have ⟨x₁, ⟨x₂, ⟨hx₁, ⟨hx₂, hI'⟩⟩⟩⟩ := List.mem_pairwise_imp_exists hI
+    rw [hI'] at hy
+    refine ⟨?_, ?_⟩
+    · calc p.left
+        _ ≤ x₁ := (subdivision_point_mem_partition hx₁).left
+        _ ≤ y := le_of_lt hy.left
+    · calc y
+        _ ≤ x₂ := le_of_lt hy.right
+        _ ≤ p.right := (subdivision_point_mem_partition hx₂).right
 
 /--
-A `Step` function is a function `f` along with a proof of the existence of some
+A function `f` is a `Step` function if there exists a `Partition` `p` such that
-partition `P` such that `f` is constant on every open subinterval of `P`.
+`f` is constant on every open subinterval of `p`.
 -/
 structure Step where
   p : Partition
@@ -31,8 +40,12 @@ structure Step where
 
 namespace Step
 
+/--
+The set definition of a `Step` function is the region between the constant
+values of the function's subintervals and the real axis.
+-/
 def set_def (f : Step) : Set ℝ² := sorry
 
--- TODO: Fill out
+end Step
 
-end Real.Function.Step
+end Real.Function

OneVariableCalculus/Real/Geometry/Rectangle.lean

@@ -102,9 +102,16 @@ abbrev LineSegment := Subtype (fun r : Rectangle =>
 
 namespace LineSegment
 
+/--
+A `LineSegment` `s` is the set of points corresponding to the shortest line
+segment joining the two distinct points of `s`.
+-/
 def set_def (s : LineSegment) : Set ℝ² :=
   sorry
 
+/--
+Either the width or height of a `LineSegment` is zero.
+-/
 theorem width_or_height_eq_zero (s : LineSegment)
   : s.val.width = 0 ∨ s.val.height = 0 := by
   apply Or.elim s.property

OneVariableCalculus/Real/Set/Partition.lean

@@ -24,13 +24,13 @@ lemma length_partition_gt_zero (p : Partition) : p.xs.length > 0 :=
 /--
 The left-most subdivision point of the `Partition`.
 -/
-def a (p : Partition) : ℝ :=
+def left (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) : ℝ :=
+def right (p : Partition) : ℝ :=
   p.xs.getLast (List.length_gt_zero_imp_not_nil (length_partition_gt_zero p))
 
 /--
@@ -38,7 +38,14 @@ 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
+  mem (x : ℝ) (p : Partition) := p.left ≤ x ∧ x ≤ p.right
+
+/--
+Every subdivision point of a `Partition` is itself a member of the `Partition`.
+-/
+theorem subdivision_point_mem_partition {p : Partition} (h : x ∈ p.xs)
+  : x ∈ p := by
+  sorry
 
 end Partition