← Mathematical handbook

Kendall tau for Ali–Mikhail–Haq copulas

theorem Verification.integral_amhPartial_product_of_den_pos {θ : ℝ} (v : ↑unitInterval) (hden : ∀ u ∈ Set.Icc 0 1, 0 < amhDen θ u ↑v) : ∫ (u : ↑unitInterval), amhPartial θ ↑u ↑v * amhPartial θ ↑v ↑u = ↑v / 3 + (1 - θ) * ↑v / (6 * (1 - θ * (1 - ↑v)))

theorem Verification.integral_amhPartial_product {θ : ℝ} (hθ : θ < 1) (v : ↑unitInterval) : ∫ (u : ↑unitInterval), amhPartial θ ↑u ↑v * amhPartial θ ↑v ↑u = ↑v / 3 + (1 - θ) * ↑v / (6 * (1 - θ * (1 - ↑v)))

theorem Verification.amh_kendallTau_integral {θ : ℝ} (hmin : -1 ≤ θ) (hmax : θ < 1) : (ProbabilityTheory.Copula.amh θ hmin ⋯).kendallTau = 1 - 4 * ∫ (v : ↑unitInterval), ↑v / 3 + (1 - θ) * ↑v / (6 * (1 - θ * (1 - ↑v)))

theorem Verification.amh_kendallTau {θ : ℝ} (hmin : -1 ≤ θ) (hmax : θ < 1) (h0 : θ ≠ 0) : (ProbabilityTheory.Copula.amh θ hmin ⋯).kendallTau = 1 - 2 / (3 * θ) - 2 * (1 - θ) ^ 2 * Real.log (1 - θ) / (3 * θ ^ 2)

theorem Verification.amh_kendallTau_zero : (ProbabilityTheory.Copula.amh 0 ⋯ ⋯).kendallTau = 0

theorem Verification.amh_kendallTau_one : (ProbabilityTheory.Copula.amh 1 ⋯ ⋯).kendallTau = 1 / 3