RS.IPart.refinement_index_map

The points of fromPoints s are exactly s. -/ lemma points_fromPoints {a b : ℝ} (s : Finset ℝ) (ha : a ∈ s) (hb : b ∈ s) (h_sub : (s : Set ℝ) ⊆ Set.Icc a b) : (fromPoints (a:=a) (b:=b) s ha hb h_sub).points = s := by classical -- replicate the local defs used in fromPoints, so we can reuse them let l : List ℝ := s.sort (· ≤ ·)

have hs_nonempty : s.Nonempty := ⟨a, ha⟩ have hlpos : 0 < l.length := by simpa [l, Finset.length_sort] using (Finset.card_pos.mpr hs_nonempty)

let n : ℕ := l.length.pred have hn : n.succ = l.length := Nat.succ_pred_eq_of_pos hlpos have hn' : n + 1 = l.length := by simpa [Nat.succ_eq_add_one] using hn

ext y constructor · intro hy -- unfold points and fromPoints enough to get "y is some l.get ..." -- (we keep [l,n] in simp so it doesn't explode) have hy' : y ∈ (Finset.univ : Finset (Fin (n + 1))).image (fun i => l.get ⟨i.1, by -- this is exactly the bound proof used in fromPoints simpa [n, Nat.sub_add_cancel (Nat.succ_le_iff.mp hlpos)] using i.2⟩) := by -- this is what points is, after unfolding fromPoints simpa [IPartition.points, fromPoints, l, n] using hy

rcases Finset.mem_image.mp hy' with ⟨i, hiuniv, rfl⟩
-- Now show this list element is in s, since l = s.sort ...
have : l.get ⟨i.1, by
    simpa [n, Nat.sub_add_cancel (Nat.succ_le_iff.mp hlpos)] using i.2⟩ ∈ l :=
  List.get_mem l _
-- Convert list-membership in l to finset-membership in s using mem_sort
exact (Finset.mem_sort (s := s) (r := (· ≤ ·))).1 (by simpa [l] using this)

· intro hy -- y ∈ s → y ∈ l have hyL : y ∈ l := (Finset.mem_sort (s := s) (r := (· ≤ ·))).2 (by simpa using hy) -- pick an index j with l.get j = y rcases List.mem_iff_get.mp hyL with ⟨j, rfl⟩

-- We need to show l.get j is in the image of x over Fin (n+1).
-- Use i := cast j into Fin (n+1).
let i : Fin (n + 1) := Fin.cast hn'.symm j

-- Unfold points/fromPoints and provide witness i
have : l.get j ∈ (Finset.univ : Finset (Fin (n + 1))).image (fun i =>
  l.get ⟨i.1, by
    simpa [n, Nat.sub_add_cancel (Nat.succ_le_iff.mp hlpos)] using i.2⟩) := by
  refine Finset.mem_image.mpr ?_
  refine ⟨i, Finset.mem_univ _, ?_⟩
  -- Compare the Fin indices used in the two gets
  -- j : Fin l.length, while the RHS uses ⟨i.1, _⟩ : Fin l.length.
  -- Show they are equal by Fin.ext (only vals matter).
  have hjlen : (⟨i.1, by
      -- i.2 : i.1 < n+1, rewrite via hn' to get i.1 < l.length
      simpa [hn', i] using i.2⟩ : Fin l.length) = j := by
    apply Fin.ext
    rfl
  -- Then the gets are equal
  simpa [hjlen]

-- now translate back to the original goal
simpa [IPartition.points, fromPoints, l, n] using this

/- The union of two partitions P and Q is the partition constructed from the union of their point sets. -/ def union {a b : ℝ} (P Q : IPartition a b) : IPartition a b := fromPoints (P.points ∪ Q.points) (by exact Finset.mem_union_left _ ( Finset.mem_image.mpr ⟨ 0, Finset.mem_univ _, P.left ⟩ )) (by exact Finset.mem_union.mpr ( Or.inl <| Finset.mem_image.mpr ⟨ Fin.last _, Finset.mem_univ _, P.right ⟩ )) (by -- Since $P$ and $Q$ are partitions of $[a, b]$, their points are within $[a, b]$. have hP : ∀ y ∈ P.points, y ∈ Set.Icc a b := by intro y hy; obtain ⟨ i, hi, rfl ⟩ := Finset.mem_image.mp hy; exact ⟨ by linarith [ P.monotone ( show 0 ≤ i from Nat.zero_le _ ), P.left ], by linarith [ P.monotone ( show i ≤ Fin.last P.n from Fin.le_last _ ), P.right ] ⟩ ; have hQ : ∀ y ∈ Q.points, y ∈ Set.Icc a b := by rintro y hy; obtain ⟨ i, _, rfl ⟩ := Finset.mem_image.mp hy; exact ⟨ by linarith [ Q.left, Q.right, Q.monotone ( show 0 ≤ i from Nat.zero_le _ ) ], by linarith [ Q.left, Q.right, Q.monotone ( show i ≤ Fin.last Q.n from Fin.le_last _ ) ] ⟩ ; grind)

lemma union_points {a b : ℝ} (P Q : IPartition a b) : (union P Q).points = P.points ∪ Q.points := by -- unfolds to fromPoints on the finset union simp [union, points_fromPoints]

/- The union of two partitions refines both. -/

lemma union_refines_left {a b : ℝ} (P Q : IPartition a b) : IsRefinement (union P Q) P := by -- goal: P.points ⊆ (union P Q).points -- i.e. P.points ⊆ P.points ∪ Q.points simpa [IsRefinement, union_points] using (Finset.subset_union_left : P.points ⊆ P.points ∪ Q.points)

lemma union_refines_right {a b : ℝ} (P Q : IPartition a b) : IsRefinement (union P Q) Q := by simpa [IsRefinement, union_points] using (Finset.subset_union_right : Q.points ⊆ P.points ∪ Q.points)

/- The points of a partition constructed from a set of points are strictly increasing. -/ lemma fromPoints_strictMono {a b : ℝ} {s : Finset ℝ} {ha : a ∈ s} {hb : b ∈ s} {h_sub : (s : Set ℝ) ⊆ Set.Icc a b} : StrictMono (fromPoints s ha hb h_sub).x := by intro i j hij -- Let l be the sorted list of s let l := s.sort (· ≤ ·) -- n is l.length.pred, so n + 1 = l.length let n := l.length.pred have hn : n + 1 = l.length := Nat.succ_pred_eq_of_pos (by simpa [l, Finset.length_sort] using (Finset.card_pos.mpr ⟨a, ha⟩)) -- The type of i, j is Fin (n + 1), so their values are < l.length -- The x function is l.get ⟨i.1, _⟩ have h_sorted : List.Sorted (· < ·) l := by convert Finset.sort_sorted_lt s using 1 -- Now, i < j in Fin (n + 1) means i.1 < j.1 < l.length -- So, l.get i.1 < l.get j.1 by strict sortedness -- Unfold the definition of IPart.fromPoints.x to see the indices dsimp [IPart.fromPoints] exact h_sorted.rel_get_of_lt hij

/- The points of the union of two partitions are strictly increasing. -/ lemma union_strictMono {a b : ℝ} (P Q : IPartition a b) : StrictMono (union P Q).x := by convert fromPoints_strictMono

/- If R is a strictly monotone partition refining P via index map k, then k maps 0 to 0. -/ lemma index_map_zero {a b : ℝ} {P R : IPartition a b} (hR : StrictMono R.x) (k : Fin (P.n + 1) → Fin (R.n + 1)) (hk_eq : ∀ i, R.x (k i) = P.x i) : k 0 = 0 := by -- Since $R$ is strictly monotone and $R.x (k 0) = a$, we have $k 0 = 0$. have h_k0_eq : R.x (k 0) = R.x 0 := by exact hk_eq 0 ▸ P.left.symm ▸ R.left.symm ▸ rfl; exact hR.injective h_k0_eq

/- If R refines P, there is a monotone index map k from P to R preserving the points.