S_sub_S

lemma S_sub_S {f : ℕ → 𝕜} {ε : ℝ} {N : ℕ} (hε : ε ≤ 1) : S f 0 N - S f ε N = cumsum f ⌈ε * N⌉₊ / N := by  have hceilN : ⌈ε * N⌉₊ ≤ N := by    simp only [Nat.ceil_le]    exact mul_le_of_le_one_left N.cast_nonneg hε  have r1 : Finset.range N = Finset.range ⌈ε * N⌉₊ ∪ Finset.Ico ⌈ε * N⌉₊ N := by    ext n    simp only [Finset.mem_range, Finset.mem_union, Finset.mem_Ico]    omega  have r2 : Disjoint (Finset.range ⌈ε * N⌉₊) (Finset.Ico ⌈ε * N⌉₊ N) := by    rw [Finset.range_eq_Ico] ; apply Finset.Ico_disjoint_Ico_consecutive  simp [S, r1, Finset.sum_union r2, cumsum, add_div]