← Mathematical handbook

theorem Verification.integral_unit_affine_reciprocal (a : ℝ) (ha : 0 < a) (ha1 : a < 1) : ∫ (v : ↑unitInterval), 1 / (a * ↑v + 1 - a) = -Real.log (1 - a) / a

Affine reciprocal integral on the unit interval.

theorem Verification.integral_unit_nelsen7_rational (a : ℝ) (ha : 0 < a) (ha1 : a < 1) : ∫ (v : ↑unitInterval), ↑v ^ 2 / (2 * (a * ↑v + 1 - a)) = (3 * a ^ 2 - 2 * a - 2 * (a - 1) ^ 2 * Real.log (1 - a)) / (4 * a ^ 3)

The logarithmic one-variable integral in Nelsen 7's Spearman rho.