Generalize set functions and move partitions in anticipation

of Apostol 1.11 exercise 8.

Bookshelf/Apostol/Chapter_1_11.lean

@@ -117,7 +117,7 @@ theorem exercise_4e (x : ℝ)
 /-- ### Exercise 7b
 
 If `a` and `b` are positive integers with no common factor, we have the formula
-`Σ_{n=1}^{b-1} ⌊na / b⌋ = ((a - 1)(b - 1)) / 2`. When `b = 1`, the sum on the
+`∑_{n=1}^{b-1} ⌊na / b⌋ = ((a - 1)(b - 1)) / 2`. When `b = 1`, the sum on the
 left is understood to be `0`.
 
 Derive the result analytically as follows: By changing the index of summation,
@@ -129,4 +129,22 @@ theorem exercise_7b (ha : a > 0) (hb : b > 0) (hp : Nat.coprime a b)
       ((a - 1) * (b - 1)) / 2 := by
   sorry
 
+/-- ### Exercise 8
+
+Let `S` be a set of points on the real line. The *characteristic function* of
+`S` is, by definition, the function `Χ` such that `Χₛ(x) = 1` for every `x` in
+`S`, and `Χₛ(x) = 0` for those `x` not in `S`. Let `f` be a step function which
+takes the constant value `cₖ` on the `k`th open subinterval `Iₖ` of some
+partition of an interval `[a, b]`. Prove that for each `x` in the union
+`I₁ ∪ I₂ ∪ ⋯ ∪ Iₙ` we have
+
+```
+f(x) = ∑_{k=1}^n cₖΧ_{Iₖ}(x).
+```
+
+This property is described by saying that every step function is a linear
+combination of characteristic functions of intervals.
+-/
+theorem exercise_8 : True := sorry
+
 end Apostol.Chapter_1_11

Bookshelf/Apostol/Chapter_1_11.tex

@@ -432,23 +432,39 @@ Now apply Exercises 4(a) and (b) to the bracket on the right.
 
 \end{proof}
 
-\section*{\unverified{Exercise 8}}%
+\section*{\proceeding{Exercise 8}}%
 \label{sec:exercise-8}
 
 Let $S$ be a set of points on the real line.
 The \textit{characteristic function} of $S$ is, by definition, the function
-  $\chi_S$ such that $\chi_S(x) = 1$ for every $x$ in $S$, and $\chi_S(x) = 0$
-  for those $x$ not in $S$.
+  $\mathcal{X}_S$ such that $\mathcal{X}_S(x) = 1$ for every $x$ in $S$, and
+  $\mathcal{X}_S(x) = 0$ for those $x$ not in $S$.
 Let $f$ be a step function which takes the constant value $c_k$ on the $k$th
   open subinterval $I_k$ of some partition of an interval $[a, b]$.
 Prove that for each $x$ in the union $I_1 \cup I_2 \cup \cdots \cup I_n$ we have
-  $$f(x) = \sum_{k=1}^n c_k\chi_{I_k}(x).$$
+  $$f(x) = \sum_{k=1}^n c_k\mathcal{X}_{I_k}(x).$$
 This property is described by saying that every step function is a linear
   combination of characteristic functions of intervals.
 
 \begin{proof}
 
-  TODO
+  Let $x \in I_1 \cup I_2 \cup \cdots \cup I_n$ and $N = \{1, \ldots, n\}$.
+  Let $k \in N$ such that $x \in I_k$.
+  Consider an arbitrary $j \in N - \{k\}$.
+  By definition of a partition, $I_j \cap I_k = \emptyset$.
+  That is, $I_j$ and $I_k$ are disjoint for all $j \in N - \{k\}$.
+  Therefore, by definition of the characteristic function,
+    $\mathcal{X}_{I_k}(x) = 1$ and $\mathcal{X}_{I_j}(x) = 0$ for all
+    $j \in N - \{k\}$.
+  Thus
+    \begin{align*}
+      f(x)
+        & = c_k \\
+        & = (c_k)(1) + \sum\nolimits_{j \in N - \{k\}} (c_j)(0) \\
+        & = c_k\mathcal{X}_{I_k}(x) +
+          \sum\nolimits_{j \in N - \{k\}} c_j\mathcal{X}_{I_j}(x) \\
+        & = \sum_{k=1}^n c_k\mathcal{X}_{I_k}(x).
+    \end{align*}
 
 \end{proof}
 

Bookshelf/Apostol/Chapter_I_03.lean

@@ -1,4 +1,6 @@
-import Common.Real.Set
+import Mathlib.Data.Real.Basic
+
+import Common.Set
 
 /-! # Apostol.Chapter_I_03
 
@@ -350,8 +352,8 @@ has a supremum, and `sup C = sup A + sup B`.
 theorem sup_minkowski_sum_eq_sup_add_sup (A B : Set ℝ) (a b : ℝ)
   (hA : A.Nonempty) (hB : B.Nonempty)
   (ha : IsLUB A a) (hb : IsLUB B b)
-  : IsLUB (Real.minkowski_sum A B) (a + b) := by
-  let C := Real.minkowski_sum A B
+  : IsLUB (Set.minkowski_sum A B) (a + b) := by
+  let C := Set.minkowski_sum A B
   -- First we show `a + b` is an upper bound of `C`.
   have hub : a + b ∈ upperBounds C := by
     rw [mem_upper_bounds_iff_forall_le]
@@ -365,7 +367,7 @@ theorem sup_minkowski_sum_eq_sup_add_sup (A B : Set ℝ) (a b : ℝ)
   -- Now we show `a + b` is the *least* upper bound of `C`. We know a least
   -- upper bound `c` exists; show that `c = a + b`.
   have ⟨c, hc⟩ := Real.exists_isLUB C
-    (Real.nonempty_minkowski_sum_iff_nonempty_add_nonempty.mpr ⟨hA, hB⟩)
+    (Set.nonempty_minkowski_sum_iff_nonempty_add_nonempty.mpr ⟨hA, hB⟩)
     ⟨a + b, hub⟩
   suffices (∀ n : ℕ+, c ≤ a + b ∧ a + b ≤ c + (1 / n)) by
     rwa [← forall_pnat_leq_self_leq_frac_imp_eq this] at hc
@@ -400,8 +402,8 @@ has an infimum, and `inf C = inf A + inf B`.
 theorem inf_minkowski_sum_eq_inf_add_inf (A B : Set ℝ)
   (hA : A.Nonempty) (hB : B.Nonempty)
   (ha : IsGLB A a) (hb : IsGLB B b)
-  : IsGLB (Real.minkowski_sum A B) (a + b) := by
-  let C := Real.minkowski_sum A B
+  : IsGLB (Set.minkowski_sum A B) (a + b) := by
+  let C := Set.minkowski_sum A B
   -- First we show `a + b` is a lower bound of `C`.
   have hlb : a + b ∈ lowerBounds C := by
     rw [mem_lower_bounds_iff_forall_ge]
@@ -415,7 +417,7 @@ theorem inf_minkowski_sum_eq_inf_add_inf (A B : Set ℝ)
   -- Now we show `a + b` is the *greatest* lower bound of `C`. We know a
   -- greatest lower bound `c` exists; show that `c = a + b`.
   have ⟨c, hc⟩ := exists_isGLB C
-    (Real.nonempty_minkowski_sum_iff_nonempty_add_nonempty.mpr ⟨hA, hB⟩)
+    (Set.nonempty_minkowski_sum_iff_nonempty_add_nonempty.mpr ⟨hA, hB⟩)
     ⟨a + b, hlb⟩
   suffices (∀ n : ℕ+, c - (1 / n) ≤ a + b ∧ a + b ≤ c) by
     rwa [← forall_pnat_frac_leq_self_leq_imp_eq this] at hc

Common.lean

@@ -2,3 +2,4 @@ import Common.Combinator
 import Common.List
 import Common.LTuple
 import Common.Real
+import Common.Set

Common/Real.lean

@@ -1,6 +1,4 @@
 import Common.Real.Basic
-import Common.Real.Function
 import Common.Real.Geometry
 import Common.Real.Rational
 import Common.Real.Sequence
-import Common.Real.Set

Common/Real/Function.lean

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

Common/Real/Function/Step.lean

@@ -1,67 +0,0 @@
-import Common.Real.Basic
-import Common.Real.Set.Partition
-
-/-! # Common.Real.Function.Step
-
-A characterization of step functions.
--/
-
-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₂ => 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₁ := (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 function `f` is a `Step` function if there exists a `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₂ => Set.Ioo x₁ x₂)),
-      ∃ c : ℝ, ∀ (hy : y ∈ I),
-        f y (mem_open_subinterval_imp_mem_partition hI hy) = c
-
-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
-
-end Step
-
-end Real.Function

Common/Real/Geometry.lean

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

Common/Real/Geometry/Area.lean

@@ -1,5 +1,5 @@
-import Common.Real.Function.Step
 import Common.Real.Geometry.Rectangle
+import Common.Real.Geometry.StepFunction
 
 /-! # Common.Real.Geometry.Area
 
@@ -107,11 +107,11 @@ 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
+theorem step_function_measurable (S : StepFunction) : S.set_def ∈ 𝓜 := by
   sorry
 
 def forall_subset_between_step_imp_le_between_area (k : ℝ) (Q : Set ℝ²) :=
-  ∀ S T : Function.Step,
+  ∀ S T : StepFunction,
     (hS : S.set_def ⊆ Q) →
     (hT : Q ⊆ T.set_def) →
     area (step_function_measurable S) ≤ k ∧ k ≤ area (step_function_measurable T)

Common/Real/Geometry/StepFunction.lean

@@ -2,20 +2,19 @@ import Mathlib.Data.Real.Basic
 import Mathlib.Data.List.Sort
 
 import Common.List.Basic
+import Common.Real.Basic
 
-/-! # Common.Real.Set.Partition
+/-! # Common.Real.Geometry.StepFunction
 
-A description of a partition as defined in the context of stepwise functions.
-Refer to [^1] for more information.
-
-[^1]: Apostol, Tom M. Calculus, Vol. 1: One-Variable Calculus, with an
-      Introduction to Linear Algebra. 2nd ed. Vol. 1. 2 vols. Wiley, 1991.
+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`.
 
@@ -27,6 +26,8 @@ structure Partition where
   sorted : Sorted LT.lt xs
   has_min_length : xs.length ≥ 2
 
+namespace Partition
+
 /--
 The length of any list associated with a `Partition` is `> 0`.
 -/
@@ -41,8 +42,6 @@ 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)
 
-namespace Partition
-
 /--
 The left-most subdivision point of the `Partition`.
 -/
@@ -103,4 +102,60 @@ theorem subdivision_point_mem_partition {p : Partition} (h : x ∈ p.xs)
 
 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 set_def (f : StepFunction) : Set ℝ² := sorry
+
+end StepFunction
+
 end Real

Common/Real/Set.lean

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

Common/Set.lean

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

Common/Set/Basic.lean

@@ -1,23 +1,24 @@
-import Mathlib.Data.Real.Basic
+import Mathlib.Data.Set.Basic
 
-/-! # Common.Real.Set.Basic
+/-! # Common.Set.Basic
 
-A collection of useful definitions and theorems regarding sets.
+Additional theorems and definitions useful in the context of sets.
 -/
 
-namespace Real
+namespace Set
 
-/--
+/-
 The Minkowski sum of two sets `s` and `t` is the set
 `s + t = { a + b : a ∈ s, b ∈ t }`.
 -/
-def minkowski_sum (s t : Set ℝ) :=
+def minkowski_sum {α : Type u} [Add α] (s t : Set α) :=
   { x | ∃ a ∈ s, ∃ b ∈ t, x = a + b }
 
 /--
 The sum of two sets is nonempty **iff** the summands are nonempty.
 -/
-def nonempty_minkowski_sum_iff_nonempty_add_nonempty {s t : Set ℝ}
+theorem nonempty_minkowski_sum_iff_nonempty_add_nonempty {α : Type u} [Add α]
+  {s t : Set α}
   : (minkowski_sum s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty := by
   apply Iff.intro
   · intro h
@@ -29,4 +30,12 @@ def nonempty_minkowski_sum_iff_nonempty_add_nonempty {s t : Set ℝ}
   · intro ⟨⟨a, ha⟩, ⟨b, hb⟩⟩
     exact ⟨a + b, ⟨a, ⟨ha, ⟨b, ⟨hb, rfl⟩⟩⟩⟩⟩
 
-end Real
+/--
+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 :=
+  if x ∈ S then 1 else 0
+
+end Set