From f5dfb9ff6b13822425ec80d3d6db0c389822ecc1 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Fri, 12 May 2023 13:17:34 -0600 Subject: [PATCH] Generalize concept of partitions and step functions. --- Bookshelf/Apostol/Chapter_1_11.lean | 8 ++ Common/List/Basic.lean | 4 +- Common/Real/Geometry.lean | 3 +- Common/Real/Geometry/Area.lean | 21 ++-- Common/Real/Geometry/StepFunction.lean | 161 ------------------------- Common/Set.lean | 3 +- Common/Set/Basic.lean | 2 +- Common/Set/Intervals.lean | 2 + Common/Set/Intervals/Partition.lean | 125 +++++++++++++++++++ Common/Set/Intervals/StepFunction.lean | 36 ++++++ 10 files changed, 188 insertions(+), 177 deletions(-) delete mode 100644 Common/Real/Geometry/StepFunction.lean create mode 100644 Common/Set/Intervals.lean create mode 100644 Common/Set/Intervals/Partition.lean create mode 100644 Common/Set/Intervals/StepFunction.lean diff --git a/Bookshelf/Apostol/Chapter_1_11.lean b/Bookshelf/Apostol/Chapter_1_11.lean index b49df0c..1014f97 100644 --- a/Bookshelf/Apostol/Chapter_1_11.lean +++ b/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 diff --git a/Common/List/Basic.lean b/Common/List/Basic.lean index a2ca64f..1fb476a 100644 --- a/Common/List/Basic.lean +++ b/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 diff --git a/Common/Real/Geometry.lean b/Common/Real/Geometry.lean index cff361e..46762f7 100644 --- a/Common/Real/Geometry.lean +++ b/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 \ No newline at end of file +import Common.Real.Geometry.Rectangle \ No newline at end of file diff --git a/Common/Real/Geometry/Area.lean b/Common/Real/Geometry/Area.lean index 39be5d3..a7cf711 100644 --- a/Common/Real/Geometry/Area.lean +++ b/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 diff --git a/Common/Real/Geometry/StepFunction.lean b/Common/Real/Geometry/StepFunction.lean deleted file mode 100644 index 25544a2..0000000 --- a/Common/Real/Geometry/StepFunction.lean +++ /dev/null @@ -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 \ No newline at end of file diff --git a/Common/Set.lean b/Common/Set.lean index d9f9f3a..fb19067 100644 --- a/Common/Set.lean +++ b/Common/Set.lean @@ -1 +1,2 @@ -import Common.Set.Basic \ No newline at end of file +import Common.Set.Basic +import Common.Set.Intervals \ No newline at end of file diff --git a/Common/Set/Basic.lean b/Common/Set/Basic.lean index e255ca1..c2c3096 100644 --- a/Common/Set/Basic.lean +++ b/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 \ No newline at end of file diff --git a/Common/Set/Intervals.lean b/Common/Set/Intervals.lean new file mode 100644 index 0000000..9a3aceb --- /dev/null +++ b/Common/Set/Intervals.lean @@ -0,0 +1,2 @@ +import Common.Set.Intervals.Partition +import Common.Set.Intervals.StepFunction \ No newline at end of file diff --git a/Common/Set/Intervals/Partition.lean b/Common/Set/Intervals/Partition.lean new file mode 100644 index 0000000..ca297bb --- /dev/null +++ b/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 \ No newline at end of file diff --git a/Common/Set/Intervals/StepFunction.lean b/Common/Set/Intervals/StepFunction.lean new file mode 100644 index 0000000..0387616 --- /dev/null +++ b/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 \ No newline at end of file