← Mathematical handbook

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

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

theorem Verification.frank_rho_conditional_integral (C : ProbabilityTheory.Copula 2) {θ : ℝ} (hθ : θ ≠ 0) (hc : ∀ (u v : ↑unitInterval), C.cdf ![u, v] = frankRealCDF θ ↑u ↑v) : C.spearmanRho = (12 * ∫ (u : ↑unitInterval), (1 - ↑u) * ∫ (v : ↑unitInterval), frankPartial θ ↑u ↑v) - 3

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