RS.IPart.mem_subinterval

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. -/ lemma refinement_index_map {a b : ℝ} (P R : IPartition a b) (h_ref : IsRefinement R P) : ∃ k : Fin (P.n + 1) → Fin (R.n + 1), Monotone k ∧ ∀ i, R.x (k i) = P.x i := by -- By definition of $IsRefinement$, there exists a monotone map $k$ from $P$ to $R$ such that $R.x (k i) = P.x i$ for all $i$. obtain ⟨k, hk⟩ : ∃ k : (Fin (P.n + 1)) → (Fin (R.n + 1)), (∀ i, R.x (k i) = P.x i) ∧ Monotone k := by -- By definition of $IsRefinement$, there exists a monotone map $k$ from $P$ to $R$ such that $R.x (k i) = P.x i$ for all $i$. We can construct $k$ by taking the smallest index $j$ such that $R.x j = P.x i$. have h_exists_k : ∀ i : Fin (P.n + 1), ∃ j : Fin (R.n + 1), R.x j = P.x i := by intro i have h_exists_j : P.x i ∈ R.points := by exact h_ref <| Finset.mem_image_of_mem _ <| Finset.mem_univ _ obtain ⟨j, hj⟩ := Finset.mem_image.mp h_exists_j use j aesop; have h_exists_k : ∀ i : Fin (P.n + 1), ∃ j : Fin (R.n + 1), R.x j = P.x i ∧ ∀ k : Fin (R.n + 1), R.x k = P.x i → j ≤ k := by exact fun i => ⟨ Finset.min' ( Finset.univ.filter fun j => R.x j = P.x i ) ⟨ Classical.choose ( h_exists_k i ), Finset.mem_filter.mpr ⟨ Finset.mem_univ _, Classical.choose_spec ( h_exists_k i ) ⟩ ⟩, Finset.mem_filter.mp ( Finset.min'_mem ( Finset.univ.filter fun j => R.x j = P.x i ) ⟨ Classical.choose ( h_exists_k i ), Finset.mem_filter.mpr ⟨ Finset.mem_univ _, Classical.choose_spec ( h_exists_k i ) ⟩ ⟩ ) |>.2, fun k hk => Finset.min'_le _ _ ( by aesop ) ⟩; choose k hk₁ hk₂ using h_exists_k; refine' ⟨ k, hk₁, fun i j hij => _ ⟩; have h_monotone : ∀ i j : Fin (P.n + 1), i ≤ j → P.x i ≤ P.x j := by exact fun i j hij => P.monotone hij; have h_monotone_R : ∀ i j : Fin (R.n + 1), i ≤ j → R.x i ≤ R.x j := by exact fun i j hij => R.monotone hij; contrapose! h_monotone; exact ⟨ i, j, hij, by linarith [ hk₁ i, hk₁ j, h_monotone_R _ _ h_monotone.le, show R.x ( k j ) < R.x ( k i ) from lt_of_le_of_ne ( h_monotone_R _ _ h_monotone.le ) fun h => h_monotone.ne <| le_antisymm h_monotone.le <| hk₂ _ _ <| by aesop ] ⟩; exact ⟨ k, hk.2, hk.1 ⟩

/- The sum of term over Ico u v telescopes to g(v) - g(u). -/ def term (g : ℝ → ℝ) {a b : ℝ} (R : IPartition a b) (j : ℕ) : ℝ := if h : j + 1 < R.n + 1 then g (R.x ⟨j+1, h⟩) - g (R.x ⟨j, Nat.lt_of_succ_lt h⟩) else 0

lemma sum_telescope_block {a b : ℝ} (g : ℝ → ℝ) (R : IPartition a b) (u v : Fin (R.n + 1)) (huv : u ≤ v) : ∑ j ∈ Finset.Ico u.val v.val, term g R j = g (R.x v) - g (R.x u) := by unfold term; induction' v using Fin.inductionOn with v ih ; aesop; cases huv.eq_or_lt <;> simp_all +decide [ Fin.lt_iff_val_lt_val, Nat.lt_succ_iff ]; rw [ Finset.sum_Ico_succ_top ( by linarith ), ih ( Nat.le_trans ( Nat.le_refl _ ) ‹_› ) ]; simp +decide [ Fin.add_def, Nat.mod_eq_of_lt ] ; ring!

/- A sum over consecutive intervals [k i, k (i+1)) combines into a single sum over [k 0, k n). -/

lemma sum_partition_blocks {M : Type*} [AddCommMonoid M] (n : ℕ) (k : Fin (n + 1) → ℕ) (hk : Monotone k) (F : ℕ → M) : ∑ i : Fin n, ∑ j ∈ Finset.Ico (k i.castSucc) (k i.succ), F j = ∑ j ∈ Finset.Ico (k 0) (k (Fin.last n)), F j := by rw [ ← Finset.sum_biUnion ]; · rcongr j aesop; simp +zetaDelta at *; constructor <;> intro h all_goals generalize_proofs at *; · rcases h with ⟨ i, hi ⟩ ; exact ⟨ le_trans ( hk <| Nat.zero_le _ ) hi.1, hi.2.trans_le <| hk <| Fin.le_last _ ⟩ ; · contrapose! h; intro hj have h_ind : ∀ i : Fin (n + 1), k i ≤ j := by intro i induction' i using Fin.induction with i ih all_goals generalize_proofs at *; · exact hj; · exact h i ih generalize_proofs at *; exact h_ind (Fin.last n); · intro i _ j _ hij; simp_all +decide [ Fin.ext_iff ] ; cases lt_or_gt_of_ne hij <;> simp_all +decide [ Finset.disjoint_left, hk ]; · intro a ha₁ ha₂ ha₃; linarith [ hk ( show Fin.castSucc i ≤ Fin.castSucc j from Nat.le_of_lt ‹› ), hk ( show Fin.succ i ≤ Fin.castSucc j from Nat.succ_le_of_lt ‹› ) ] ; · exact fun a ha₁ ha₂ ha₃ => le_trans ( hk <| Nat.le_of_lt_succ <| by simpa [ Fin.castSucc_lt_succ ] using ‹j < i› ) ha₁

/- That was enough of a dive. Back to maths. Well, first, two trivial estimates.-/

/- The length of the i-th subinterval of a partition P is at most the mesh of P. -/ lemma mesh_ge_diff {a b : ℝ} (P : IPartition a b) (i : Fin P.n) : P.x i.succ - P.x i.castSucc ≤ P.mesh := by apply Basic.le_max_getD apply Finset.mem_image_of_mem exact Finset.mem_univ i

/- Helper lemmas: index_map_last shows the index map preserves the last element. exists_index_between shows that for any j in the range of k, there is an interval [k i, k (i+1)) containing j. -/ lemma index_map_last {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 (Fin.last P.n) = Fin.last R.n := by -- Since $R.x$ is strictly monotone, the only way $R.x (k (Fin.last P.n)) = b$ can hold is if $k (Fin.last P.n)$ is the last element of $R$. have h_last : R.x (k (Fin.last P.n)) = R.x (Fin.last R.n) := by cases P ; cases R ; aesop; exact hR.injective h_last

lemma exists_index_between {n m : ℕ} (k : Fin (n + 1) → Fin (m + 1)) (hk : Monotone k) (hk0 : k 0 = 0) (hkn : k (Fin.last n) = Fin.last m) (j : Fin m) : ∃ i : Fin n, k i.castSucc ≤ j.castSucc ∧ j.castSucc < k i.succ := by by_contra h_contra; -- Since $k$ is monotone and $k 0 = 0$, we have $k i \le j$ for all $i$. have h_le : ∀ i : Fin (n + 1), k i ≤ Fin.castSucc j := by intro i; induction i using Fin.inductionOn <;> aesop; exact absurd ( h_le ( Fin.last n ) ) ( by simpa [ hkn ] using Fin.castSucc_lt_last j )

/- For any j in the codomain of a monotone map k (preserving endpoints), there exists i such that k i <= j < k (i+1). -/ lemma exists_index_between_v2 {n m : ℕ} (k : Fin (n + 1) → Fin (m + 1)) (hk : Monotone k) (hk0 : k 0 = 0) (hkn : k (Fin.last n) = Fin.last m) (j : Fin m) : ∃ i : Fin n, k i.castSucc ≤ j.castSucc ∧ j.castSucc < k i.succ := by exact exists_index_between k hk hk0 hkn j

/- For any y in [a, b], there exists a subinterval of P containing y, provided P.n > 0.