← Copula mathematical handbook

Exact positive-dependence parameter ranges for FGM copulas

theorem ProbabilityTheory.Copula.isSI_fgm (θ : ℝ) (hθ : |θ| ≤ 1) (hpos : 0 ≤ θ) : (fgm θ hθ).IsSI

theorem ProbabilityTheory.Copula.isTP2CDF_fgm (θ : ℝ) (hθ : |θ| ≤ 1) (hpos : 0 ≤ θ) : (fgm θ hθ).IsTP2CDF

theorem ProbabilityTheory.Copula.isPQD_fgm_iff (θ : ℝ) (hθ : |θ| ≤ 1) : (fgm θ hθ).IsPQD ↔ 0 ≤ θ

theorem ProbabilityTheory.Copula.isLTD_fgm_iff (θ : ℝ) (hθ : |θ| ≤ 1) : (fgm θ hθ).IsLTD ↔ 0 ≤ θ

theorem ProbabilityTheory.Copula.isRTI_fgm_iff (θ : ℝ) (hθ : |θ| ≤ 1) : (fgm θ hθ).IsRTI ↔ 0 ≤ θ

theorem ProbabilityTheory.Copula.isSI_fgm_iff (θ : ℝ) (hθ : |θ| ≤ 1) : (fgm θ hθ).IsSI ↔ 0 ≤ θ

theorem ProbabilityTheory.Copula.isTP2CDF_fgm_iff (θ : ℝ) (hθ : |θ| ≤ 1) : (fgm θ hθ).IsTP2CDF ↔ 0 ≤ θ