2023-04-20 19:19:56 +00:00
|
|
|
|
import Bookshelf.List.Basic
|
|
|
|
|
import Bookshelf.Real.Set.Interval
|
2023-04-18 17:29:19 +00:00
|
|
|
|
|
|
|
|
|
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`.
|
|
|
|
|
-/
|
2023-04-24 18:59:11 +00:00
|
|
|
|
def left (p : Partition) : ℝ :=
|
2023-04-18 17:29:19 +00:00
|
|
|
|
p.xs.head (List.length_gt_zero_imp_not_nil (length_partition_gt_zero p))
|
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
The right-most subdivision point of the `Partition`.
|
|
|
|
|
-/
|
2023-04-24 18:59:11 +00:00
|
|
|
|
def right (p : Partition) : ℝ :=
|
2023-04-18 17:29:19 +00:00
|
|
|
|
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
|
2023-04-24 18:59:11 +00:00
|
|
|
|
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
|
2023-04-18 17:29:19 +00:00
|
|
|
|
|
|
|
|
|
end Partition
|
|
|
|
|
|
2023-04-22 19:11:50 +00:00
|
|
|
|
end Real
|