← Mathematical handbook

Ali–Mikhail–Haq association formulas

theorem Papers.AnsariRockel2024.amh_conditionalCDF {θ : ℝ} (hmin : -1 ≤ θ) (hmax : θ < 1) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (ProbabilityTheory.Copula.amh θ hmin ⋯).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => Verification.amhPartial θ ↑u ↑v

theorem Papers.AnsariRockel2024.amh_chatterjeeXi {θ : ℝ} (hmin : -1 ≤ θ) (hmax : θ < 1) (h0 : θ ≠ 0) : (ProbabilityTheory.Copula.amh θ hmin ⋯).chatterjeeXi = -θ / 6 - 2 / 3 + 3 / θ - 2 / θ ^ 2 - 2 * (θ - 1) ^ 2 * Real.log (1 - θ) / θ ^ 3

theorem Papers.AnsariRockel2024.amh_chatterjeeXi_zero : (ProbabilityTheory.Copula.amh 0 ⋯ ⋯).chatterjeeXi = 0

theorem Papers.AnsariRockel2024.amh_chatterjeeXi_one : (ProbabilityTheory.Copula.amh 1 ⋯ ⋯).chatterjeeXi = 1 / 6

theorem Papers.AnsariRockel2024.amh_xi_bound_near_zero {θ : ℝ} (hmin : -1 ≤ θ) (hhalf : θ ≤ 1 / 2) : (ProbabilityTheory.Copula.amh θ hmin ⋯).chatterjeeXi ≤ 4 * θ ^ 2

theorem Papers.AnsariRockel2024.amh_xi_tendsto_zero {A : Type u_1} {l : Filter A} (θ : A → ℝ) (hmin : ∀ (x : A), -1 ≤ θ x) (hmax : ∀ (x : A), θ x ≤ 1) (hθ : Filter.Tendsto θ l (nhds 0)) : Filter.Tendsto (fun (x : A) => (ProbabilityTheory.Copula.amh (θ x) ⋯ ⋯).chatterjeeXi) l (nhds 0)

theorem Papers.AnsariRockel2024.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 Papers.AnsariRockel2024.amh_kendallTau_zero : (ProbabilityTheory.Copula.amh 0 ⋯ ⋯).kendallTau = 0

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

theorem Papers.AnsariRockel2024.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 Papers.AnsariRockel2024.amh_spearmanRho_zero : (ProbabilityTheory.Copula.amh 0 ⋯ ⋯).spearmanRho = 0

theorem Papers.AnsariRockel2024.amh_spearmanRho {θ : ℝ} (hmin : -1 ≤ θ) (hmax : θ < 1) (h0 : θ ≠ 0) : (ProbabilityTheory.Copula.amh θ hmin ⋯).spearmanRho = (12 * (1 + θ) * ∫ (t : ℝ) in 1..1 - θ, Real.log t / (1 - t)) / θ ^ 2 - 24 * (1 - θ) * Real.log (1 - θ) / θ ^ 2 - 3 * (θ + 12) / θ

theorem Papers.AnsariRockel2024.amh_spearmanRho_one : (ProbabilityTheory.Copula.amh 1 ⋯ ⋯).spearmanRho = (24 * ∫ (t : ℝ) in 1..0, Real.log t / (1 - t)) - 39

theorem Papers.AnsariRockel2024.amh_spearmanRho_closed {θ : ℝ} (hmin : -1 ≤ θ) (hmax : θ ≤ 1) (h0 : θ ≠ 0) : (ProbabilityTheory.Copula.amh θ hmin hmax).spearmanRho = (12 * (1 + θ) * ∫ (t : ℝ) in 1..1 - θ, Real.log t / (1 - t)) / θ ^ 2 - 24 * (1 - θ) * Real.log (1 - θ) / θ ^ 2 - 3 * (θ + 12) / θ