Positive dependence¶

Import Copula.Dependence or Copula. The library separates directional tail and stochastic properties from total positivity of a CDF, a conditional kernel, or a density. These objects need different predicates.

Conventions and definitions¶

For a bivariate copula, write (U,V) for coordinates (0,1). LTD, RTI and SI describe V given U. Apply the predicate to C.reindex ![1,0] for the opposite direction. No symmetry is assumed for these three properties.

Predicate	Mathematical condition
`C.IsPQD`	`C(u,v) ≥ uv` (positive quadrant dependence)
`C.IsNQD`	`C(u,v) ≤ uv` (negative quadrant dependence)
`C.IsLTD`	`u ↦ C(u,v)/u` is nonincreasing for `u > 0`
`C.IsRTI`	`u ↦ (1−u−v+C(u,v))/(1−u)` is nondecreasing for `u < 1`
`C.IsSI`	Each section `u ↦ C(u,v)` is concave
`C.IsSD`	Each section `u ↦ C(u,v)` is convex
`C.IsCI`	SI for both `C` and `C.transpose`
`C.IsCD`	SD for both `C` and `C.transpose`
`C.IsTP2CDF`	`C(a,c) C(b,d) ≥ C(a,d) C(b,c)` for `a ≤ b`, `c ≤ d`
`C.HasTP2Kernel`	Some version of the conditional CDF kernel is TP2
`C.HasMTP2Density`	Some nonnegative measurable density version satisfies the MTP2 lattice inequality

The tail predicates use cross-multiplied inequalities internally, including the boundary points. Their equivalence to the ratio formulations is proved by isLTD_iff_ratio_antitone and isRTI_iff_survivalRatio_monotone. isRTI_iff_ratio_antitone gives the equivalent decrease of P(V ≤ v | U > u) = (v−C(u,v))/(1−u).

SI uses the chord condition

(b−a) C(c,v) + (c−b) C(a,v) ≤ (c−a) C(b,v),  a ≤ b ≤ c.

This is the CDF-section concavity characterization of stochastic increasingness. It handles coincident endpoints without division. The kernel criterion below connects this representation to conditional stochastic ordering.

Dependence.ConditionalMonotonicity uses the CI/CD convention of Ansari–Rockel. It proves SD implies NQD and that reflecting the second coordinate interchanges SI and SD. For exchangeable copulas, CI is equivalent to SI and CD to SD. All bivariate Archimedean copulas are proved exchangeable. Independence is both CI and CD, the upper Fréchet bound is CI, and the lower bound is CD. FGM is CI exactly for nonnegative parameters and CD exactly for nonpositive parameters. The full Nelsen 7 family is CD.

For background on the distinctions between CDF, kernel and density total positivity, see Fuchs and Tschimpke, Total positivity of copulas from a Markov kernel perspective. The standard tail and concavity formulations are also discussed in Weak Dependence Notions and Their Mutual Relationships.

Proved implications and closure¶

HasTP2Kernel ──→ IsSI ──→ IsLTD ──→ IsPQD
                   └──→ IsRTI ──→ IsPQD
IsTP2CDF ───────────────→ IsLTD ──→ IsPQD

CDF-TP2 also implies LTD after swapping the coordinates. PQD and CDF-TP2 are proved invariant under that swap. The library does not assert such an invariance for directional SI, LTD or RTI.

SI, LTD, RTI and PQD are each preserved by Copula.mix. Total positivity is not included in this mixture closure result. PQD and NQD together characterize independence.

Binary ordinal sums also preserve PQD. Every ordinal sum with an interior split has C(a,a)=a, so it fails NQD and differs from independence, even when both input copulas are independent. The ordinal-sum module does not yet establish closure of SI, LTD, RTI or total positivity.

import Copula.Dependence

open ProbabilityTheory
open scoped unitInterval

example (C : Copula 2) (h : C.IsSI) : C.IsPQD := h.isPQD

example (C D : Copula 2) (hC : C.IsSI) (hD : D.IsSI) (a : I) :
    (Copula.mix C D a).IsSI := hC.mix hD a

example (C : Copula 2) (h : C.HasTP2Kernel) : C.IsRTI := h.isSI.isRTI

Conditional kernels and null sets¶

cdf_eq_integral_conditionalCDF proves the disintegration formula

C(u,v) = ∫[0,u] K(t,[0,v]) dt.

cdf_eq_integral_kernel allows any almost-everywhere equal kernel version. isSI_of_kernel then proves SI when u ↦ K(u,[0,v]) is antitone for every v. Its proof uses the concavity of the indefinite integral of an antitone function, rather than derivatives of the copula.

HasTP2Kernel quantifies over a Markov kernel that agrees almost everywhere with C.conditionalKernel. It does not require the arbitrarily chosen canonical kernel to obey an ordering on null conditioning events. The converse construction of a monotone kernel from the SI chord predicate is not yet formalized.

Multivariate total positivity and densities¶

The generic ProbabilityTheory.IsMTP2 f expresses

f(x) f(y) ≤ f(x ∧ y) f(x ∨ y).

Here the meet and join are coordinatewise minimum and maximum on a cube. The generic predicate contains the algebraic inequality; nonnegativity is an explicit, mandatory part of HasMTP2Density. This density predicate works in every finite dimension, including zero, and requires equality of the actual copula measure with volume.withDensity (ENNReal.ofReal ∘ f).

The library proves the following reusable function results:

Nonnegative pointwise products preserve TP2 and MTP2.
Composition with a lattice homomorphism preserves MTP2.
Products of one-coordinate factors satisfy the lattice identity with equality.
In dimension two, the lattice and ordered-rectangle inequalities are equivalent.

The density witness implies absolute continuity. The constructor criterion toMeasure_eq_withDensity_of_cdf_integral identifies a density from its lower-orthant integrals. It is used to identify the FGM density with the existing FGM copula, so the family result concerns the bundled probability law.

This API uses density MTP2. Generalized MTP2 notions for probability measures that may be singular are a separate extension; see Positive Dependence and Weak Convergence.

Benchmarks and FGM¶

Copula	Proved results
Independence	PQD, NQD, LTD, RTI, SI, CDF-TP2, kernel-TP2; MTP2 density in every dimension
Comonotonicity	PQD, LTD, RTI, SI, CDF-TP2, kernel-TP2; no Lebesgue MTP2 density
Countermonotonicity	NQD; fails PQD, LTD, RTI, SI, CDF-TP2 and kernel-TP2
Nelsen 7, `theta ∈ [0,1]`	CD throughout; CDF-TP2 and an MTP2 density hold exactly at `theta = 1`
FGM, `theta ∈ [-1,1]`	PQD, LTD, RTI, SI and CDF-TP2 each hold exactly when `theta ≥ 0`

For FGM the density is proved to be

c_theta(u,v) = 1 + theta (1−2u)(1−2v).

It is nonnegative for the full admissible parameter interval. The displayed density satisfies the MTP2 inequality exactly for theta ≥ 0; consequently hasMTP2Density_fgm constructs the density witness for every nonnegative admissible parameter. No claim about conditional-kernel TP2 for FGM is currently included.

The comonotonic example is an explicit distinction between kernel and density total positivity: its diagonal has full copula mass and zero cube volume.

Rank consequences and remaining work¶

PQD implies nonnegative Spearman rho, Kendall tau, Spearman footrule, Gini gamma and Blomqvist beta. It also implies rho ≤ 3 tau. The implication chains above let SI, LTD, RTI and CDF/kernel TP2 hypotheses supply these conclusions. Xi is already nonnegative for every copula, so its sign does not characterize positive dependence.

Import Copula.Order.StrictSpearman (or Copula) for the sharpened criteria: within PQD, rho and tau are positive exactly when the copula differs from independence, and either coefficient being zero forces independence. Within NQD the analogous signs are negative, and zero again forces independence. The NQD proof also supplies 3 tau ≤ rho ≤ 0. These equivalences rely on the quadrant-dependence hypothesis; they do not hold for arbitrary copulas.

The ordinal-sum API also proves that NQD copulas have C(a,a)<a at every interior threshold, so they admit no nontrivial binary ordinal-sum decomposition. This includes independence and countermonotonicity; import Copula.OrdinalSum or Copula for the decomposition theorem.

The implications from an MTP2 density to CDF TP2, SI (in both directions), LCSD and RCSI are proved in Copula.Dependence.HierarchyDensity via total positivity of the measure (HasMTP2Density.isTP2Measure, HasMTP2Density.isTP2CDF, HasMTP2Density.isSI, HasMTP2Density.isLCSD, HasMTP2Density.isRCSI). The implication from density MTP2 to kernel TP2, association and FKG inequalities, a monotone-kernel converse for SI, and further family classifications remain future work. They are not hidden assumptions of any current theorem.

Exact Frechet and Mardia classifications¶

On the full valid Frechet simplex, CI holds iff b=0 and CD iff a=0. For Mardia, CI holds exactly at theta=0,1 and CD exactly at theta=-1,0. Both families are absolutely continuous with respect to square Lebesgue measure exactly at independence, and that is their exact density-TP2 region. Positive M or W weights put positive measure on a Lebesgue-null diagonal. These statements concern density TP2, not total positivity of a singular measure or its CDF.

Formal statement Source and proofProbabilityTheory.Copula.frechet_ci_iff

Formal statement Source and proofProbabilityTheory.Copula.frechet_density_tp2_iff

Formal statement Source and proofProbabilityTheory.Copula.mardia_ci_iff

Formal statement Source and proofProbabilityTheory.Copula.mardia_density_tp2_iff

Module map¶

Dependence.Basic: quadrant, tail and SI predicates, ratio equivalences and mixture closure.
Dependence.TotalPositivity: generic TP2/MTP2 algebra, CDF and density predicates.
Dependence.Conditional: disintegration, the conditional SI criterion and kernel TP2.
Dependence.Transpose: swapping coordinates and symmetric predicates.
Dependence.Rank: signs of rank coefficients and the rho ≤ 3 tau bound.
Dependence.Examples, Singular: benchmark memberships, failures and the singular-density distinction.
Dependence.Density, FGM, FGMDensity: density identification and exact FGM results.
Dependence.Frechet: full CI/CD and density classifications, measure identity and Mardia incomparability.

Corner sets, total positivity of the measure, and strictness¶

Import Copula.Dependence.HierarchyDensity, Copula.Dependence.HierarchyExamples or Copula. C.IsLCSD and C.IsRCSI are the cross-multiplied corner set conditions of Harris. isLCSD_iff_isTP2CDF and isRCSI_iff_isTP2_survival identify them with total positivity of the CDF and of the joint survival function, and both are symmetric in the coordinates. LCSD gives LTD and RCSI gives RTI, in both directions.

C.IsTP2Measure asks C(S₁×T₂) C(S₂×T₁) ≤ C(S₁×T₁) C(S₂×T₂) for measurable sets S₁ ≤ S₂, T₁ ≤ T₂. An MTP2 density implies it (HasMTP2Density.isTP2Measure), and it implies SI in both directions (IsTP2Measure.isCI), LCSD and RCSI. M satisfies it without a density.

HasMTP2Density ──→ IsTP2Measure ──→ IsCI ──→ IsSI ──→ IsLTD, IsRTI ──→ IsPQD
                        ├──→ IsLCSD (= IsTP2CDF) ──→ IsLTD (both directions)
                        └──→ IsRCSI ──→ IsRTI (both directions)

Product perturbations uv + φ(u)ψ(v) with piecewise linear profiles show strictness: PQD ⇏ LTD, RTI ⇏ LTD, LTD ⇏ RTI, LTD ∧ RTI ⇏ SI and SI(V|U) ⇏ SI(U|V). Under LTD and RTI the Capéraà–Genest inequality τ ≤ ρ holds (IsLTD.kendallTau_le_spearmanRho), so with ρ ≤ 3τ from PQD one gets τ ≤ ρ ≤ 3τ.

Library revision: fe53ea2f · Lean 4.34.0