← Mathematical handbook

Ali–Mikhail–Haq CDF TP2 and proved actual-density cases

theorem Papers.AnsariRockel2024.amh_zero : ProbabilityTheory.Copula.amh 0 ⋯ ⋯ = ProbabilityTheory.Copula.independence 2

The zero-parameter AMH copula is independence on the closed square.

theorem Papers.AnsariRockel2024.amh_cdf_tp2_iff (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ ≤ 1) : (ProbabilityTheory.Copula.amh θ hmin hmax).IsTP2CDF ↔ 0 ≤ θ

CDF-level TP2 holds exactly for nonnegative AMH parameters.

theorem Papers.AnsariRockel2024.amh_negative_not_mtp2_density (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ ≤ 1) (hθ : θ < 0) : ¬(ProbabilityTheory.Copula.amh θ hmin hmax).HasMTP2Density

Negative AMH parameters have no MTP2 Lebesgue density.

theorem Papers.AnsariRockel2024.amh_zero_mtp2_density : (ProbabilityTheory.Copula.amh 0 ⋯ ⋯).HasMTP2Density

AMH at θ=0 has the independence MTP2 density.

theorem Papers.AnsariRockel2024.amh_one_mtp2_density : (ProbabilityTheory.Copula.amh 1 ⋯ ⋯).HasMTP2Density

AMH at θ=1 has the actual Clayton(1) MTP2 density.

theorem Papers.AnsariRockel2024.amh_density_formula (θ : ℝ) (hθ : 0 ≤ θ) (hθ1 : θ < 1) : (ProbabilityTheory.Copula.amh θ ⋯ ⋯).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑(Set.Icc 0 1)) => ENNReal.ofReal (Verification.amhDensity θ x)

The continuous rational formula is the actual AMH Lebesgue density for every nonnegative parameter below one, including independence.

theorem Papers.AnsariRockel2024.amh_density_tp2_iff (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ ≤ 1) : (ProbabilityTheory.Copula.amh θ hmin hmax).HasMTP2Density ↔ 0 ≤ θ

Table 3's full density-TP2 classification, including the positive interior.