noncomputable def uniformGridRiemannSum (f : ℝ → ℝ) (N : ℕ+) : ℝ

Definition 1.3.12: The uniform-grid Riemann-sum approximation on [0, 1] with right-endpoint grid points x_i = i / N for a positive number N of subintervals is (1 / N) * ∑_{i=1}^N f(x_i). The exact comparison quantity remains the canonical interval integral ∫ x in (0 : ℝ)..1, f x = ∫_0^1 f(x) dx.

theorem uniformGridRiemannSum_def (f : ℝ → ℝ) (N : ℕ+) : uniformGridRiemannSum f N = 1 / ↑↑N * ∑ i ∈ Finset.range ↑N, f ((↑i + 1) / ↑↑N)

Unfolding formula for the uniform-grid right-endpoint Riemann sum.