Koksma's inequality in Lean without Stieltjes integrals: quantize, then let k → ∞

To prove |N⁻¹∑f(y_n) − ∫₀¹f| ≤ V(f)·D* in Mathlib, avoid Riemann–Stieltjes and Fubini. (1) For g monotone on [0,1], set V = g1 − g0 and q = g0 + (V/k)∑_{j=1}^k indicator{x ∈ [0,1] : g0 + jV/k ≤ g x}. The indicator sum at x equals ⌊θ⌋₊ with θ = (g x − g0)k/V, because #{j ∈ Icc 1 k : j ≤ θ} = #Icc 1 ⌊θ⌋₊. So |g − q| ≤ V/k. (2) Each level set E is upward closed in [0,1]. With a = sInf E you get Ioc a 1 ⊆ E ⊆ Icc a 1, so its counting error is |#{y<a}/N − a| or |#{y≤a}/N − a|. Derive the ≤ form from the < form with a right limit: the filter is eventually constant in 𝓝[>] a (eventually_all_finset), then le_of_tendsto. (3) Take integrals of indicators via integral_indicator_one plus measureReal_restrict_apply. Level sets are measurable via Set.OrdConnected.measurableSet. (4) Finish with le_of_forall_pos_le_add. For BV f, use Mathlib's variationOnFromTo.add_self_monotoneOn and sub_self_monotoneOn. Their increments add to 2V(f). Gotchas: IntervalIntegrable.congr takes an EqOn on uIoc, not an Eventually. Pass the Finset to IntervalIntegrable.sum explicitly or the congr goal gets metavariables. measurable_const.indicator makes the function fun _ => c, which does not match 1; use measurable_one.indicator.