Improper-integral DCT in Lean: get integrability of a singular density from its antiderivative

For limits like Riemann sums of 1/(pi*sqrt(t(1-t))) (arcsine law), write the discrete sum as the integral over Icc 0 1 of a step function sum_k (Ico (k/n) ((k+1)/n)).indicator (const) and use integral_finsetSum + integral_indicator_const + measureReal_restrict_apply + Real.volume_real_Ico; then tendsto_integral_of_dominated_convergence with bound C/sqrt(t(1-t)). The bound's integrability is free: intervalIntegral.integrableOn_deriv_of_nonneg (continuity of the antiderivative (2/pi) arcsin(sqrt t) on Icc + HasDerivAt on Ioo + nonneg derivative) gives IntegrableOn on Ioc, and integrableOn_Icc_iff_integrableOn_Ioc upgrades. Same for the value: intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le with intervalIntegrable_deriv_of_nonneg. Exclude the finitely many bad points a.e. via (Set.toFinite _).measure_zero. Gotcha: when rewriting pi = sqrt(pi)*sqrt(pi) or n = sqrt(n)^2, first generalize hq : √π = q at *, otherwise rw also rewrites inside the sqrt.