Generalize concept of partitions and step functions.

Bookshelf/Apostol/Chapter_1_11.lean

@@ -2,6 +2,8 @@ import Mathlib.Data.Real.Basic
 import Mathlib.Tactic.LibrarySearch
 
 import Common.Real.Floor
+import Common.Set.Basic
+import Common.Set.Intervals.StepFunction
 
 /-! # Apostol.Chapter_1_11 -/
 
@@ -129,6 +131,10 @@ theorem exercise_7b (ha : a > 0) (hb : b > 0) (hp : Nat.coprime a b)
       ((a - 1) * (b - 1)) / 2 := by
   sorry
 
+section
+
+open Set.Intervals
+
 /-- ### Exercise 8
 
 Let `S` be a set of points on the real line. The *characteristic function* of
@@ -147,4 +153,6 @@ combination of characteristic functions of intervals.
 -/
 theorem exercise_8 : True := sorry
 
+end
+
 end Apostol.Chapter_1_11

Common/List/Basic.lean

@@ -244,8 +244,8 @@ theorem len_pairwise_len_cons_sub_one {xs : List α} (h : xs.length > 0)
 If a `pairwise`'d `List` isn't empty, then the input `List` must have at least
 two entries.
 -/
-theorem mem_pairwise_imp_length_self_ge_2 {xs : List α} (h : xs.pairwise f ≠ [])
-  : xs.length ≥ 2 := by
+theorem mem_pairwise_imp_length_self_ge_two {xs : List α}
+  (h : xs.pairwise f ≠ []) : xs.length ≥ 2 := by
   unfold pairwise tail? at h
   cases hx : xs with
   | nil => rw [hx] at h; simp at h

Common/Real/Geometry.lean

@@ -1,4 +1,3 @@
 import Common.Real.Geometry.Area
 import Common.Real.Geometry.Basic
-import Common.Real.Geometry.Rectangle
-import Common.Real.Geometry.StepFunction
+import Common.Real.Geometry.Rectangle

Common/Real/Geometry/Area.lean

@@ -1,5 +1,5 @@
 import Common.Real.Geometry.Rectangle
-import Common.Real.Geometry.StepFunction
+import Common.Set.Intervals.StepFunction
 
 /-! # Common.Real.Geometry.Area
 
@@ -107,23 +107,24 @@ 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 : StepFunction) : S.toSet ∈ 𝓜 := by
+theorem step_function_measurable (S : Set.Intervals.StepFunction ℝ)
+  : S.toSet ∈ 𝓜 := by
   sorry
 
-def exhaustionProperty (k : ℝ) (Q : Set ℝ²) :=
-  ∀ S T : StepFunction,
-    (hS : S.toSet ⊆ Q) →
-    (hT : Q ⊆ T.toSet) →
-    area (step_function_measurable S) ≤ k ∧ k ≤ area (step_function_measurable T)
+def forallSubsetsBetween (k : ℝ) (Q : Set ℝ²) :=
+  ∀ S T : Set.Intervals.StepFunction ℝ,
+  (hS : S.toSet ⊆ Q) →
+  (hT : Q ⊆ T.toSet) →
+  area (step_function_measurable S) ≤ k ∧ k ≤ area (step_function_measurable T)
 
 axiom exhaustion_exists_unique_imp_measurable (Q : Set ℝ²)
-  : (∃! k : ℝ, exhaustionProperty k Q)
+  : (∃! k : ℝ, forallSubsetsBetween k Q)
   → Q ∈ 𝓜
 
 axiom exhaustion_exists_unique_imp_area_eq (Q : Set ℝ²)
   : ∃ k : ℝ,
-      (h : exhaustionProperty k Q ∧
-        (∀ x : ℝ, exhaustionProperty x Q → x = k))
+      (h : forallSubsetsBetween k Q ∧
+        (∀ x : ℝ, forallSubsetsBetween x Q → x = k))
     → area (exhaustion_exists_unique_imp_measurable Q ⟨k, h⟩) = k
 
 end Real.Geometry.Area

Common/Real/Geometry/StepFunction.lean

@@ -1,161 +0,0 @@
-import Mathlib.Data.Real.Basic
-import Mathlib.Data.List.Sort
-
-import Common.List.Basic
-import Common.Real.Basic
-
-/-! # Common.Real.Geometry.StepFunction
-
-A characterization of constructs surrounding step functions.
--/
-
-namespace Real
-
-open List
-
-/-! ## Partition -/
-
-/--
-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 ℝ
-  sorted : Sorted LT.lt xs
-  has_min_length : xs.length ≥ 2
-
-namespace Partition
-
-/--
-The length of any list associated with a `Partition` is `> 0`.
--/
-private lemma length_gt_zero (p : Partition) : p.xs.length > 0 :=
-  calc p.xs.length
-    _ ≥ 2 := p.has_min_length
-    _ > 0 := by simp
-
-/--
-The length of any list associated with a `Partition` is `≠ 0`.
--/
-instance (p : Partition) : NeZero (length p.xs) where
-  out := LT.lt.ne' (length_gt_zero p)
-
-/--
-The left-most subdivision point of the `Partition`.
--/
-def left (p : Partition) : ℝ :=
-  p.xs.head (neq_nil_iff_length_gt_zero.mpr (length_gt_zero p))
-
-/--
-The right-most subdivision point of the `Partition`.
--/
-def right (p : Partition) : ℝ :=
-  p.xs.getLast (neq_nil_iff_length_gt_zero.mpr (length_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.left ≤ x ∧ x ≤ p.right
-
-/--
-Every subdivision point is `≥` the left-most point of the partition.
--/
-theorem subdivision_point_geq_left {p : Partition} (h : x ∈ p.xs)
-  : p.left ≤ x := by
-  unfold left
-  rw [head_eq_get_zero (exists_mem_iff_neq_nil.mp ⟨x, h⟩)]
-  have ⟨i, hi⟩ := mem_iff_exists_get.mp h
-  conv => rhs; rw [← hi]
-  by_cases hz : i = (0 : Fin (length p.xs))
-  · rw [hz]
-    simp
-  · refine le_of_lt (Sorted.rel_get_of_lt p.sorted ?_)
-    rwa [← ne_eq, ← Fin.pos_iff_ne_zero i] at hz
-
-/--
-Every subdivision point is `≤` the right-most point of the partition.
--/
-theorem subdivision_point_leq_right {p : Partition} (h : x ∈ p.xs)
-  : x ≤ p.right := by
-  unfold right
-  have hx := exists_mem_iff_neq_nil.mp ⟨x, h⟩
-  rw [getLast_eq_get_length_sub_one hx]
-  have ⟨i, hi⟩ := mem_iff_exists_get.mp h
-  conv => lhs; rw [← hi]
-  have ⟨_, ⟨_, hs⟩⟩ := self_neq_nil_imp_exists_mem.mp hx
-  by_cases hz : i = ⟨p.xs.length - 1, by rw [hs]; simp⟩
-  · rw [hz]
-  · refine le_of_lt (Sorted.rel_get_of_lt p.sorted ?_)
-    rw [← ne_eq, Fin.ne_iff_vne] at hz
-    rw [Fin.lt_iff_val_lt_val]
-    exact lt_of_le_of_ne (le_tsub_of_add_le_right i.2) hz
-
-/--
-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 := ⟨subdivision_point_geq_left h, subdivision_point_leq_right h⟩
-
-end Partition
-
-/-! ## Step Functions -/
-
-/--
-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₂ => Set.Ioo x₁ x₂))
-  (hy : y ∈ I) : y ∈ p := by
-  cases h : p.xs with
-  | nil =>
-    -- By definition, a partition must always have at least two points in the
-    -- interval. Discharge the empty case.
-    rw [h] at hI
-    cases hI
-  | cons x ys =>
-    have ⟨i, x₁, ⟨x₂, ⟨hx₁, ⟨hx₂, hI'⟩⟩⟩⟩ :=
-      List.mem_pairwise_imp_exists_adjacent hI
-    have hx₁ : x₁ ∈ p.xs := by
-      rw [hx₁]
-      let j : Fin (List.length p.xs) := ⟨i.1, Nat.lt_of_lt_pred i.2⟩
-      exact List.mem_iff_exists_get.mpr ⟨j, rfl⟩
-    have hx₂ : x₂ ∈ p.xs := by
-      rw [hx₂]
-      let j : Fin (List.length p.xs) := ⟨i.1 + 1, lt_tsub_iff_right.mp i.2⟩
-      exact List.mem_iff_exists_get.mpr ⟨j, rfl⟩
-    rw [hI'] at hy
-    apply And.intro
-    · calc p.left
-        _ ≤ x₁ := (Partition.subdivision_point_mem_partition hx₁).left
-        _ ≤ y := le_of_lt hy.left
-    · calc y
-        _ ≤ x₂ := le_of_lt hy.right
-        _ ≤ p.right := (Partition.subdivision_point_mem_partition hx₂).right
-
-/--
-A function `f` is a `StepFunction` if there exists a `Partition` `p` such that
-`f` is constant on every open subinterval of `p`.
--/
-structure StepFunction where
-  p : Partition
-  f : ∀ x ∈ p, ℝ
-  const_open_subintervals :
-    ∀ (hI : I ∈ p.xs.pairwise (fun x₁ x₂ => Set.Ioo x₁ x₂)),
-      ∃ c : ℝ, ∀ (hy : y ∈ I),
-        f y (mem_open_subinterval_imp_mem_partition hI hy) = c
-
-namespace StepFunction
-
-/--
-The set definition of a `StepFunction` is the region between the constant values
-of the function's subintervals and the real axis.
--/
-def toSet (f : StepFunction) : Set ℝ² := sorry
-
-end StepFunction
-
-end Real

Common/Set.lean

@@ -1 +1,2 @@
-import Common.Set.Basic
+import Common.Set.Basic
+import Common.Set.Intervals

Common/Set/Basic.lean

@@ -35,7 +35,7 @@ The characteristic function of a set `S`.
 
 It returns `1` if the specified input belongs to `S` and `0` otherwise.
 -/
-def characteristic (S : Set α) (x : α) [Decidable (x ∈ S)]: Nat :=
+def characteristic (S : Set α) (x : α) [Decidable (x ∈ S)] : Nat :=
   if x ∈ S then 1 else 0
 
 end Set

Common/Set/Intervals.lean

@@ -0,0 +1,2 @@
+import Common.Set.Intervals.Partition
+import Common.Set.Intervals.StepFunction

Common/Set/Intervals/Partition.lean

@@ -0,0 +1,125 @@
+import Mathlib.Data.Finset.Basic
+import Mathlib.Data.List.Sort
+import Mathlib.Data.Set.Intervals.Basic
+
+import Common.List.Basic
+
+/-! # Common.Set.Intervals.Partition
+
+Additional theorems and definitions useful in the context of sets.
+-/
+
+namespace Set.Intervals
+
+open List
+
+/--
+A `Partition` is a finite subset of `[a, b]` containing points `a` and `b`.
+-/
+structure Partition (α : Type _) [Preorder α] [@DecidableRel α LT.lt] where
+  /- The left-most endpoint of the partition. -/
+  a : α
+  /- The right-most endpoint of the partition. -/
+  b : α
+  /- The subdivision points. -/
+  xs : List α
+  /- Ensure the subdivision points are in sorted order. -/
+  sorted_xs : Sorted LT.lt xs
+  /- Ensure each subdivision point is in our defined interval. -/
+  within_xs : ∀ x ∈ xs, x ∈ Ioo a b
+
+namespace Partition
+
+/--
+An object `x` is a member of a `Partition` `p` if `x` is an endpoint of `p` or a
+subdivision point of `p`.
+
+Notice that being a member of `p` is different from being a member of some
+(sub)interval determined by `p`.
+-/
+instance [Preorder α] [@DecidableRel α LT.lt] : Membership α (Partition α) where
+  mem (x : α) (p : Partition α) := x = p.a ∨ x ∈ p.xs ∨ x = p.b
+
+/--
+Return the endpoints and subdivision points of a `Partition` as a sorted `List`.
+-/
+def toList [Preorder α] [@DecidableRel α LT.lt] (p : Partition α) : List α :=
+  (p.a :: p.xs) ++ [p.b]
+
+/--
+`x` is a member of `Partition` `p` **iff** `x` is a member of `p.List`.
+-/
+theorem mem_self_iff_mem_toList [Preorder α] [@DecidableRel α LT.lt]
+  (p : Partition α) : x ∈ p ↔ x ∈ p.toList := by
+  apply Iff.intro
+  · sorry
+  · sorry
+
+/--
+Every member of a `Partition` is greater than or equal to its left-most point.
+-/
+theorem left_le_mem_self [Preorder α] [@DecidableRel α LT.lt]
+  (p : Partition α) : ∀ x ∈ p, p.a ≤ x := by
+  sorry
+
+/--
+Every member of a `Partition` is less than or equal to its right-most point.
+-/
+theorem right_ge_mem_self [Preorder α] [@DecidableRel α LT.lt]
+  (p : Partition α) : ∀ x ∈ p, x ≤ p.b := by
+  sorry
+
+/-
+Return the closed subintervals determined by the `Partition`.
+-/
+def closedSubintervals [Preorder α] [@DecidableRel α LT.lt]
+  (p : Partition α) : List (Set α) :=
+  p.toList.pairwise (fun x₁ x₂ => Icc x₁ x₂)
+
+/-
+Return the open subintervals determined by the `Partition`.
+-/
+def openSubintervals [Preorder α] [@DecidableRel α LT.lt]
+  (p : Partition α) : List (Set α) :=
+  p.toList.pairwise (fun x₁ x₂ => Ioo x₁ x₂)
+
+/--
+A member of an open subinterval of a `Partition` `p` is a member of the entire
+open interval determined by `p`.
+-/
+theorem mem_open_subinterval_mem_open_interval
+  [Preorder α] [@DecidableRel α LT.lt] {p : Partition α}
+  (hI : I ∈ p.openSubintervals) (hy : y ∈ I) : y ∈ Ioo p.a p.b := by
+  have ⟨i, ⟨x₁, ⟨x₂, ⟨hx₁, ⟨hx₂, hI'⟩⟩⟩⟩⟩ :=
+    List.mem_pairwise_imp_exists_adjacent hI
+  have hx₁' : p.a ≤ x₁ := by
+    refine p.left_le_mem_self x₁ ?_
+    rw [p.mem_self_iff_mem_toList]
+    have : ↑i < p.toList.length := calc ↑i
+      _ < p.toList.length - 1 := i.2
+      _ < p.toList.length := by
+        unfold List.length Partition.toList
+        simp
+    exact List.mem_iff_exists_get.mpr ⟨⟨↑i, this⟩, Eq.symm hx₁⟩
+  have hx₂' : x₂ ≤ p.b := by
+    refine p.right_ge_mem_self x₂ ?_
+    rw [p.mem_self_iff_mem_toList]
+    have : ↑i + 1 < p.toList.length := add_lt_add_right i.2 1
+    exact List.mem_iff_exists_get.mpr ⟨⟨↑i + 1, this⟩, Eq.symm hx₂⟩
+  have hx_sub := Set.Ioo_subset_Ioo hx₁' hx₂'
+  rw [hI'] at hy
+  exact Set.mem_of_subset_of_mem hx_sub hy
+
+/--
+A member of an open subinterval of a `Partition` `p` is a member of the entire
+closed interval determined by `p`.
+-/
+theorem mem_open_subinterval_mem_closed_interval
+  [Preorder α] [@DecidableRel α LT.lt] {p : Partition α}
+  (hI : I ∈ p.openSubintervals) (hy : y ∈ I) : y ∈ Icc p.a p.b := by
+  have := mem_open_subinterval_mem_open_interval hI hy
+  exact Set.mem_of_subset_of_mem Set.Ioo_subset_Icc_self this
+
+end Partition
+
+end Set.Intervals

Common/Set/Intervals/StepFunction.lean

@@ -0,0 +1,36 @@
+import Common.List.Basic
+import Common.Set.Intervals.Partition
+
+/-! # Common.Set.Intervals.StepFunction
+
+Characterization of step functions.
+-/
+
+namespace Set.Intervals
+
+/--
+A function `f`, whose domain is a closed interval `[a, b]`, is a `StepFunction`
+if there exists a `Partition` `P = {x₀, x₁, …, xₙ}` of `[a, b]` such that `f` is
+constant on each open subinterval of `P`.
+-/
+structure StepFunction (α : Type _) [Preorder α] [@DecidableRel α LT.lt] where
+  /- A partition of some closed interval `[a, b]`. -/
+  partition : Partition α
+  /-- A function whose domain is a closed interval `[a, b]`. -/
+  function : ∀ x ∈ Icc partition.a partition.b, α
+  /-- Ensure the function is constant on each open subinterval of `p`. -/
+  const_open_subintervals :
+    ∀ (hI : I ∈ partition.openSubintervals), ∃ c : α, ∀ (hy : y ∈ I),
+      function y (Partition.mem_open_subinterval_mem_closed_interval hI hy) = c
+
+namespace StepFunction
+
+/--
+The locus of points between the `x`-axis and the function.
+-/
+def toSet [Preorder α] [@DecidableRel α LT.lt]
+  (s : StepFunction α) : Set (α × α) := sorry
+
+end StepFunction
+
+end Set.Intervals