Kendall's tau of FGM copulas #
The polynomial density gives the exact formula 2θ/9 on the whole admissible
interval, as in Ansari–Rockel, Table 6.
theorem
ProbabilityTheory.Copula.integral_fgm
(θ : ℝ)
(hθ : |θ| ≤ 1)
(f : (Fin 2 → ↑unitInterval) → ℝ)
:
∫ (x : Fin 2 → ↑unitInterval), f x ∂(fgm θ hθ).toMeasure = ∫ (x : Fin 2 → ↑unitInterval), fgmDensity θ x * f x