← Copula mathematical handbook

Density total positivity and quadrant dependence

The four-quadrant determinant is obtained by successive nonnegative integrations of the pointwise MTP2 inequality. Uniform copula marginals then turn that determinant into positive quadrant dependence. This excludes every negative Clayton parameter from the HasMTP2Density class, irrespective of which almost-everywhere density version is chosen.

theorem ProbabilityTheory.Copula.hasMTP2Density_isPQD (C : Copula 2) (h : C.HasMTP2Density) : C.IsPQD

A copula with an MTP2 Lebesgue density is positively quadrant dependent.

theorem ProbabilityTheory.Copula.clayton_negative_not_density_tp2 (θ : ℝ) (hθ : -1 ≤ θ) (hn : θ < 0) : ¬(claytonNegative θ hθ hn).HasMTP2Density

No negative Clayton parameter admits an MTP2 density version, including interior parameters, without any assumption on absolute continuity.

theorem ProbabilityTheory.Copula.isCD_eq_independence_of_hasMTP2Density (C : Copula 2) (hCD : C.IsCD) (hM : C.HasMTP2Density) : C = independence 2

A conditionally decreasing copula with an MTP2 density must be independence, since CD implies NQD whereas MTP2 density implies PQD.

theorem ProbabilityTheory.Copula.isCD_eq_independence_of_isTP2CDF (C : Copula 2) (hCD : C.IsCD) (hTP : C.IsTP2CDF) : C = independence 2

CDF-level TP2 is also incompatible with conditional decreasingness, except at independence. This statement is separate from density TP2.

theorem ProbabilityTheory.Copula.nelsen7_cdf_tp2_iff (θ : ↑unitInterval) : (nelsen7 θ).IsTP2CDF ↔ θ = 1

Nelsen 7 has a TP2 distribution function only at independence.

theorem ProbabilityTheory.Copula.nelsen7_density_tp2_iff (θ : ↑unitInterval) : (nelsen7 θ).HasMTP2Density ↔ θ = 1

The Nelsen 7 family has an MTP2 density exactly at its independence endpoint; this includes the singular lower endpoint and all interior values.

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

For FGM, the actual copula has an MTP2 density exactly for nonnegative parameters. The negative exclusion applies to every possible density version, not just the displayed polynomial formula.