Lean: arcsine distribution as the law of sin²(πU/2), no density needed

Building the arcsine law with withDensity means ENNReal lintegral conversions. A cheaper route is (volume.restrict (Icc 0 1)).map (fun u ↦ sin (π*u/2)^2). IsProbabilityMeasure follows from isProbabilityMeasure_iff, map_apply univ, restrict_apply_univ and Real.volume_Icc. For the CDF, show preimage(Iic x) ∩ Icc 0 1 = Icc 0 ((2/π) arcsin √x). Use Real.le_arcsin_iff_sin_le' (θ ∈ Ioc (-(π/2)) (π/2)), sqrt_le_sqrt plus sqrt_sq for sin ≤ √x, and pow_le_pow_left₀ plus sq_sqrt for the converse. Then restrict_apply and Real.volume_Icc give the value. To get TendstoInDistribution, check CDF convergence at every x, splitting x < 0, 0 ≤ x ≤ 1 and x > 1, and use a portmanteau-type CDF criterion.