Ansari–Rockel coverage and formula audit

Target: Jonathan Ansari and Marcus Rockel, Dependence properties of bivariate copula families, Dependence Modeling 12(1), 2024. This index was checked against arXiv v3, 6 April 2024, Tables 1–6 and Appendix A. It includes all 38 distinct families: 22 Archimedean, nine extreme-value (Gumbel is in both classes), three elliptical and five unclassified.

This is a reference and a formalization checklist, not a claim that all 38 families or all table entries have Lean proofs. The Lean column identifies actual measure constructors. Pending means there is no constructor yet. The property and coefficient tables below record mathematical targets; only declarations linked in the final section are proved in this library. Numerical observations and unresolved source discrepancies must not become axioms.

Conventions

• CI means SI in both directions; the existing IsSI is the paper's CIS.
• CD means stochastic decreasingness in both directions.
• The paper's TP2 is density TP2 (Definition 2.5), corresponding to HasMTP2Density, not IsTP2CDF. Singular copulas need separate treatment.
• LO means LowerOrthantLE. The paper's two-direction Schur comparison is SchurBothLE, requiring both C.SchurLE D and C.transpose.SchurLE D.transpose. Order.SymmetricSchur proves that this reduces to the directional comparison for exchangeable copulas, in particular bivariate Archimedean copulas.
• ↑ and ↓ denote parameter monotonicity. * denotes a numerical-only observation in the paper. ? means the paper does not supply a result.
• Formulas are for interior coordinates unless boundary values are explicit. Every copula has C(0,v)=C(u,0)=0, C(1,v)=v, C(u,1)=u. These must be supplied before using real division, logarithms or negative powers in Lean. Limits at parameter endpoints are not substitutions into singular expressions.
• Write P=uv, S=u+v, W=max(0,S-1), M=min(u,v), x₊=max(0,x). Let H=P/(S-P) on the interior (Clayton at one).

All families: parameter domains and CDF expressions

Archimedean families (Tables 1–2)

ID	Family	Parameters	Interior CDF	Lean
A01	Clayton	θ ≥ −1	(u^(−θ)+v^(−θ)−1)₊^(−1/θ) for θ ≠ 0; Π at 0	clayton for θ > 0; claytonNegative for −1≤θ<0; independence 2 at 0
A02	Nelsen 2	θ ≥ 1	(1−((1−u)^θ+(1−v)^θ)^(1/θ))₊	nelsen2; nelsen2_cdf_full; tendsto_nelsen2_atTop; both tail limits; exact CI/CD and TP2 exclusions; lower-orthant parameter order
A03	Ali–Mikhail–Haq	−1 ≤ θ ≤ 1	P/(1−θ(1−u)(1−v))	amh; full-square cdf_amh; CI/PQD and CDF TP2 iff θ≥0, CD/NQD iff θ≤0; MTP2 density proved at θ=0,1 and excluded for θ<0; exact lower-orthant parameter order and tail pair including θ=1
A04	Gumbel–Hougaard	θ ≥ 1	exp(−((−log u)^θ+(−log v)^θ)^(1/θ))	gumbel; full-square pointwise comonotonic endpoint; increasing lower-orthant order; exact lower/upper tail coefficients; independence at θ=1; CDF TP2 for all θ≥1
A05	Frank	θ ∈ ℝ	−log(1+(exp(−θu)−1)(exp(−θv)−1)/(exp(−θ)−1))/θ; Π at 0	frank, frank_cdf_full for θ > 0; frankNegative, frankNegative_cdf_source for θ < 0; independence 2 at zero
A06	Joe	θ ≥ 1	1−((1−u)^θ+(1−v)^θ−(1−u)^θ(1−v)^θ)^(1/θ)	joe; joe_cdf_full; full-square pointwise comonotonic endpoint; both tail limits
A07	Nelsen 7	0 ≤ θ ≤ 1	(θP+(1−θ)(S−1))₊	nelsen7
A08	Nelsen 8	θ ≥ 1	((θ²P−(1−u)(1−v))/(θ²−(θ−1)²(1−u)(1−v)))₊	nelsen8; nelsen8_cdf_full; nelsen8_one; pointwise Clayton-at-one limit; both tail limits; exact CD classification
A09	Gumbel–Barnett	0 ≤ θ ≤ 1	P exp(−θ log u log v)	nelsen9 (θ > 0), nelsen9_cdf_full
A10	Nelsen 10	0 ≤ θ ≤ 1	P/(1+(1−u^θ)(1−v^θ))^(1/θ); Π at 0	nelsen10 (θ > 0), nelsen10_cdf_full
A11	Nelsen 11	0 ≤ θ ≤ 1/2	(u^θ v^θ−2(1−u^θ)(1−v^θ))₊^(1/θ); Π at 0	nelsen11 (0 < θ ≤ 1/2), nelsen11_cdf_full; hasLowerTailDependence_nelsen11
A12	Nelsen 12	θ ≥ 1	(1+((u^(−1)−1)^θ+(v^(−1)−1)^θ)^(1/θ))^(−1)	nelsen12; nelsen12_cdf_full; full-square pointwise comonotonic endpoint; increasing lower-orthant order; CI and MTP2 density at θ=1; CDF TP2, PQD and non-CD for all θ≥1
A13	Nelsen 13	θ ≥ 0	exp(1−((1−log u)^θ+(1−log v)^θ−1)^(1/θ)); Gumbel–Barnett at parameter 1 when θ=0	nelsen13 (θ > 0), nelsen13_cdf_full; nelsen13_one
A14	Nelsen 14	θ ≥ 1	(1+((u^(−1/θ)−1)^θ+(v^(−1/θ)−1)^θ)^(1/θ))^(−θ)	nelsen14; nelsen14_cdf_full; full-square pointwise comonotonic endpoint; exact lower/upper tail coefficients; CI and MTP2 density at θ=1; CDF TP2, PQD and non-CD for all θ≥1
A15	Genest–Ghoudi (Nelsen 15)	θ ≥ 1	(1−((1−u^(1/θ))^θ+(1−v^(1/θ))^θ)^(1/θ))₊^θ	genestGhoudi; genestGhoudi_cdf_full; full-square pointwise comonotonic endpoint; exact lower/upper tail coefficients; non-CI, CDF/density-TP2 exclusions; CD iff θ=1
A16	Nelsen 16	θ ≥ 0	(s+sqrt(s²+4θ))/2, s=S−1−θ(1/u+1/v−1)	nelsen16, nelsen16_cdf_full; nelsen16_zero (W at 0); tendsto_nelsen16_atTop (Clayton(1) at ∞); hasLowerTailDependence_nelsen16 (λL = 1/2 for θ > 0)
A17	Nelsen 17	θ ∈ ℝ, θ ≠ 0	(1+((1+u)^(−θ)−1)((1+v)^(−θ)−1)/(2^(−θ)−1))^(−1/θ)−1	nelsen17, nelsen17_cdf_full; nelsen17_neg_one (Π at −1)
A18	Nelsen 18	θ ≥ 2	(1+θ/log(exp(θ/(u−1))+exp(θ/(v−1))))₊	nelsen18, cdf_nelsen18; tendsto_nelsen18_atTop (M at ∞); hasLowerTailDependence_nelsen18, hasUpperTailDependence_nelsen18
A19	Nelsen 19	θ ≥ 0	θ/log(exp(θ/u)+exp(θ/v)−exp θ); H at 0	nelsen19 (θ > 0), nelsen19_cdf_full
A20	Nelsen 20	θ ≥ 0	log(exp(u^(−θ))+exp(v^(−θ))−exp 1)^(−1/θ); Π at 0	nelsen20 (θ > 0), nelsen20_cdf_full
A21	Nelsen 21	θ ≥ 1	1−(1−((1−(1−u)^θ)^(1/θ)+(1−(1−v)^θ)^(1/θ)−1)₊^θ)^(1/θ)	nelsen21, nelsen21_cdf_full; nelsen21_one (W at 1); hasLowerTailDependence_nelsen21
A22	Nelsen 22	0 ≤ θ ≤ 1	(1+sin(asin(u^θ−1)+asin(v^θ−1)))^(1/θ) when the sum of arcsines ≥ −π/2; otherwise 0; Π at θ=0	nelsen22 (0 < θ ≤ 1), nelsen22_cdf_full; hasLowerTailDependence_nelsen22

Generator pairs (φ,ψ), with C=ψ(φ(u)+φ(v)). A multiplicative rescaling of φ and reciprocal rescaling of ψ represent the same copula. These analytic targets supplement the explicit CDFs above; they are not Lean generators until their admissibility fields are proved.

IDs	φ(t)	ψ(y), y ≥ 0
A01	(t^(−θ)−1)/θ	(1+θy)₊^(−1/θ); exponential pair at θ=0
A02	(1−t)^θ	(1−y^(1/θ))₊
A03	log((1−θ(1−t))/t)	(1−θ)/(exp y−θ) for θ<1; use H's pair at θ=1
A04	(−log t)^θ	exp(−y^(1/θ))
A05	−log((exp(−θt)−1)/(exp(−θ)−1))	−log(1+(exp(−θ)−1)exp(−y))/θ
A06	−log(1−(1−t)^θ)	1−(1−exp(−y))^(1/θ)
A07	−log(1−θ+θt)	((exp(−y)+θ−1)/θ)₊; W at θ=0
A08	(1−t)/(1+(θ−1)t)	(1−y)₊/(1+(θ−1)y)
A09	log(1−θ log t)	exp((1−exp y)/θ); exponential pair at θ=0
A10	log(2t^(−θ)−1)	(2/(exp y+1))^(1/θ); exponential pair at θ=0
A11	log(2−t^θ)	(2−exp y)₊^(1/θ); exponential pair at θ=0
A12	(1/t−1)^θ	1/(1+y^(1/θ))
A13	(1−log t)^θ−1	exp(1−(1+y)^(1/θ)); scaled limiting pair at θ=0
A14	(t^(−1/θ)−1)^θ	(1+y^(1/θ))^(−θ)
A15	(1−t^(1/θ))^θ	(1−y^(1/θ))₊^θ
A16	(1−t)(1+θ/t)	(1−y−θ+sqrt((1−y−θ)²+4θ))/2
A17	−log(((1+t)^(−θ)−1)/(2^(−θ)−1))	(1+(2^(−θ)−1)exp(−y))^(−1/θ)−1
A18	exp(θ/(t−1)), φ(1)=0	1+θ/log y for 0<y<exp(−θ); 1 at y=0; 0 above cutoff
A19	exp(θ/t)−exp θ	θ/log(y+exp θ); H's pair at θ=0
A20	exp(t^(−θ))−exp 1	log(y+exp 1)^(−1/θ); exponential pair at θ=0
A21	1−(1−(1−t)^θ)^(1/θ)	1−(1−(1−y)^θ)^(1/θ) for y≤1; 0 otherwise
A22	−asin(t^θ−1)	(1−sin y)^(1/θ) for y≤π/2; 0 otherwise; exponential pair at θ=0

Extreme-value families (Tables 1 and 4)

Their common interior expression is C(u,v)=exp((log u+log v) A(log v/(log u+log v))). The following gives a closed Pickands expression for every EV row, including the Gumbel overlap. At t=0 or t=1 set A(t)=1; powers with zero bases and negative exponents require limits. Φ is the standard normal CDF and Tν the Student-t CDF.

ID	Family	Parameters	A(t)	Lean
E01	BB5	θ≥1, δ>0	(t^θ+(1−t)^θ−((1−t)^(−θδ)+t^(−θδ))^(−1/δ))^(1/θ)	Pending
E02	Cuadras–Augé	0≤δ≤1	1−δ min(t,1−t)	cuadrasAuge
E03	Galambos	δ>0	1−(t^(−δ)+(1−t)^(−δ))^(−1/δ)	Pending
A04	Gumbel–Hougaard	θ≥1	(t^θ+(1−t)^θ)^(1/θ)	gumbel
E04	Hüsler–Reiss	δ≥0	(1−t)Φ(z(1−t))+tΦ(z(t)), z(t)=1/δ+(δ/2)log(t/(1−t)); A=1 at δ=0	Pending
E05	Joe EV	α,β∈[0,1], δ>0	1−((α(1−t))^(−δ)+(βt)^(−δ))^(−1/δ); A=1 if αβ=0	Pending
E06	Marshall–Olkin	α,β∈[0,1]	max(1−α(1−t),1−βt)	marshallOlkin
E07	Tawn	α,β∈[0,1], θ≥1	(1−α)(1−t)+(1−β)t+((α(1−t))^θ+(βt)^θ)^(1/θ)	tawn
E08	t-EV	−1<r<1, ν>0	(1−t)T(ν+1,z(1−t))+tT(ν+1,z(t)), z(t)=sqrt((1+ν)/(1−r²))((t/(1−t))^(1/ν)−r)	Pending

Special/limiting cases to retain: BB5 at θ=1 is Galambos and as δ→0 is Gumbel; Galambos and Hüsler–Reiss range from Π to M; Joe EV at α=β=1 is Galambos and as δ→∞ tends to Marshall–Olkin; Tawn at α=β=1 is Gumbel and as θ→∞ tends to Marshall–Olkin. The named gumbel_cdf_full, tawn_cdf_positive, and tawn_cdf_full formulas are checked, including the grounded zero axes. The finite-parameter identities tawn_one_one, tawn_zero_left, tawn_zero_right, and tawn_shape_one are proved, including every endpoint. The infinite-parameter limit still requires proof; it is not evaluation at an infinite real parameter. The t-EV limiting-case column of Table 4 requires independent checking (see source audit below).

Elliptical and unclassified families (Tables 1 and 4)

For an elliptical bivariate law with joint CDF F and common continuous margin G, the expression is C(u,v)=F(G⁻¹(u),G⁻¹(v)). This is an exact distributional expression, not generally an elementary closed form. The existing constructors prove its Sklar interpretation for Gaussian scale mixtures.

ID	Family	Parameters	CDF / defining law	Lean
L01	Gaussian	−1≤r≤1	Bivariate standard normal, correlation r; W and M at −1 and 1	gaussian
L02	Student-t	−1≤r≤1, ν>0	Z/sqrt(G), G~Gamma(ν/2,rate ν/2) independent of correlated normal Z	studentT
L03	Laplace	−1≤r≤1	sqrt(G) Z, G~Exp(1) independent of correlated normal Z	laplace
U01	Fréchet	α,β≥0, α+β≤1	αM+βW+(1−α−β)P	frechet
U02	Mardia	−1≤θ≤1	Fréchet with α=θ²(1+θ)/2, β=θ²(1−θ)/2	mardia
U03	FGM	−1≤θ≤1	P(1+θ(1−u)(1−v))	fgm
U04	Plackett	θ>0	(1+(θ−1)S−sqrt((1+(θ−1)S)²−4Pθ(θ−1)))/(2(θ−1)); Π at 1	Pending
U05	Raftery	0≤δ≤1	M+(1−δ)/(1+δ) P^(1/(1−δ))(1−max(u,v)^(−(1+δ)/(1−δ))); M at δ=1	Pending

The Raftery expression includes the normalization missing in v3 Table 1; see Schmidt's copula table, and the paper's own conditional derivative (25). For L02, the bivariate density has exponent −(ν+2)/2; the correlation parameter is not the dimension.

For nonsingular elliptical parameters, the joint CDF above is the double integral of the following density over (-∞,x] × (-∞,y]. Write q=(x²−2rxy+y²)/(1−r²):

• Gaussian: exp(−q/2)/(2π sqrt(1−r²)).
• Student-t: Γ((ν+2)/2)/(Γ(ν/2) νπ sqrt(1−r²)) · (1+q/ν)^(−(ν+2)/2).
• Laplace: K₀(sqrt(2q))/(π sqrt(1−r²)), with K₀ the modified Bessel function. For the scale-mixture normalization used here the univariate Laplace scale is 1/sqrt 2; changing that common scale leaves the copula unchanged. The density's value at the origin is immaterial to its measure.

These distributional density expressions are reference formulas; their identification with the existing Lean measures remains pending.

Dependence, ordering and tails: every family

This is a target index of Tables 3 and 5, with endpoint cautions. No unlinked cell is a declaration of a proved Lean result. split(c) means LO increases, Schur decreases below c and increases above c. Tail pairs are (λL,λU).

ID	CI / CD region	Density TP2	LO; Schur	Tail pair / caveat
A01	CI θ≥0; CD θ≤0	θ≥0	split(0)	(2^(−1/θ),0) for θ>0; (0,0) for θ≤0
A02	neither for θ>1; CD at 1	no	↑; unordered*	(0,2−2^(1/θ))
A03	CI θ≥0; CD θ≤0	θ≥0	split(0)	(0,0) for θ<1; (1/2,0) at 1
A04	CI	yes	↑; ↑	(0,2−2^(1/θ))
A05	CI θ≥0; CD θ≤0	θ≥0	split(0)	(0,0)
A06	CI	yes	↑; ↑	(0,2−2^(1/θ))
A07	CD; also CI at 1	only θ=1	↑; ↓	(0,0)
A08	neither for θ>1; CD at 1	no	↑; unordered*	(0,0)
A09	CD; also CI at 0	only θ=0	↓; ↑	(0,0)
A10	CD; also CI at 0	only θ=0	unordered; unordered	(0,0)
A11	CD; also CI at 0	only θ=0	↓; ↑	(0,0)
A12	CI	yes	↑; ↑	(2^(−1/θ),2−2^(1/θ))
A13	CI iff θ≥1	iff θ≥1	↑; ↑ on θ≥1	(0,0)
A14	CI	yes	↑; ↑	(1/2,2−2^(1/θ))
A15	neither for θ>1; CD at 1	no	↑; unordered*	(0,2−2^(1/θ))
A16	CI iff θ≥3	iff θ≥3+2sqrt 2	↑; ↑ on θ≥3	(1/2,0) for θ>0; (0,0) at 0
A17	CI θ≥−1; CD θ≤−1	iff θ≥−1	split(−1), excluding θ=0	(0,0)
A18	neither	no	↑; unordered*	(0,1)
A19	CI	yes	↑; ↑	(1,0) for θ>0; (1/2,0) at 0
A20	CI	yes	↑; ↑	(1,0) for θ>0; (0,0) at 0
A21	neither for θ>1; CD at 1	no	↑; unordered*	(0,2−2^(1/θ))
A22	CD; also CI at 0	only θ=0	↓; ↑	(0,0)
E01	CI	?	↑ in δ; ↑ in δ	(0,2−(2−2^(−1/δ))^(1/θ))
E02	CI	only δ=0	↑; ↑	(1{δ=1},δ)
E03	CI	?	↑; ↑	(0,2^(−1/δ))
E04	CI	yes*	↑; ↑	(0,2(1−Φ(1/δ))) for δ>0; (0,0) at 0
E05	CI	no* away from Π	↑ in δ; ↑ in δ	(0,(α^(−δ)+β^(−δ))^(−1/δ)); upper 0 if αβ=0
E06	CI	no if αβ>0; Π if αβ=0	↑ on α=β; ↑ on α=β	(1{α=β=1},min(α,β))
E07	CI	no* away from Π; audit Gumbel subfamily	↑ in θ; ↑ in θ	(0,α+β−(α^θ+β^θ)^(1/θ))
E08	CI	no*	↑ in r; ↑ in r	(0,2(1−T(ν+1,sqrt((ν+1)(1−r)/(1+r)))))
L01	CI r≥0; CD r≤0	0≤r<1; singular at ±1	split(0)	(0,0) for r<1; (1,1) at 1
L02	neither for −1<r<1	no	↑ in r; ?	both 2(1−T(ν+1,sqrt((ν+1)(1−r)/(1+r)))); limits 0 at −1 and 1 at 1
L03	paper excludes CI for r≤0 in interior; rest ?	no in interior	↑ in r; ?	? in interior; W/M endpoints give 0/1
U01	CI iff β=0; CD iff α=0	source cell inconsistent with density definition	↑ in α, ↓ in β; Schur ↑ on each unmixed axis	(α,α)
U02	CI at 0,1; CD at −1,0	source cell omits Π and includes singular M	unordered; Schur ↑ for θ≥0, ↓ for θ≤0	both θ²(1+θ)/2
U03	CI θ≥0; CD θ≤0	θ≥0	split(0)	(0,0)
U04	CI θ≥1; CD θ≤1	no for θ>2; yes on [1,2]*; no for θ<1	split(1); printed Schur range needs audit	(0,0)
U05	CI	only δ=0	↑; ↑	(2δ/(1+δ),0) for δ<1; (1,1) at 1

LTD, RTI and PQD follow from SI where the library's implication theorems apply. They should be derived once from the relevant CI/CIS proof rather than inserted as independent assumptions in every family record.

Association expressions (all nonempty cells of Table 6)

Blank cells in the paper mean no expression supplied there, not zero. Let Dk(x)=k/x^k ∫₀ˣ t^k/(exp t−1) dt, E1(x)=∫₁∞ exp(−xs)/s ds, and let ₂F₁ denote the hypergeometric function. ξ is directional: second coordinate given first.

ID	ξ	Spearman ρ	Kendall τ
A01	6∫₀¹ ₂F₁(1/θ,2+2/θ;1+1/θ;1−v^(−θ)) dv−2, θ>0	not supplied	θ/(θ+2)
A03	3/θ−θ/6−2/3−2/θ²−2(θ−1)²log(1−θ)/θ³	12(1+θ)/θ² ∫₁^(1−θ) log t/(1−t) dt−24(1−θ)log(1−θ)/θ²−3(θ+12)/θ	1−2/(3θ)−2(1−θ)²log(1−θ)/(3θ²)
A05	not supplied	1−12(D1(θ)−D2(θ))/θ	1−4(1−D1(θ))/θ
A07	1−θ	(9θ²−6θ−6(θ−1)²log(1−θ))/θ³−3	2(θ²−θ−(θ−1)²log(1−θ))/θ²
A09	3 exp(3/(2θ)) E1(3/(2θ))/(4θ)+θ/3−1/2	not supplied	not supplied
E02	δ²/(2−δ)	3δ/(4−δ)	δ/(2−δ)
A04	not supplied	12/θ ∫₀¹ (t(1−t))^(1/θ−1)/(1+t^(1/θ)+(1−t)^(1/θ))² dt−3	(θ−1)/θ
E06	2α²β/(3α+β−2αβ)	3αβ/(2α−αβ+2β)	αβ/(α−αβ+β)
L01	printed 3/π asin(1/2+r²/(1+r))−1/2 requires correction	6 asin(r/2)/π	2 asin r/π
L02	not supplied	6 E[asin(r Ṽ₁)]/π	2 asin r/π
L03	not supplied	6 E[asin(r Ṽ₂)]/π	2 asin r/π
U01	(α−β)²+αβ	α−β	(α−β)(α+β+2)/3
U02	θ⁴(3θ²+1)/4	θ³	θ³(θ²+2)/3
U03	θ²/15	θ/3	2θ/9
U04	not supplied	printed (θ+1)/(θ−1)−4θ log θ/(θ−1)² requires correction	not supplied
U05	not supplied	δ(4−3δ)/(2−δ)²	2δ/(3−δ)

The mixing laws of Ṽ₁ and Ṽ₂ must be specified as in Heinen–Valdesogo, Proposition 1, before implementing those expectations. The displayed expression alone does not define the random variables. Special functions and integrals in this table must not be advertised as elementary formulas.

Removable cases: AMH and Frank at zero give all three coefficients zero; Nelsen 7 at zero gives (ξ,ρ,τ)=(1,−1,−1) and at one gives (0,0,0); Gumbel–Barnett at zero gives ξ=0; Marshall–Olkin with a zero weight gives all three zero; Plackett at one gives ρ=0. Endpoints with logarithms require limit proofs. Footrule, gamma and beta are additional library targets, not columns supplied by this paper.

Source audit: do not silently transcribe these cells

These observations concern the version linked above, not a claim about every published version. Corrections below are mathematical checks against definitions and special cases, not a published erratum.

1. Gaussian tails at r=−1 must be zero: that copula is W. Table 5 and A.3.3 incorrectly include this endpoint with M. The library already proves W's two tail limits are zero.
2. The printed Gaussian ξ expression is not even in r, is singular at −1, and has an arcsine argument above one for some negative r. The expression to verify from the cited source is 3 asin((1+r²)/2)/π−1/2.
3. The printed Plackett ρ has an extra factor two on its logarithmic term; it fails the independence limit at θ=1. The target to verify is (θ+1)/(θ−1)−2θ log θ/(θ−1)².
4. Fréchet LO decreases in β: increasing the weight of W replaces Π by W≤Π. Table 5/A.4.2 say increasing in both weights. A.4.1 also reverses the simplex inequality, and equation (23) gives the wrong sign for Mardia's β.
5. Density TP2 cannot include M: it has no Lebesgue density. The Fréchet and Mardia TP2 cells conflict with Definition 2.5 and also omit independence.
6. Mardia at θ=0 is Π, hence both CI and CD. The printed CI/CD cells omit it.
7. AMH at θ=1 is H and has lower tail coefficient 1/2, not zero. Its printed generator degenerates at one and must be replaced by H's generator.
8. Nelsen 16 at zero is W, Nelsen 19 at zero is H, and Nelsen 20 at zero is Π. Their lower-tail entries therefore need separate endpoints (0, 1/2, 0).
9. Nelsen 18's inverse-generator cutoff in Table 2 has its inequality reversed. Nelsen 21's cutoff must be one, not π/2.
10. Tawn's Pickands term must be (α(1−t))^θ, with α inside the power. Its numerical non-TP2 claim cannot apply to α=β=1, the Gumbel subfamily. Joe EV's analogous claim must also respect its Galambos subfamily.
11. The second Marshall–Olkin TP2 row cannot exclude α>0, β=0: this is Π. Singular endpoints must be handled independently of density arguments.
12. Raftery's CDF needs the factor 1/(1+δ). Its upper-tail coefficient is zero for δ<1 but equals one at δ=1, where the copula is M.
13. Table 1's Student-t density uses the correlation symbol where the dimension two is needed. The t-EV limits in Table 4 also need checking: the displayed Marshall–Olkin parameter can lie outside [0,1], and a Hüsler–Reiss limit requires an appropriate joint parameter regime.
14. Plackett's negative-side Schur interval ends at one, not zero; θ>0 is its parameter domain. The numerical TP2 observation on [1,2] remains numerical.

Checked implementation and remaining work

The four added families A02, A12, A14 and A15 have measure constructors, Archimedean classification, exact interior CDF theorems and endpoint identifications in Nelsen.lean. Truncated.lean proves the non-strict linear generator; Power.lean proves both generator power transformations. These are genuine validity proofs in dimension two, including singular distributions, without density assumptions.

TailDependence/Joe.lean proves A06's exact tail pair (0,2−2^(1/θ)) for every θ≥1. TailDependence/Nelsen2.lean proves A02's exact tail pair (0,2−2^(1/θ)) for every θ≥1, including θ=1. Nelsen8.lean proves A08's rational generator, printed CDF on the full closed square, and θ=1 lower-Fréchet endpoint. The tail proofs establish the exact pair (0,0). The family module proves increasing lower-orthant parameter order; Nelsen8Limits.lean proves the full-square Clayton-at-one limit as θ→∞. The dependence proofs show non-PQD and non-CI for every θ≥1, exclude CDF-level TP2 and an MTP2 density, and prove CD exactly at θ=1. Schur order and association-coefficient cells remain separate obligations. Nelsen7.lean adds A07 with its CDF on the entire square, CD, increasing LO order and both endpoints. The general density-PQD bridge in Dependence/DensityTotalPositivity.lean also gives both exact total-positivity ranges: only θ=1 (independence) has a TP2 CDF or admits an MTP2 density. The negative Clayton branch covers −1≤θ<0 and identifies −1 with W. The library now has constructors for 19 of the paper's 38 families; both signed Frank branches have exact closed-square CDFs. A constructor count is not a count of fully proved property tables.

Dependence/Clayton.lean proves CI (in both directions) and positive quadrant dependence for every positive Clayton parameter, and negative quadrant dependence throughout −1≤θ<0. The positive-parameter CI proof uses concavity of every first-coordinate CDF section and Archimedean symmetry. The negative-parameter CD entry is proved in Dependence/ClaytonNegative.lean by a convex-section argument across the truncated support. Dependence/ClaytonClassification.lean proves the reverse exclusions by strict midpoint quadrant comparisons, completing the signed CI/CD parameter split. TailDependence/Clayton.lean proves both exact tail coefficients for each signed branch: (2^(−1/θ),0) for θ>0 and (0,0) for −1≤θ<0. The exact CDF-level TP2 region is now checked separately in Dependence/ClaytonTotalPositivity.lean: every θ>0 has a TP2 CDF, θ=0 is independence and has a TP2 CDF, while every −1≤θ<0 fails CDF TP2. The θ=−1 endpoint is W and has no Lebesgue MTP2 density. Dependence/ClaytonDensityFormula.lean also checks MTP2 of the standard positive-parameter density formula as a function. Dependence/ClaytonDensityMeasure.lean identifies that formula with the actual Clayton measure on the full square. Consequently every θ>0 has an actual MTP2 density and is absolutely continuous. Dependence/DensityTotalPositivity.lean proves that any copula with an MTP2 density is PQD, then uses strict non-PQD of negative Clayton to exclude all −1≤θ<0. Thus the signed Clayton density-TP2 range is exactly θ≥0, including the independence parameter.

ConditionalMonotonicity.lean defines CI/CD, proves reflection duality and exact FGM CI/CD regions. FGMKendall.lean proves τ=2θ/9; FGMChatterjee.lean identifies the conditional CDF and proves ξ=θ²/15, completing FGM's three Table 6 entries and all six library rank coefficients. Rank/Frechet.lean proves ρ=α−β and ρ=θ³. Order/Frechet.lean proves the corrected weight ordering and a counterexample to the reversed claim. FGMSchur.lean proves FGM Schur order in either or both directions exactly when the absolute parameters are ordered.

Previously proved family results are indexed in families, positive dependence, orders, rank coefficients, and tail dependence. In particular FGM has exact parameter classification, LO order, an actual MTP2 density exactly for nonnegative parameters, rho/footrule/gamma/beta formulas and both zero tails. The negative exclusion covers every possible density version via the general CD-plus-MTP2 independence theorem. Fréchet and Mardia have both tail formulas. These facts do not establish the remaining table cells.

ExtremeValue/Diagonal.lean proves the power diagonal and extremal coefficient for every bivariate max-stable copula. TailDependence/ExtremeValue.lean now checks both tail formulas for A04 (Gumbel), E02 (Cuadras–Augé), E06 (Marshall–Olkin) and E07 (Tawn). Lower tails at the M endpoints are one; the other parameters have lower tail zero. These include all admitted zero weights and θ=1 cases. Rank/PowerDiagonal.lean also proves their footrule and beta formulas, which supplement the paper's rho/tau/xi table rather than completing its outstanding entries.

Rank/FrechetChatterjee.lean now proves the Table 6 xi formulas for U01 and U02: (α−β)²+αβ and θ⁴(1+3θ²)/4, including the entire simplex and both signed Mardia endpoints. Rank/FrechetKendall.lean proves their tau formulas (α−β)(α+β+2)/3 and θ³(θ²+2)/3, completing the rho/tau/xi entries for both families in Table 6. It also proves footrule, gamma and beta, so all six library coefficients now have formulas for U01 and U02. The shared Kendall mixture API expresses tau as a quadratic form in the weights, with cross terms given by the concordance function Q; its probability interpretation is proved for arbitrary bivariate copulas, including singular ones. The shared mixture API proves exact quadratic identities and strict convexity of xi. The conditional-distance API proves xi=0 iff independence for every bivariate copula, including singular laws.

Dependence/Frechet.lean now proves exact CI/CD classifications and absolute continuity/density TP2 for U01 and U02, including independence and singular endpoints. Frechet is CI iff b=0 and CD iff a=0; Mardia is CI at theta=0,1 and CD at theta=-1,0. Both families have a Lebesgue density exactly at independence, which is also their exact density-TP2 region. These correct the printed singular-endpoint TP2 and omitted independence claims; they do not classify alternative total-positivity notions.

Rank/Nelsen7.lean identifies the conditional CDF and proves A07's Table 6 formula xi=1-theta on the entire closed interval. Order/Nelsen7.lean proves the exact Schur order in both directions: C_theta precedes C_eta iff eta<=theta. The family is CI exactly at independence (theta=1), while CD holds throughout. The full Nelsen 7 rho and tau expressions are proved in Rank/Nelsen7Rho.lean and Rank/Nelsen7Tau.lean, including both endpoint values. The density-TP2 entry is settled by the exact classification above.

Outstanding proof work includes the other named constructors, generator criteria for CI/CD and density TP2, Pickands representation and admissibility, the CI/CD equivalences between LO and Schur order, family parameter orders, analytic tail limits, and the unproved coefficient formulas above. A family is complete only after its domain, boundary cases, CDF, applicable property/order statements and supplied coefficient expressions are linked to checked declarations. Unknown and numerical-only source cells remain separately identified even when the rest of their family is formalized.

Library revision: fe53ea2f · Lean 4.34.0