← Mathematical handbook

Spearman rho integrals for Ali–Mikhail–Haq copulas

theorem Verification.amhDen_pos_of_pos_right {θ u v : ℝ} (hθ : θ ≤ 1) (hu : u ∈ Set.Icc 0 1) (hv : v ∈ Set.Icc 0 1) (hvp : 0 < v) : 0 < amhDen θ u v

theorem Verification.integral_amh_cdf_section_of_den_pos {θ : ℝ} (hmin : -1 ≤ θ) (hmax : θ ≤ 1) (h0 : θ ≠ 0) (v : ↑unitInterval) (hv : ↑v ≠ 1) (hden : ∀ u ∈ Set.Icc 0 1, 0 < amhDen θ u ↑v) : ∫ (u : ↑unitInterval), (ProbabilityTheory.Copula.amh θ hmin hmax).cdf ![u, v] = ↑v / (θ * (1 - ↑v)) + ↑v * (1 - θ * (1 - ↑v)) / (θ * (1 - ↑v)) ^ 2 * Real.log (1 - θ * (1 - ↑v))

theorem Verification.integral_amh_cdf_section {θ : ℝ} (hmin : -1 ≤ θ) (hmax : θ < 1) (h0 : θ ≠ 0) (v : ↑unitInterval) (hv : ↑v ≠ 1) : ∫ (u : ↑unitInterval), (ProbabilityTheory.Copula.amh θ hmin ⋯).cdf ![u, v] = ↑v / (θ * (1 - ↑v)) + ↑v * (1 - θ * (1 - ↑v)) / (θ * (1 - ↑v)) ^ 2 * Real.log (1 - θ * (1 - ↑v))

theorem Verification.amh_spearmanRho_integral_of_le_one {θ : ℝ} (hmin : -1 ≤ θ) (hmax : θ ≤ 1) (h0 : θ ≠ 0) : (ProbabilityTheory.Copula.amh θ hmin hmax).spearmanRho = (12 * ∫ (v : ↑unitInterval), ↑v / (θ * (1 - ↑v)) + ↑v * (1 - θ * (1 - ↑v)) / (θ * (1 - ↑v)) ^ 2 * Real.log (1 - θ * (1 - ↑v))) - 3

theorem Verification.amh_spearmanRho_integral {θ : ℝ} (hmin : -1 ≤ θ) (hmax : θ < 1) (h0 : θ ≠ 0) : (ProbabilityTheory.Copula.amh θ hmin ⋯).spearmanRho = (12 * ∫ (v : ↑unitInterval), ↑v / (θ * (1 - ↑v)) + ↑v * (1 - θ * (1 - ↑v)) / (θ * (1 - ↑v)) ^ 2 * Real.log (1 - θ * (1 - ↑v))) - 3

theorem Verification.amh_spearmanRho_zero : (ProbabilityTheory.Copula.amh 0 ⋯ ⋯).spearmanRho = 0