← Mathematical handbook

theorem Verification.integral_frankPartial_product {θ : ℝ} (hθ : θ ≠ 0) (v : ↑unitInterval) (hv : ↑v ≠ 0) : ∫ (u : ↑unitInterval), frankPartial θ ↑u ↑v * frankPartial θ ↑v ↑u = 1 / θ - ↑v / (Real.exp (θ * ↑v) - 1)

theorem Verification.frank_kendallTau_of_cdf (C : ProbabilityTheory.Copula 2) {θ : ℝ} (hθ : θ ≠ 0) (hc : ∀ (u v : ↑unitInterval), C.cdf ![u, v] = frankRealCDF θ ↑u ↑v) : C.kendallTau = 1 - 4 / θ * (1 - debyeOne θ)