Research supplements / Articles Search /
Article supplement / 2024

Dependence properties of bivariate copula families

Jonathan Ansari · Marcus Rockel

Dependence Modeling · DOI 10.1515/demo-2024-0002

Journal article ↗arXiv:2310.17307v3 ↗Source folder ↗Lean module ↗
Complete for stated scope

Every cell that arXiv v3 Tables 1–6 states as a result has a verified row: the CDF/constructor, CI/CD region, density TP2, lower-orthant and Schur parameter orders, tail coefficients, the Table 4 special and limiting cases, and the supplied Table 6 formulas, for all 38 families. The same holds for the general results (Section 2.1 representation, Definition 2.3, Lemmas 2.4, 2.6, 2.7, 2.8, 2.10, Propositions 3.1, 3.2, 3.3, Theorem 3.4). Where the printed source is wrong, the corrected statement is verified and the discrepancy is recorded (e.g. AMH lower tail at θ=1, Raftery CDF, Plackett ρ, Gaussian ξ and tails, Fréchet/Mardia weights, the t-EV ν→∞ limit, the blanket Tawn TP2 exclusion). Cells marked ? in the source state no result. Numerical-only (*) observations are verified where a proof or counterexample was found: all Schur * cells, and the Joe-EV/Tawn/t-EV TP2 exclusions at explicit members. The Hüsler–Reiss TP2 claim and the all-parameter EV exclusions are excluded as numerical-only. Numbering follows arXiv v3; publisher-version differences are recorded in SOURCE_COMPARISON.md.

Stable identifier
AnsariRockel2024
Source for numbering
arXiv:2310.17307v3; selected published statements and discrepancies compared in SOURCE_COMPARISON.md
Lean entry point
Papers.AnsariRockel2024.Main

Verification map

Status: complete for scope. Every cell that arXiv v3 Tables 1–6 states as a result has a verified row: the CDF/constructor, CI/CD region, density TP2, lower-orthant and Schur parameter orders, tail coefficients, the Table 4 special and limiting cases, and the supplied Table 6 formulas, for all 38 families. The same holds for the general results (Section 2.1 representation, Definition 2.3, Lemmas 2.4, 2.6, 2.7, 2.8, 2.10, Propositions 3.1, 3.2, 3.3, Theorem 3.4). Where the printed source is wrong, the corrected statement is verified and the discrepancy is recorded (e.g. AMH lower tail at θ=1, Raftery CDF, Plackett ρ, Gaussian ξ and tails, Fréchet/Mardia weights, the t-EV ν→∞ limit, the blanket Tawn TP2 exclusion). Cells marked ? in the source state no result. Numerical-only (*) observations are verified where a proof or counterexample was found: all Schur * cells, and the Joe-EV/Tawn/t-EV TP2 exclusions at explicit members. The Hüsler–Reiss TP2 claim and the all-parameter EV exclusions are excluded as numerical-only. Numbering follows arXiv v3; publisher-version differences are recorded in SOURCE_COMPARISON.md.

The positive-parameter and printed negative-parameter Frank CDFs, Joe, Nelsen 2/8/12/14/15, Gumbel–Hougaard, and Tawn closed-square CDFs, together with the Tawn endpoint identities, are now proved in the pinned copula package. The article declarations below refer directly to those package theorems, so the family formulas have one shared proof.

Source and conventions

Source: arXiv:2310.17307v3. Statement-level differences to the journal version are recorded in SOURCE_COMPARISON.md; they are outside the verified scope.

A copula is represented by its probability measure. The classical representation theorem below proves existence and uniqueness from the classical boundary and rectangle conditions. The FGM CDF is checked explicitly. Fréchet uses weights aa on MM, bb on WW, and 1−a−b1-a-b on independence, with a,b≥0a,b\geq0 and a+b≤1a+b\leq1. Mardia uses a=θ2(1+θ)/2a=\theta^2(1+\theta)/2 and b=θ2(1−θ)/2b=\theta^2(1-\theta)/2. Signed parameters satisfy −1≤θ≤1-1\leq\theta\leq1; singular endpoints are included. CI and CD mean conditional monotonicity in both directions. Rho and tau use the source population normalizations; xi is coordinate 1 given coordinate 0.

The library defines xi using a regular conditional CDF. The bridge to the source's almost-everywhere partial derivative is proved in ConditionalDerivative.lean, without assuming an absolutely continuous copula.

The additional extreme-value tails use actual copula constructors and the power-diagonal limit proofs in the pinned library. The parameters are finite: Gumbel and Tawn have theta>=1; Marshall-Olkin, Cuadras-Auge and Tawn weights include their closed unit intervals. The lower tail at M is treated separately. These tail results do not establish the families' remaining dependence or association-coefficient table cells.

Result map

Every row refers to arXiv v3. Each named declaration is compiled, printed, and checked against the standard axiom allowlist in Axioms.lean.

Source result Lean declaration Status Hypotheses and scope
Section 2.1: classical representation Papers.AnsariRockel2024.classical_representation verified Bivariate classical boundary and rectangle conditions; unique representing measure.
Table 5: FGM CDF Papers.AnsariRockel2024.fgm_cdf verified Entire closed square and signed parameter interval.
Tables 1–2: Clayton CDF, both parameter branches Papers.AnsariRockel2024.clayton_positive_cdf; Papers.AnsariRockel2024.clayton_negative_cdf; Papers.AnsariRockel2024.clayton_positive_zero_axes; Papers.AnsariRockel2024.clayton_negative_zero_axes verified The source formula is checked for every positive θ and every negative θ in [-1,0), throughout the closed square. The negative branch explicitly truncates the base before exponentiation; zero-coordinate CDF values are handled separately, avoiding undefined negative powers of zero.
Table 2: Clayton special and limiting cases Papers.AnsariRockel2024.clayton_negative_one; Papers.AnsariRockel2024.clayton_tendsto_zero; Papers.AnsariRockel2024.clayton_tendsto_atTop verified At θ=-1 the copula equals W. Positive θ tending to zero gives the independence CDF, and θ tending to infinity gives M, at every point of the closed square. These are pointwise CDF limits, not a claim of uniform convergence or rank-coefficient convergence.
Table 2: Clayton θ=1 rational case Papers.AnsariRockel2024.clayton_one_cdf verified On positive coordinates the CDF equals uv/(u+v-uv), with a proved positive denominator. Zero-coordinate values are covered by the separate axis theorem; the undefined 0/0 expression is not used.
Table 2: Ali–Mikhail–Haq CDF Papers.AnsariRockel2024.amh_cdf_full verified The rational formula uv/(1−θ(1−u)(1−v)) is proved for every θ∈[−1,1] and every point of the closed square, including both zero axes and the θ=1 Clayton endpoint. This is a CDF result; Table 3 has separate audited rows below, while the Table 6 association formulas are audited separately below.
Table 3: Ali–Mikhail–Haq quadrant dependence Papers.AnsariRockel2024.amh_pqd_iff; Papers.AnsariRockel2024.amh_nqd_iff verified On the full interval θ∈[−1,1], the actual AMH copula is PQD iff θ≥0 and NQD iff θ≤0. The reverse directions use the exact midpoint CDF. CI/CD, tail coefficients and the full density-TP2 classification have separate audited rows; association formulas are audited separately below.
Correction to arXiv v3 Table 3: Ali–Mikhail–Haq tail pair Papers.AnsariRockel2024.amh_tails_lt_one; Papers.AnsariRockel2024.amh_tails_one verified For −1≤θ<1, the actual lower and upper coefficients are both zero. At θ=1 the copula is Clayton(1), so the pair is (1/2,0). The arXiv v3 Table 3 lower-tail value 0 at θ=1 is false and is not claimed verified. Correspondence of this cell with the journal version has not been checked.
Table 3: Ali–Mikhail–Haq lower-orthant parameter order Papers.AnsariRockel2024.amh_lowerOrthant_iff verified For θ,η∈[−1,1], Cθ≤LO Cη iff θ≤η. The forward implication follows from the exact rational CDF throughout the square; the converse uses the midpoint CDF 1/(4−θ). This row does not assert the source's Schur order.
Table 3: Ali–Mikhail–Haq exact CI/CD regions Papers.AnsariRockel2024.amh_ci_iff; Papers.AnsariRockel2024.amh_cd_iff verified Over the complete θ∈[−1,1] interval, CI iff θ≥0 and CD iff θ≤0, including independence at θ=0 and the Clayton(1) endpoint. The proof establishes the actual conditional CDF section curvature in both coordinate directions; it does not claim a Lebesgue TP2 density.
Table 3: Ali–Mikhail–Haq Schur parameter order Papers.AnsariRockel2024.amh_schur_nonnegative_iff; Papers.AnsariRockel2024.amh_schur_nonpositive_iff verified For θ,η∈[0,1], the actual two-direction Schur comparison Cθ≤S Cη holds iff θ≤η. For θ,η∈[−1,0], it holds iff η≤θ. These are the two same-sign ranges stated in arXiv v3 Table 3; cross-sign comparisons are not asserted. The result uses the article's general CI/CD Schur–orthant equivalence and the package's full-range AMH CI/CD and lower-orthant proofs.
Additional Ali–Mikhail–Haq CDF total positivity Papers.AnsariRockel2024.amh_cdf_tp2_iff verified On θ∈[−1,1], the actual CDF is TP2 iff θ≥0, including both endpoints and all square boundaries. This is CDF-level TP2, separate from the source's Lebesgue-density TP2 cell.
Table 3: Ali–Mikhail–Haq density TP2 cases Papers.AnsariRockel2024.amh_zero; Papers.AnsariRockel2024.amh_negative_not_mtp2_density; Papers.AnsariRockel2024.amh_zero_mtp2_density; Papers.AnsariRockel2024.amh_one_mtp2_density verified Every θ<0 lacks an MTP2 Lebesgue density; θ=0 is independence and θ=1 is Clayton(1), each with an actual MTP2 density. The positive interior is proved in the next row.
Table 3: complete Ali–Mikhail–Haq density TP2 classification Papers.AnsariRockel2024.amh_density_formula; Papers.AnsariRockel2024.amh_density_tp2_iff verified On the full signed interval, an actual MTP2 Lebesgue density exists iff θ≥0. For 0≤θ<1 the continuous rational formula is identified with the copula measure by two integrations; its numerator and reciprocal denominator are TP2. The singular analytic formula at θ=1 is handled separately by the proved Clayton(1) density. No density hypothesis is assumed.
Table 3: positive Clayton CI/CD region Papers.AnsariRockel2024.clayton_positive_ci; Papers.AnsariRockel2024.clayton_positive_not_cd verified Every θ>0 is CI and not CD. CDF-section concavity and Archimedean symmetry prove CI; a strict midpoint comparison with independence excludes CD. The actual positive-parameter density-TP2 result is verified below.
Table 3: positive Clayton quadrant dependence Papers.AnsariRockel2024.clayton_positive_pqd verified Every θ>0 has C(u,v)≥uv on the closed square. This follows from the now verified CI entry; density TP2 is now verified below. The proof lives in the pinned copula package.
Table 3: Clayton parameter endpoints Papers.AnsariRockel2024.clayton_zero_ci_cd; Papers.AnsariRockel2024.clayton_negative_one_cd verified At θ=0 the independence copula is both CI and CD. At θ=−1 the negative Clayton copula equals W and is CD. The full negative interval is verified in the next row.
Table 3: negative Clayton CI/CD region Papers.AnsariRockel2024.clayton_negative_cd; Papers.AnsariRockel2024.clayton_negative_not_ci verified Every θ in [−1,0) is CD and not CI. CDF-section convexity across the truncation boundary and Archimedean symmetry prove CD; a strict midpoint comparison with independence excludes CI. The full negative-parameter density-TP2 exclusion is verified below.
Table 3: negative Clayton quadrant dependence Papers.AnsariRockel2024.clayton_negative_nqd verified Every θ in [-1,0) has C(u,v)≤uv on the closed square, including W at θ=-1. This follows from the now verified CD entry. The proof lives in the pinned copula package.
Additional Clayton CDF total-positivity classification Papers.AnsariRockel2024.clayton_positive_cdf_tp2; Papers.AnsariRockel2024.clayton_zero_cdf_tp2; Papers.AnsariRockel2024.clayton_negative_not_cdf_tp2 verified The CDF is TP2 for θ≥0 and fails TP2 for −1≤θ<0, including the W endpoint. This is a separate CDF property; the positive-parameter density-TP2 claim is verified below.
Table 3: Clayton θ=−1 density TP2 exclusion Papers.AnsariRockel2024.clayton_negative_one_not_density_tp2 verified At θ=−1 the copula is W, which is singular and has no Lebesgue MTP2 density. The broader negative-parameter exclusion is verified in the next row.
General bridge: MTP2 copula density implies PQD Papers.AnsariRockel2024.hasMTP2Density_isPQD verified Successive nonnegative integration of the pointwise TP2 inequality gives a four-quadrant mass determinant for the actual withDensity measure. Uniform copula marginals turn it into C(u,v) ≥ uv for every point. The argument applies to any measurable nonnegative MTP2 density version, including densities modified on null sets.
Table 3: negative Clayton density TP2 exclusion Papers.AnsariRockel2024.clayton_negative_not_density_tp2 verified Every θ in [−1,0) fails HasMTP2Density: an MTP2 density would force PQD, while negative Clayton is strictly non-PQD. This includes every interior parameter and the singular W endpoint; no absolute-continuity assumption is used. Together with the positive-parameter theorem and independence, the signed Clayton density-TP2 range is exactly θ≥0.
Table 3: positive Clayton analytic density candidate Papers.AnsariRockel2024.clayton_cdf_positive_eq_analytic; Papers.AnsariRockel2024.clayton_cdf_formula_hasDerivAt_first; Papers.AnsariRockel2024.clayton_cdf_formula_hasDerivAt_second; Papers.AnsariRockel2024.clayton_mixed_derivative_eq_densityFormula verified On strictly positive unit coordinates, the actual Clayton CDF equals its analytic formula, and the formula’s first and mixed derivatives are evaluated. The mixed derivative is exactly the pinned package’s nonnegative MTP2 candidate. This is pointwise calculus; global equality of the candidate density measure with the actual copula measure is proved below.
Table 3: positive Clayton density on positive rectangles Papers.AnsariRockel2024.clayton_density_formula_integral_second; Papers.AnsariRockel2024.clayton_cdf_formula_integral_first; Papers.AnsariRockel2024.clayton_density_formula_positive_rectangle; Papers.AnsariRockel2024.clayton_density_formula_positive_rectangle_eq_measure; Papers.AnsariRockel2024.clayton_densityFormula_positive_rectangle_eq_measure; Papers.AnsariRockel2024.clayton_withDensity_positive_rectangle_eq_measure; Papers.AnsariRockel2024.clayton_density_formula_cutoff_square; Papers.AnsariRockel2024.clayton_density_formula_cutoff_square_bounds; Papers.AnsariRockel2024.clayton_density_formula_cutoff_square_tendsto_one; Papers.AnsariRockel2024.clayton_density_formula_positive_rectangle_cdf_bounds; Papers.AnsariRockel2024.clayton_density_formula_cutoff_rectangle_tendsto_cdf verified The pinned package density candidate itself integrates over every positive half-open unit-square rectangle to the actual copula mass, and its withDensity measure agrees there; the matching analytic real-coordinate integral equals the four-corner CDF increment. The one-coordinate FTC identities and cutoff-square bounds are also checked; its integral lies between 1−2r and 1−r, hence tends to one as the positive cutoff vanishes. More generally, a rectangle with equal vanishing lower cutoffs has candidate-density integral tending to its upper-corner Clayton CDF. Global measure equality is proved below by monotone cutoff rectangles and nullity of the coordinate axes.
Table 3: positive Clayton density TP2 and absolute continuity Papers.AnsariRockel2024.clayton_withDensity_axis_zero; Papers.AnsariRockel2024.clayton_withDensity_positive_lowerOrthant_eq_measure; Papers.AnsariRockel2024.clayton_withDensity_lowerOrthant_eq_measure; Papers.AnsariRockel2024.clayton_toMeasure_eq_withDensity_positive; Papers.AnsariRockel2024.clayton_positive_density_tp2; Papers.AnsariRockel2024.clayton_positive_absolutelyContinuous verified For every θ>0, the pinned explicit formula is a measurable, nonnegative MTP2 density of the actual Clayton copula measure on the full closed unit square. Positive rectangles exhaust lower orthants, both coordinate axes are null, and CDF uniqueness identifies the full measures. Absolute continuity follows. Together with the negative exclusion above and the independence case, this gives the full signed density-TP2 classification.
Table 3: positive Clayton tail pair Papers.AnsariRockel2024.clayton_positive_lower_tail; Papers.AnsariRockel2024.clayton_positive_upper_tail verified For every θ>0, (λL,λU)=(2^(−1/θ),0). The lower coefficient follows from the exact diagonal ratio; the upper coefficient follows from the diagonal derivative at one.
Table 3: negative Clayton tail pair Papers.AnsariRockel2024.clayton_negative_lower_tail; Papers.AnsariRockel2024.clayton_negative_upper_tail verified For every θ in [−1,0), both coefficients are zero. A general package theorem proves NQD forces zero lower and upper tail coefficients. The θ=0 independence case is already covered by the package.
Section 2.4: derivative formula for xi Papers.AnsariRockel2024.xi_derivative_formula verified All bivariate copulas; almost-everywhere correspondence with the conditional CDF.
Table 6, FGM, Spearman rho Papers.AnsariRockel2024.fgm_rho verified Full signed interval, including zero and both endpoints.
Table 6, FGM, Kendall tau Papers.AnsariRockel2024.fgm_tau verified Full signed interval, including zero and both endpoints.
Table 6, FGM, Chatterjee xi Papers.AnsariRockel2024.fgm_xi verified Full signed interval, including zero and both endpoints.
Table 6, Frechet, Spearman rho Papers.AnsariRockel2024.frechet_rho verified Full weight simplex, including singular endpoints.
Table 6, Frechet, Kendall tau Papers.AnsariRockel2024.frechet_tau verified Full weight simplex, including singular endpoints.
Table 6, Frechet, Chatterjee xi Papers.AnsariRockel2024.frechet_xi verified Full weight simplex, including singular endpoints.
Table 6, Mardia, Spearman rho Papers.AnsariRockel2024.mardia_rho verified Full signed interval; nonnegative W-weight as specified above.
Table 6, Mardia, Kendall tau Papers.AnsariRockel2024.mardia_tau verified Full signed interval; nonnegative W-weight as specified above.
Table 6, Mardia, Chatterjee xi Papers.AnsariRockel2024.mardia_xi verified Full signed interval; nonnegative W-weight as specified above.
Table 5 / Appendix A.4.1: FGM CI Papers.AnsariRockel2024.fgm_ci verified Full signed interval, including zero and both endpoints.
Table 5 / Appendix A.4.1: FGM CD Papers.AnsariRockel2024.fgm_cd verified Full signed interval, including zero and both endpoints.
Table 5 / Appendix A.4.2: FGM lower orthant order Papers.AnsariRockel2024.fgm_lowerOrthant verified Full signed interval, including zero and both endpoints.
Table 5 / Appendix A.4.3: FGM lower and upper tails Papers.AnsariRockel2024.fgm_tails verified Full signed interval, including zero and both endpoints.
Table 5 / Appendix A.4.3: Frechet tails Papers.AnsariRockel2024.frechet_tails verified Full weight simplex, including singular endpoints.
Table 5 / Appendix A.4.3: Mardia tails Papers.AnsariRockel2024.mardia_tails verified Full signed interval; nonnegative W-weight as specified above.
Table 5 / Appendix A.4.1: FGM density Papers.AnsariRockel2024.fgm_density verified Actual copula measure equals Lebesgue measure with the displayed continuous density; all signed parameters.
Table 5 / Appendix A.4.1: FGM density TP2 Papers.AnsariRockel2024.fgm_density_tp2_iff; Papers.AnsariRockel2024.fgm_has_tp2_density verified The displayed density is TP2 iff theta>=0; for nonnegative theta it supplies a HasMTP2Density witness. No claim about TP2 of the CDF is substituted for density TP2.
General bridge: CD plus MTP2 density Papers.AnsariRockel2024.isCD_eq_independence_of_hasMTP2Density verified Any conditionally decreasing copula with an actual MTP2 Lebesgue density is independence: CD gives NQD, density MTP2 gives PQD, and both quadrant orders determine the product copula.
General bridge: CD plus CDF TP2 Papers.AnsariRockel2024.isCD_eq_independence_of_isTP2CDF verified CDF-level TP2 gives PQD while CD gives NQD, so both force independence. This does not use a density.
Nelsen 7 CDF TP2 range Papers.AnsariRockel2024.nelsen7_cdf_tp2_iff verified CDF-level TP2 holds iff θ=1 on the full closed interval, including the countermonotonic endpoint. This is distinct from the density-TP2 classification.
Table 3: Nelsen 7 density TP2 range Papers.AnsariRockel2024.nelsen7_density_tp2_iff verified Over the full parameter interval [0,1], an actual MTP2 density exists iff θ=1 (independence). Every θ<1 is CD but not independence, so the general bridge excludes any MTP2 density version, including the singular endpoint.
Table 5: FGM actual MTP2-density range Papers.AnsariRockel2024.fgm_hasMTP2Density_iff verified Over the full signed parameter interval [-1,1], the actual FGM copula has some MTP2 Lebesgue density iff θ≥0. The existing explicit polynomial is a witness for θ≥0. For θ<0, CD plus an MTP2 density would force independence, contradicting the exact FGM CI classification. This rules out every alternative density version, strengthening the displayed-formula classification above.
Tables 1-2: Nelsen 7 CDF and endpoints Papers.AnsariRockel2024.nelsen7_cdf; Papers.AnsariRockel2024.nelsen7_endpoints verified Entire square and theta in [0,1], including W at zero and independence at one.
Table 3 / Appendix A.1.1: Nelsen 7 CD Papers.AnsariRockel2024.nelsen7_cd verified Conditional decreasingness in both directions for every theta in [0,1].
Table 3 / Appendix A.1.2: Nelsen 7 lower orthant order Papers.AnsariRockel2024.nelsen7_lowerOrthant_iff verified Comparison holds iff the parameters are ordered; full closed parameter interval.
Table 3: Nelsen 7 tail dependence Papers.AnsariRockel2024.nelsen7_tails verified Both limits exist and equal zero, including both parameter endpoints.
Tables 1-2: Nelsen 2 CDF and lower-bound endpoint Papers.AnsariRockel2024.nelsen2_cdf_full; Papers.AnsariRockel2024.nelsen2_one verified The truncated-power source formula on the closed square for every finite theta>=1; theta=1 is W.
Table 2: Nelsen 2 infinite-parameter endpoint Papers.AnsariRockel2024.nelsen2_tendsto_atTop verified For any admissible real parameter path tending to infinity, the actual CDF converges pointwise to M on every point of the closed square, including both axes. This does not assert uniform convergence or convergence of rank coefficients.
Tables 1-2: Nelsen 8 CDF and lower-bound endpoint Papers.AnsariRockel2024.nelsen8_cdf_full; Papers.AnsariRockel2024.nelsen8_one verified The paper's printed rational CDF holds on every point of the closed square for finite θ≥1; the denominator is strictly positive and θ=1 is W. Nelsen 8 Schur ordering and association-coefficient cells remain open.
Table 3: Joe tail pair Papers.AnsariRockel2024.joe_tails verified For every finite θ≥1, both limits exist: lower 0 and upper 2−2^(1/θ), including the θ=1 independence endpoint.
Table 3: Nelsen 8 lower-orthant parameter order Papers.AnsariRockel2024.nelsen8_lowerOrthant verified For all finite 1≤θ≤η, Cθ≤LO Cη on the entire closed square. This does not establish the separate Schur order.
Table 3: Nelsen 8 non-PQD and non-CI Papers.AnsariRockel2024.nelsen8_not_pqd; Papers.AnsariRockel2024.nelsen8_not_ci verified For every finite θ≥1 a strictly positive diagonal point has CDF zero, ruling out PQD and therefore CI. This includes the θ=1 lower-Fréchet endpoint.
Table 3: Nelsen 8 TP2 exclusions Papers.AnsariRockel2024.nelsen8_not_tp2_cdf; Papers.AnsariRockel2024.nelsen8_not_mtp2_density verified For every finite θ≥1 neither the CDF is TP2 nor does the actual copula admit an MTP2 Lebesgue density. These are separate properties; both exclusions follow from the formally proved non-PQD witness.
Table 2: Nelsen 8 infinite-parameter endpoint Papers.AnsariRockel2024.nelsen8_tendsto_atTop verified For any admissible real parameter path tending to infinity, the actual Nelsen 8 CDF converges pointwise to Clayton at parameter one on the entire closed square. This does not assert uniform convergence or convergence of rank coefficients.
Table 3: Nelsen 8 exact CD range Papers.AnsariRockel2024.nelsen8_cd_one; Papers.AnsariRockel2024.nelsen8_not_cd; Papers.AnsariRockel2024.nelsen8_cd_iff verified The copula is CD exactly at θ=1. For every θ>1, a fixed chord at v=1/2, u=1/2,3/4,1 violates convexity by a strictly positive rational expression.
Table 3: Nelsen 8 tail pair Papers.AnsariRockel2024.nelsen8_tails verified For every finite θ≥1, both lower and upper tail limits exist and equal zero, including the θ=1 countermonotonic endpoint.
Table 3: Nelsen 2 lower-orthant parameter order Papers.AnsariRockel2024.nelsen2_lowerOrthant verified For all finite 1≤θ≤η, Cθ≤LO Cη on the entire closed square, by the two-coordinate real Lp norm inequality. This does not establish the separate numerically suggested Schur order.
Table 3: Nelsen 2 exact CI/CD range Papers.AnsariRockel2024.nelsen2_not_pqd; Papers.AnsariRockel2024.nelsen2_not_ci; Papers.AnsariRockel2024.nelsen2_not_cd; Papers.AnsariRockel2024.nelsen2_cd_one; Papers.AnsariRockel2024.nelsen2_cd_iff verified Every finite θ≥1 has a positive diagonal point with CDF zero, excluding PQD and CI. CD holds exactly at θ=1; at θ>1 the positive upper-tail coefficient contradicts the zero upper-tail limit forced by CD.
Table 3: Nelsen 2 TP2 exclusions Papers.AnsariRockel2024.nelsen2_not_tp2_cdf; Papers.AnsariRockel2024.nelsen2_not_mtp2_density verified For every finite θ≥1, neither the CDF is TP2 nor does the actual copula admit an MTP2 Lebesgue density; each would imply PQD.
Table 3: Nelsen 2 tail pair Papers.AnsariRockel2024.nelsen2_tails verified For every finite θ≥1, both limits exist: lower 0 and upper 2−2^(1/θ), including the θ=1 countermonotonic endpoint.
Table 3: Nelsen 12 and 14 dependence at θ=1 Papers.AnsariRockel2024.nelsen12_ci_one; Papers.AnsariRockel2024.nelsen14_ci_one; Papers.AnsariRockel2024.nelsen12_tp2_cdf_one; Papers.AnsariRockel2024.nelsen14_tp2_cdf_one; Papers.AnsariRockel2024.nelsen12_mtp2_density_one; Papers.AnsariRockel2024.nelsen14_mtp2_density_one; Papers.AnsariRockel2024.nelsen12_not_cd_one; Papers.AnsariRockel2024.nelsen14_not_cd_one verified At θ=1 each actual copula is Clayton(1), so each is CI, its CDF is TP2, it has an MTP2 Lebesgue density, and it is not CD. These endpoint identities are supplemented below by CI, CDF and density TP2, and non-CD results on the full finite parameter range.
Table 3: Nelsen 12 and 14 non-CD and PQD Papers.AnsariRockel2024.nelsen12_not_cd; Papers.AnsariRockel2024.nelsen14_not_cd; Papers.AnsariRockel2024.nelsen12_pqd; Papers.AnsariRockel2024.nelsen14_pqd verified Neither family is CD for any finite θ≥1: CD implies NQD and hence zero lower-tail dependence, contradicting the proved positive exact coefficients. Nelsen 12 is PQD for all θ≥1 by its lower-orthant order above Clayton(1). Nelsen 14 is PQD throughout the same range by a direct full-square power-norm inequality. CI and actual density TP2 on the full parameter range are established separately below.
CDF-level TP2 for BB1, Gumbel and max-product families Papers.AnsariRockel2024.nelsen12_tp2_cdf; Papers.AnsariRockel2024.nelsen14_tp2_cdf; Papers.AnsariRockel2024.gumbel_tp2_cdf; Papers.AnsariRockel2024.tawn_tp2_cdf; Papers.AnsariRockel2024.marshallOlkin_tp2_cdf; Papers.AnsariRockel2024.cuadrasAuge_tp2_cdf verified For all admissible finite shape and weight parameters, the actual CDFs are TP2 on the closed square. BB1 and Gumbel follow from log-convex inverse generators; Tawn and common-shock families follow from max-product preservation. This is CDF-level total positivity only. It does not verify the article's separate density-level TP2 classifications for the remaining parameter ranges.
Table 3: Nelsen 12 tail pair Papers.AnsariRockel2024.nelsen12_tails verified For every finite θ≥1, lower=2^(−1/θ) and upper=2−2^(1/θ), including θ=1. Both are limits of the actual copula's diagonal.
Table 3: Nelsen 12 lower-orthant parameter order Papers.AnsariRockel2024.nelsen12_lowerOrthant verified For every finite 1≤θ≤η, Cθ≤LO Cη throughout the closed square. This uses the real two-coordinate power-norm inequality. Both-direction Schur order is established separately below.
Table 2: Nelsen 12 infinite-parameter endpoint Papers.AnsariRockel2024.nelsen12_tendsto_atTop verified For any admissible real parameter path tending to infinity, the actual CDF converges pointwise to M throughout the closed square, including grounded axes. No uniform or rank-coefficient convergence is asserted.
Tables 1-2: Nelsen 12 CDF and Clayton endpoint Papers.AnsariRockel2024.nelsen12_cdf_full; Papers.AnsariRockel2024.nelsen12_one verified The source inverse-power formula with grounded zero axes for every finite theta>=1; theta=1 is Clayton(1).
Table 2: Nelsen 14 infinite-parameter endpoint Papers.AnsariRockel2024.nelsen14_tendsto_atTop verified For every admissible real parameter path tending to infinity, the actual CDF converges pointwise to M throughout the closed square, including grounded axes. No uniform or rank-coefficient convergence is asserted.
Table 3: Nelsen 14 tail pair Papers.AnsariRockel2024.nelsen14_tails verified For every finite θ≥1, lower=1/2 and upper=2−2^(1/θ), including θ=1. The upper result follows from the derivative of the grounded diagonal at one.
Tables 1-2: Nelsen 14 CDF and Clayton endpoint Papers.AnsariRockel2024.nelsen14_cdf_full; Papers.AnsariRockel2024.nelsen14_one verified The source reciprocal-parameter formula with grounded zero axes for every finite theta>=1; theta=1 is Clayton(1).
Table 2: Genest–Ghoudi infinite-parameter endpoint Papers.AnsariRockel2024.genestGhoudi_tendsto_atTop verified For every admissible real parameter path tending to infinity, the actual CDF converges pointwise to M throughout the closed square, including grounded axes. No uniform or rank-coefficient convergence is asserted.
Table 3: Genest–Ghoudi CI/CD classification Papers.AnsariRockel2024.genestGhoudi_not_ci; Papers.AnsariRockel2024.genestGhoudi_cd_iff verified Every finite θ≥1 fails CI, and CD holds exactly at θ=1. The θ=1 member is the countermonotonic copula; positive upper-tail dependence rules out CD for θ>1.
Table 3: Genest–Ghoudi TP2 exclusion Papers.AnsariRockel2024.genestGhoudi_not_tp2_cdf; Papers.AnsariRockel2024.genestGhoudi_not_mtp2_density verified Neither the actual CDF is TP2 nor does the actual copula admit an MTP2 Lebesgue density, for any finite θ≥1.
Genest–Ghoudi positive-quadrant exclusion Papers.AnsariRockel2024.genestGhoudi_not_pqd verified A strictly positive diagonal point has zero CDF for every finite θ≥1, so the actual copula is not PQD.
Table 3: Genest–Ghoudi tail pair Papers.AnsariRockel2024.genestGhoudi_tails verified For every finite θ≥1, lower=0 and upper=2−2^(1/θ), including the θ=1 countermonotonic endpoint. Both are actual diagonal limits.
Tables 1-2: Genest-Ghoudi CDF and lower-bound endpoint Papers.AnsariRockel2024.genestGhoudi_cdf_full; Papers.AnsariRockel2024.genestGhoudi_one verified The source inner/outer-power formula on the closed square for every finite theta>=1; theta=1 is W.
Table 2: Joe infinite-parameter endpoint Papers.AnsariRockel2024.joe_tendsto_atTop verified For any admissible real parameter path tending to infinity, the actual CDF converges pointwise to M on the entire closed square, including grounded axes. No uniform or rank-coefficient convergence is asserted.
Tables 1-2: Joe CDF and independence endpoint Papers.AnsariRockel2024.joe_cdf_full; Papers.AnsariRockel2024.joe_one verified The printed power formula for all finite theta>=1 and positive coordinates, with grounded zero-axis extension; theta=1 is independence.
Table 1: Frank CDF, positive parameter branch Papers.AnsariRockel2024.frank_positive_cdf_full verified For every θ>0, the source logarithmic formula holds on positive coordinates and the grounded value is zero on both axes.
Table 1: Frank CDF, negative parameter branch Papers.AnsariRockel2024.frank_negative_cdf_source; Papers.AnsariRockel2024.frank_negative_cdf_reflected verified For every θ<0, the actual reflected copula has the exact printed logarithmic CDF on the entire closed square, including axes and edges.
Table 3: Frank exact CI/CD split Papers.AnsariRockel2024.frank_positive_ci; Papers.AnsariRockel2024.frank_positive_not_cd; Papers.AnsariRockel2024.frank_negative_cd; Papers.AnsariRockel2024.frank_negative_not_ci; Papers.AnsariRockel2024.frank_zero_ci_cd verified Positive parameters are CI and not CD; negative parameters are CD and not CI. Independence at zero has both properties. Concavity is proved for actual CDF sections, reflection gives the negative branch, and a boundary derivative rules out independence at every nonzero parameter.
Table 3: Frank quadrant dependence and negative density TP2 exclusion Papers.AnsariRockel2024.frank_positive_quadrant; Papers.AnsariRockel2024.frank_negative_quadrant; Papers.AnsariRockel2024.frank_negative_not_density_tp2 verified Positive parameters are PQD and not NQD; negative parameters are NQD and not PQD. No negative Frank copula admits any TP2 Lebesgue density version. Positive-parameter density TP2 is covered by the separate density row below.
Table 3: Frank full density-TP2 classification Papers.AnsariRockel2024.frank_positive_density; Papers.AnsariRockel2024.frank_positive_density_tp2; Papers.AnsariRockel2024.frank_density_tp2_iff; Papers.AnsariRockel2024.frank_ci_iff; Papers.AnsariRockel2024.frank_cd_iff verified An explicit continuous TP2 density is integrated twice to identify the actual positive Frank measure. For the unified signed family, existence of a TP2 density and CI each hold iff θ≥0; CD holds iff θ≤0. The zero member is independence and the negative member is the established reflected Frank copula.
Table 3: Frank tail pair, full real parameter range Papers.AnsariRockel2024.frank_positive_tails; Papers.AnsariRockel2024.frank_negative_tails; Papers.AnsariRockel2024.frank_zero_tails verified Both tail limits exist and equal zero for every finite positive and negative parameter, and for independence at zero. The proof differentiates the actual diagonal at both endpoints; no density or parameter-continuity assumption is used.
Table 1: Frank infinite-parameter endpoints Papers.AnsariRockel2024.frank_cdf_lower_bound; Papers.AnsariRockel2024.frank_tendsto_atTop; Papers.AnsariRockel2024.frank_tendsto_atBot verified Along any positive parameter path tending to +∞, the CDF converges to M on the full closed square, using the global bound min(u,v)−log(2)/θ≤Cθ(u,v)≤min(u,v). Reflection proves convergence to W along every negative path tending to −∞.
Table 1: Frank two-sided independence limit Papers.AnsariRockel2024.frankSigned_cdf_regular; Papers.AnsariRockel2024.frank_continuousAt_zero; Papers.AnsariRockel2024.frank_tendsto_zero verified The actual signed Frank CDF is continuous at θ=0 on the whole closed square and converges to the independence CDF along any real parameter path tending to zero, including paths that change sign or hit zero. The analytic quotient is regularized by derivative-extended difference quotients of exp and log.
Table 1: Frank zero-parameter case Papers.AnsariRockel2024.frank_zero_cdf verified At θ=0, the specified family member is independence and has product CDF on the entire closed square. The two-sided independence limit is verified in the separate continuity row below.
Table 3: Gumbel-Hougaard lower-orthant parameter order Papers.AnsariRockel2024.gumbel_lowerOrthant verified For all finite 1≤θ≤η, Cθ≤LO Cη on the entire closed square by the logarithmic two-coordinate power-norm inequality. The separate Schur-order cell is now covered below.
Table 2: Gumbel-Hougaard infinite-parameter endpoint Papers.AnsariRockel2024.gumbel_tendsto_atTop verified For any admissible real parameter path tending to infinity, the actual CDF converges pointwise to M on the entire closed square, including grounded axes. No uniform or rank-coefficient convergence is asserted.
Table 2: Gumbel–Hougaard independence endpoint Papers.AnsariRockel2024.gumbel_one verified At θ=1, the actual copula equals independence, including all boundary coordinates.
Table 1: Gumbel-Hougaard CDF Papers.AnsariRockel2024.gumbel_cdf_full verified The source logarithmic formula on positive coordinates, with grounded zero-axis extension, for all finite theta>=1.
Table 3 / Appendix A.1.3: Gumbel-Hougaard tails Papers.AnsariRockel2024.gumbel_tails verified Both limits exist for every finite theta>=1: lower=0, upper=2-2^(1/theta). Includes theta=1.
Table 5 / Appendix A.2.3: Marshall-Olkin tails Papers.AnsariRockel2024.marshallOlkin_tails verified Both limits for all alpha,beta in [0,1]: upper=min(alpha,beta), lower=1 exactly at alpha=beta=1, otherwise 0. Singular and zero-weight parameters included.
Table 5 / Appendix A.2.3: Cuadras-Auge tails Papers.AnsariRockel2024.cuadrasAuge_tails verified Both limits for every delta in [0,1]: upper=delta; lower=1 at delta=1 (M), otherwise 0.
Table 1: Tawn CDF Papers.AnsariRockel2024.tawn_cdf_positive; Papers.AnsariRockel2024.tawn_cdf_full verified The source power-exponential formula for positive coordinates and its grounded zero-axis extension, for all finite theta>=1 and weights in [0,1], including endpoints.
Table 1: Tawn endpoint and weight-axis reductions Papers.AnsariRockel2024.tawn_zero_zero; Papers.AnsariRockel2024.tawn_one_one; Papers.AnsariRockel2024.tawn_zero_left; Papers.AnsariRockel2024.tawn_zero_right; Papers.AnsariRockel2024.tawn_shape_one verified Zero weights or shape theta=1 yield independence for all admissible remaining parameters; two unit weights recover Gumbel-Hougaard. Includes every boundary coordinate and zero base.
Table 5 / Appendix A.2.3: Tawn tails Papers.AnsariRockel2024.tawn_tails verified Both limits for finite theta>=1 and alpha,beta in [0,1]: lower=0, upper=alpha+beta-(alpha^theta+beta^theta)^(1/theta). All zero weights and theta=1 included; no infinite-parameter substitution.
Table 5 / Appendix A.4.2: exact FGM Schur order Papers.AnsariRockel2024.fgm_schur_iff verified Schur comparison in both directions iff abs(theta)<=abs(eta), on the full signed parameter interval [-1,1]. The order uses the continuous convex-test characterization of conditional-CDF majorization.
Table 5 / Appendix A.4.2: corrected Frechet parameter order Papers.AnsariRockel2024.frechet_parameter_order verified On the full valid weight simplex, increasing the M weight and decreasing the W weight increases the copula in lower orthant order. This corrects the printed direction for the W weight; no characterization of all comparable weight pairs is claimed.
Table 5 / Appendix A.4.2: counterexample to printed Frechet order Papers.AnsariRockel2024.frechet_order_counterexample verified At fixed M weight zero, raising W's weight from zero to one gives independence then W; independence is not below W in lower orthant order.
Table 5 / Appendix A.4.1: Frechet CI Papers.AnsariRockel2024.frechet_ci_iff verified Full valid weight simplex: CI iff the W weight b is zero; both conditioning directions and all endpoints.
Table 5 / Appendix A.4.1: Frechet CD Papers.AnsariRockel2024.frechet_cd_iff verified Full valid weight simplex: CD iff the M weight a is zero; both conditioning directions and all endpoints.
Support for the density-TP2 correction: Frechet absolute continuity Papers.AnsariRockel2024.frechet_absolutelyContinuous_iff verified The actual copula measure is absolutely continuous with respect to square Lebesgue measure iff a=b=0. Positive M or W weight charges a Lebesgue-null diagonal.
Correction to Table 5 / Appendix A.4.1: Frechet density TP2 Papers.AnsariRockel2024.frechet_density_tp2_iff verified Under the literal Lebesgue-density definition, HasMTP2Density iff a=b=0 (independence). The singular M endpoint has no Lebesgue density.
Correction to Table 5 / Appendix A.4.1: Mardia CI Papers.AnsariRockel2024.mardia_ci_iff verified Full signed interval [-1,1]: CI iff theta=0 or theta=1. Includes the independence case omitted in the printed classification.
Correction to Table 5 / Appendix A.4.1: Mardia CD Papers.AnsariRockel2024.mardia_cd_iff verified Full signed interval [-1,1]: CD iff theta=0 or theta=-1. Includes the independence case omitted in the printed classification.
Support for the density-TP2 correction: Mardia absolute continuity Papers.AnsariRockel2024.mardia_absolutelyContinuous_iff verified Full signed interval: the actual copula measure is absolutely continuous with respect to square Lebesgue measure iff theta=0.
Correction to Table 5 / Appendix A.4.1: Mardia density TP2 Papers.AnsariRockel2024.mardia_density_tp2_iff verified Full signed interval: HasMTP2Density iff theta=0 (independence), with the valid nonnegative W weight.
Table 5 / Appendix A.4.2: Mardia lack of parameter ordering Papers.AnsariRockel2024.mardia_not_lowerOrthant_ordered verified The copulas at theta=0 and theta=1/2 are incomparable in lower orthant order. Explicit CDF witnesses at (1/8,1/8) and (1/8,7/8) rule out the two directions.
Table 6 / Appendix A.5.1: Nelsen 7 conditional CDF Papers.AnsariRockel2024.nelsen7_conditionalCDF verified For every theta,v in [0,1], the actual conditional CDF equals the step with height thetav+1-theta and, when that height is positive, cutoff (1-theta)(1-v)/(theta*v+1-theta), almost everywhere in the conditioning coordinate. At zero height the profile is identically zero.
Table 6 / Appendix A.5.1: Nelsen 7 derivative correspondence Papers.AnsariRockel2024.nelsen7_derivative verified The same step equals the first partial derivative almost everywhere, using the general conditional-CDF bridge; no density hypothesis.
Table 6 / Appendix A.5.1: Nelsen 7 Spearman rho Papers.AnsariRockel2024.nelsen7_integral_cdf_first; Papers.AnsariRockel2024.nelsen7_rho_integral; Papers.AnsariRockel2024.nelsen7_rho_interior; Papers.AnsariRockel2024.nelsen7_rho verified The CDF is integrated exactly over one coordinate, then the resulting rational integral is evaluated to the printed logarithmic expression for 0<theta<1. The countermonotonic and independence endpoints are -1 and 0 respectively.
Table 6 / Appendix A.5.1: Nelsen 7 Kendall tau Papers.AnsariRockel2024.nelsen7_tau_rho; Papers.AnsariRockel2024.nelsen7_tau_interior; Papers.AnsariRockel2024.nelsen7_tau verified The actual conditional CDF product gives tau=-1+theta*(rho+3)/3 without a density assumption. Substituting the proved rho formula yields the printed logarithmic expression for 0<theta<1 and exact endpoint values -1 and 0. All three Nelsen 7 Table 6 coefficients are now checked.
Table 6: Nelsen 7 Chatterjee xi Papers.AnsariRockel2024.nelsen7_xi verified Xi=1-theta for the entire closed parameter interval, including W at zero and independence at one.
arXiv v3 Appendix A.5.1: printed Nelsen 7 xi intermediate integrand Papers.AnsariRockel2024.nelsen7_printed_xi_candidate_expanded; Papers.AnsariRockel2024.nelsen7_printed_xi_candidate_formula; Papers.AnsariRockel2024.nelsen7_printed_xi_candidate_zero; Papers.AnsariRockel2024.nelsen7_printed_xi_identity_false_half; Papers.AnsariRockel2024.nelsen7_printed_xi_identity_false verified The printed positive-part integrand is the CDF times (theta*v+1-theta)^2, not the squared step conditional CDF. Its xi expression equals -1-theta/4 for every theta, whereas actual xi is 1-theta; at the interior point theta=1/2 the values are -9/8 and 1/2. The arXiv v3 intermediate equality is false and is not claimed verified. The final Table 6 identity xi=1-theta is separately proved. This finding is specific to arXiv v3; journal-version correspondence for this line is not established.
Table 3 / Appendix A.1.1: Nelsen 7 exact CI region Papers.AnsariRockel2024.nelsen7_ci_iff verified CI iff theta=1. Complements the existing full-interval CD theorem; no interior or positivity restriction.
Table 3 / Appendix A.1.2: exact Nelsen 7 Schur order Papers.AnsariRockel2024.nelsen7_schur_iff verified Schur comparison in both directions holds iff the parameters are reversely ordered: C_theta precedes C_eta iff eta<=theta, including both endpoints. Uses continuous convex tests of conditional CDFs.
Lemmas 2.6(i) and 2.8(i): comparison with monotone copulas Papers.AnsariRockel2024.schur_below_cis; Papers.AnsariRockel2024.schur_below_cds verified For arbitrary C and CIS D, C<=Schur D implies C<=LO D. For CDS D it implies D<=LO C. No monotonicity or density hypothesis is added for C. Convex hinge tests and an antitone version of the comparator kernel prove the bound.
Lemmas 2.6(ii) and 2.8(ii): exact monotone-class order equivalences Papers.AnsariRockel2024.cis_schur_iff_orthant; Papers.AnsariRockel2024.cds_schur_iff_reverse_orthant verified For any two CIS copulas, Schur order is equivalent to lower orthant order; for two CDS copulas it is equivalent to reversed lower orthant order. A finite convex-majorization theorem and L1 convergence of row averages prove all continuous convex tests. No density or smoothness hypothesis.
Proposition 3.2: all three survival invariances Papers.AnsariRockel2024.survival_lowerOrthant_iff; Papers.AnsariRockel2024.survival_cis_iff; Papers.AnsariRockel2024.survival_schur_iff verified Lower orthant order, directional CIS and directional Schur order are preserved and reflected by taking survival copulas. All bivariate copulas, including singular laws.
Lemma 2.9: concordance consistency in copula form Papers.AnsariRockel2024.concordance_coefficients_mono verified Lower orthant comparison implies both rho and tau comparison, for all bivariate copulas.
Lemma 2.10: copula specialization Papers.AnsariRockel2024.schur_xi_mono verified Directional conditional-CDF Schur order implies xi comparison. This is the continuous-margin copula specialization; the general arbitrary-margin random-variable statement is not claimed by this row.
Lemma 2.12: both tail coefficients Papers.AnsariRockel2024.lower_tail_mono; Papers.AnsariRockel2024.upper_tail_mono verified Lower orthant comparison implies comparison of both tail limits when the limits exist. No assumption that every copula has such limits.
Equation (3): Pickands representation from max-stability Papers.AnsariRockel2024.extremeValue_pickands_representation verified An actual max-stable bivariate copula determines its canonical Pickands function by a logarithmic ray; the representation is proved, not assumed. No density or differentiability hypothesis.
Section 2.1.2 / support for Theorem 3.4: canonical Pickands bounds and logarithmic structure Papers.AnsariRockel2024.extremeValue_pickands_bounds; Papers.AnsariRockel2024.extremeValue_log_homogeneous; Papers.AnsariRockel2024.extremeValue_log_submodular; Papers.AnsariRockel2024.extremeValue_log_increment_first; Papers.AnsariRockel2024.extremeValue_log_increment_second verified Max-stability alone gives max(1-t,t)<=A(t)<=1 for the canonical extracted function. The negative log-CDF in nonnegative logarithmic coordinates is homogeneous, has nonpositive rectangle increments, and each coordinate increment lies between zero and the coordinate displacement. The logarithmic rectangle inequality follows by differentiating the powered CDF rectangle sum at exponent zero from the right. No density or smoothness of the copula is assumed. Convexity of the canonical Pickands function and general CI are now proved in their dedicated rows below.
Support for Theorem 3.4: convex logarithmic sections without regularity assumptions Papers.AnsariRockel2024.extremeValue_log_section_convex verified For every max-stable bivariate copula and every fixed nonnegative second logarithmic coordinate, the negative log-CDF is convex in its positive first logarithmic coordinate. Submodularity and homogeneity give weighted comparisons at geometrically spaced points. A general continuity argument upgrades them to ordinary convexity: a hypothetical chord violation, perturbed by a small convex quadratic, would attain a positive interior maximum contradicting the strict geometric comparison. No copula density or derivative is assumed. The supporting-line transfer to concavity of the original CDF sections and general CI is now completed in the dedicated row below.
Theorem 3.4(i)-(ii): Pickands and orthant order Papers.AnsariRockel2024.extremeValue_pickands_order verified Lower orthant comparison is equivalent to reverse pointwise comparison of the associated Pickands functions on (0,1). Parts (iii)-(v) for arbitrary extreme-value copulas are now verified below without separate CI assumptions.
Theorem 3.4(iv)-(v): each directional Schur/Pickands equivalence under CI Papers.AnsariRockel2024.extremeValue_schur_first_iff_pickands_of_ci; Papers.AnsariRockel2024.extremeValue_schur_second_iff_pickands_of_ci verified Each conditional-CDF Schur direction individually is equivalent to reverse Pickands order for two extreme-value copulas independently known CI. These earlier conditional versions remain available; the general CI theorem now removes the additional premises below.
Remark 3.5: ordered rank coefficients Papers.AnsariRockel2024.extremeValue_pickands_concordance_mono; Papers.AnsariRockel2024.extremeValue_pickands_xi_mono_of_ci verified Reverse Pickands order raises rho and tau unconditionally; it raises xi in both conditioning directions when both copulas are CI. The lower-tail limit is the power-diagonal endpoint indicator; upper-tail limit is 2 minus the extremal coefficient. The unconditional xi comparison is now verified separately below.
Remark 3.5: ordered tail coefficients Papers.AnsariRockel2024.extremeValue_pickands_tail_mono verified Reverse Pickands order raises both extreme-value tail coefficients, including the comonotonic endpoint. Every bivariate extreme-value copula has both limits by the proved power-diagonal theorem.
Theorem 3.4(iii): Schur/Pickands bridge under CI Papers.AnsariRockel2024.extremeValue_schur_iff_pickands_of_ci verified For two extreme-value copulas that are independently known CI, reverse Pickands order is equivalent to both directional copula Schur comparisons. The general theorem is now verified separately below using the proved universal CI result.
Table 1: Marshall-Olkin CDF Papers.AnsariRockel2024.marshallOlkin_cdf verified The minimum of the two power products on the entire closed square, including zero coordinates and parameter endpoints.
Table 5 / Appendix A.2: Marshall-Olkin CI and orders Papers.AnsariRockel2024.marshallOlkin_ci; Papers.AnsariRockel2024.marshallOlkin_orthant_mono; Papers.AnsariRockel2024.marshallOlkin_schur_mono verified Both conditional directions are increasing, and coordinatewise parameter increase raises lower orthant order and both Schur orders. Singular laws and all weights in [0,1] included.
Table 5 / Appendix A.2: Cuadras-Auge CI and orders Papers.AnsariRockel2024.cuadrasAuge_ci; Papers.AnsariRockel2024.cuadrasAuge_orthant_mono; Papers.AnsariRockel2024.cuadrasAuge_schur_mono verified The entire parameter interval [0,1] is CI and increasing in lower orthant and both-direction Schur order.
Appendix A.5: Cuadras-Auge conditional CDF Papers.AnsariRockel2024.cuadrasAuge_conditionalCDF verified The explicit piecewise version is identified with the actual copula's conditional law almost everywhere, using CDF derivatives away from the diagonal. All delta in [0,1].
Table 6 / Appendix A.5: Cuadras-Auge rho and xi Papers.AnsariRockel2024.cuadrasAuge_rho; Papers.AnsariRockel2024.cuadrasAuge_xi verified Exact rho=3*delta/(4-delta) and xi=delta^2/(2-delta), with independent integration of the CDF and squared conditional CDF. Both endpoints included.
Table 6: Cuadras-Auge Kendall tau Papers.AnsariRockel2024.cuadrasAuge_tau verified Exact tau=delta/(2-delta) for every delta in [0,1]. The proof derives the conditional-CDF product identity by disintegration and Fubini for arbitrary copulas, then evaluates the symmetric triangle integral; it does not assume a density. Together with the preceding row, all three Table 6 coefficients for this family are checked.
Table 5: Marshall-Olkin density TP2 and absolute continuity Papers.AnsariRockel2024.marshallOlkin_density_tp2; Papers.AnsariRockel2024.marshallOlkin_absolutelyContinuous verified Both properties hold exactly when alpha=0 or beta=0. When both weights are positive, the common-shock construction charges a Lebesgue-null power curve. This proves the analytic min(alpha,beta)>0 non-TP2 entry, not the incompatible numerical-only max(alpha,beta)>0 claim.
Table 6: Marshall-Olkin Spearman rho Papers.AnsariRockel2024.marshallOlkin_rho verified Exact rho=3 alpha beta/(2 alpha+2 beta-alpha beta) for every alpha,beta in [0,1], including both independence axes and singular positive-weight laws. Derived by splitting the CDF integral at its parameter-dependent power curve.
Appendix A.5.2: Marshall-Olkin conditional CDF Papers.AnsariRockel2024.marshallOlkin_conditionalCDF verified For alpha>0, the explicit piecewise version agrees almost everywhere with the actual conditional law; the moving power-curve value is irrelevant.
Table 6 / Appendix A.5.2: Marshall-Olkin Chatterjee xi Papers.AnsariRockel2024.marshallOlkin_xi verified Exact xi=2 alpha^2 beta/(3 alpha+beta-2 alpha beta) for all alpha,beta in [0,1], including both independence axes, the alpha=1/2 case, and singular positive-weight laws. Derived by integrating the squared actual conditional CDF.
Table 6: Marshall-Olkin Kendall tau Papers.AnsariRockel2024.marshallOlkin_tau verified Exact tau=alpha beta/(alpha+beta-alpha beta) for all alpha,beta in [0,1], including both independence axes, beta=1, and singular positive-weight laws. Derived from the conditional-CDF product identity and a power-curve split; no density assumption. All three Table 6 coefficients for this family are now checked.
Table 4: Marshall-Olkin independence axes Papers.AnsariRockel2024.marshallOlkin_independence_axes verified Either zero weight gives the independence copula, even if the other weight is positive.
Table 5: Cuadras-Auge density TP2 and absolute continuity Papers.AnsariRockel2024.cuadrasAuge_density_tp2; Papers.AnsariRockel2024.cuadrasAuge_absolutelyContinuous verified Both hold exactly at delta=0. Every positive parameter charges the diagonal, including the delta=1 endpoint.
Tables 1–2: Gumbel–Barnett constructor, CDF and independence endpoint Papers.AnsariRockel2024.gumbelBarnett_cdf; Papers.AnsariRockel2024.gumbelBarnett_zero; Papers.AnsariRockel2024.gumbelBarnett_parameter_continuous verified An actual measure copula is constructed from an admissible bivariate generator for 0<θ≤1 and independence at zero. The printed exponential CDF holds on the entire closed square and depends continuously on θ∈[0,1], including zero.
Table 3: Gumbel–Barnett CI/CD and density TP2 Papers.AnsariRockel2024.gumbelBarnett_cd; Papers.AnsariRockel2024.gumbelBarnett_ci_iff; Papers.AnsariRockel2024.gumbelBarnett_density_tp2_iff verified CD for every θ∈[0,1]; CI and existence of a TP2 Lebesgue density each hold exactly at θ=0. The density exclusion is about every possible density version, using the proved implication from MTP2 density to PQD.
Table 3: Gumbel–Barnett parameter orders and tails Papers.AnsariRockel2024.gumbelBarnett_lowerOrthant_iff; Papers.AnsariRockel2024.gumbelBarnett_schur_iff; Papers.AnsariRockel2024.gumbelBarnett_tails verified Exact lower-orthant order reverses the parameter order; both-direction Schur order follows the parameter order. Both tail coefficients are zero, including both endpoints.
Table 6: Gumbel–Barnett exact xi Papers.AnsariRockel2024.gumbelBarnett_conditionalCDF; Papers.AnsariRockel2024.gumbelBarnett_xi; Papers.AnsariRockel2024.gumbelBarnett_xi_zero verified The actual conditional CDF is identified almost everywhere, then integrated to prove xi = 3 exp(3/(2θ)) E1(3/(2θ))/(4θ) + θ/3 − 1/2 for 0<θ≤1, with E1(a)=∫₁∞ exp(−as)/s ds. At θ=0, xi=0. Both changes of variables and the improper-integral evaluation are checked in Lean.
Tables 1–2: Nelsen 10 actual constructor and CDF Papers.AnsariRockel2024.nelsen10_cdf; Papers.AnsariRockel2024.nelsen10_zero; Papers.AnsariRockel2024.nelsen10_one verified The inner-power transformation of the admissible AMH(−1) generator constructs the actual copula for 0<θ≤1. Its printed CDF uv/(1+(1−u^θ)(1−v^θ))^(1/θ) holds on the closed square. The zero member is independence and the θ=1 member is AMH(−1). Continuity at zero is covered by the separate endpoint row below.
Table 3: Nelsen 10 quadrant dependence, CI, density TP2 and tails Papers.AnsariRockel2024.nelsen10_nqd; Papers.AnsariRockel2024.nelsen10_pqd_iff; Papers.AnsariRockel2024.nelsen10_ci_iff; Papers.AnsariRockel2024.nelsen10_density_tp2_iff; Papers.AnsariRockel2024.nelsen10_tails verified NQD for all θ∈[0,1]; PQD, CI and existence of a TP2 Lebesgue density each hold exactly at θ=0. Both tail coefficients are zero throughout the closed interval. CD and the unordered-parameter entries are covered below.
Table 3: Nelsen 10 CD Papers.AnsariRockel2024.nelsen10_cd verified CD holds on the entire closed parameter interval [0,1]. Each actual CDF section has an increasing first derivative on the interior and is continuous at both boundaries; Archimedean exchangeability gives the second direction.
Table 1: Nelsen 10 independence limit Papers.AnsariRockel2024.nelsen10_continuousAt_zero verified The actual CDF is continuous in θ at zero at every point of the closed square. The logarithmic denominator has derivative zero at zero, yielding convergence to independence despite the printed 1/θ exponent.
Table 3: Nelsen 10 unordered parameter family Papers.AnsariRockel2024.nelsen10_cdf_crossing; Papers.AnsariRockel2024.nelsen10_orthant_incomparable; Papers.AnsariRockel2024.nelsen10_schur_incomparable; Papers.AnsariRockel2024.nelsen10_schurBoth_incomparable verified The θ=1/2 and θ=1 members are incomparable in lower-orthant order: the CDFs cross at the diagonal points 1/16 and 9/16, with all values compared by exact rational arithmetic. The proved CD equivalence then excludes both directions of directional and both-direction Schur order. This establishes that the parameter family is not totally ordered; it does not assert that every distinct pair is incomparable.
Tables 1–2: Nelsen 11 constructor and CDF Papers.AnsariRockel2024.nelsen11_cdf; Papers.AnsariRockel2024.nelsen11_zero verified A convex truncated generator constructs an actual measure copula for every 0<θ≤1/2. Its printed positive-part power CDF holds on the full closed square, including both grounded axes and the interior zero region. The member at zero is independence, and the limiting correspondence is proved in the separate row below.
Table 3: Nelsen 11 quadrant dependence, CI, density TP2 and tails Papers.AnsariRockel2024.nelsen11_nqd; Papers.AnsariRockel2024.nelsen11_pqd_iff; Papers.AnsariRockel2024.nelsen11_ci_iff; Papers.AnsariRockel2024.nelsen11_density_tp2_iff; Papers.AnsariRockel2024.nelsen11_tails verified NQD throughout [0,1/2]. PQD, CI and existence of a TP2 Lebesgue density each hold exactly at θ=0, with an explicit interior zero-CDF witness for every positive parameter. Both tail coefficients are zero. CD and both parameter orders are covered below.
Table 1: Nelsen 11 independence limit Papers.AnsariRockel2024.nelsen11_tendsto_zero verified Along every admissible parameter path tending to zero, the actual CDF converges to independence at every point of the closed square. The logarithmic base has derivative log(u)+log(v) at zero, and continuity proves that its positive-part cutoff is inactive near zero at interior points. Both grounded axes are handled separately.
Table 3: Nelsen 11 CD Papers.AnsariRockel2024.nelsen11_cd verified CD holds throughout the closed parameter interval [0,1/2]. The proof establishes convexity of the positive CDF branch and its extension by zero across the cutoff, then uses Archimedean exchangeability for the other direction. It includes the independence member and does not assume differentiability at the cutoff.
Table 3: Nelsen 11 parameter orders Papers.AnsariRockel2024.nelsen11_lowerOrthant_antitone; Papers.AnsariRockel2024.nelsen11_schur_monotone verified For every 0≤θ≤η≤1/2, Cη≤LO Cθ and Cθ≤SchurBoth Cη. Concavity of the transformed generator gives the exact power comparison, including the truncated zero region; the established CD equivalence supplies both Schur directions. The zero-parameter independence case is included.
Tables 1–2: Nelsen 13 constructor and special cases Papers.AnsariRockel2024.nelsen13_cdf; Papers.AnsariRockel2024.nelsen13_zero; Papers.AnsariRockel2024.nelsen13_one verified A positive convex Archimedean generator constructs an actual copula for every θ>0, with the printed exponential-power CDF on the full closed square. The θ=0 member is Gumbel–Barnett(1), and θ=1 is independence. Both limiting correspondences are proved in the endpoint row below.
Table 3: Nelsen 13 tail coefficients Papers.AnsariRockel2024.nelsen13_tails verified Both tail coefficients are zero for every finite θ≥0. The diagonal has derivative 2 at one; an exponential bound proves the lower diagonal ratio tends to zero at zero. The θ=0 member uses the verified Gumbel–Barnett tails. CI, both parameter orders, and the exact density-TP2 classification are covered below.
Table 3: Nelsen 13 lower-orthant parameter order Papers.AnsariRockel2024.nelsen13_lowerOrthant_monotone verified The actual family increases in lower-orthant order for every 0≤θ≤η, including the Gumbel–Barnett endpoint at zero. A convex-power comparison proves the positive-parameter order; a separate product bound includes zero.
Tables 1–2: Nelsen 13 endpoint limits Papers.AnsariRockel2024.nelsen13_tendsto_zero; Papers.AnsariRockel2024.nelsen13_tendsto_atTop verified Along every admissible parameter path, the actual CDF converges to Gumbel–Barnett(1) at zero and to min(u,v) at infinity, on the full closed square. The first limit uses the derivative of the logarithmic power base; the second squeezes its root between max(a,b) and 2^(1/θ) max(a,b).
Table 3: Nelsen 13 CI and Schur order Papers.AnsariRockel2024.nelsen13_ci_iff; Papers.AnsariRockel2024.nelsen13_schur_monotone verified CI holds exactly for θ≥1. An analytic second-derivative bound gives concavity of actual CDF sections, including their continuous boundary values. Below one, the diagonal point u=v=exp(−1) violates PQD. The established orthant order and CI equivalence give increasing both-direction Schur order throughout θ≥1.
Table 3: Nelsen 13 density TP2 necessity Papers.AnsariRockel2024.nelsen13_density_tp2_requires_one verified Existence of a TP2 Lebesgue density requires θ≥1, since it implies PQD. Sufficiency and the full printed equivalence are now covered in the next row.
Table 3: Nelsen 13 exact density TP2 Papers.AnsariRockel2024.nelsen13_density_measure; Papers.AnsariRockel2024.nelsen13_density_tp2_iff verified A TP2 Lebesgue density exists exactly for θ≥1. The nonnegative measurable mixed-derivative formula is TP2 by log-convexity of the second derivative of the inverse generator. Two integrations establish its mass on every positive rectangle; absolute continuity and increasing rectangle exhaustion identify the full measure, including the axes.
Table 3: Nelsen 12 and 14 CI Papers.AnsariRockel2024.nelsen12_ci; Papers.AnsariRockel2024.nelsen14_ci verified Both actual copula families are CI for every finite θ≥1. A shared BB1 proof uses log-convexity of the negative derivative of the inverse generator, the inverse-function derivative identity, and continuous boundary CDF sections. Actual density TP2 on the full range is covered below.
Table 3: Nelsen 12 Schur parameter order Papers.AnsariRockel2024.nelsen12_schur_monotone verified Increasing both-direction Schur order holds for every 1≤θ≤η, by the proved CI classification and lower-orthant parameter order.
Table 3: Gumbel–Hougaard CI and Schur order Papers.AnsariRockel2024.gumbel_ci; Papers.AnsariRockel2024.gumbel_schur_monotone verified CI and increasing both-direction Schur parameter order hold for every finite θ≥1. Log-convexity of the negative generator derivative proves CI; the lower-orthant order then gives both Schur directions. Actual density TP2 is covered below.
Table 3: Joe CI Papers.AnsariRockel2024.joe_ci verified Joe is CI for every finite θ≥1, including independence at one. The proof establishes concavity of log(1−exp(−t)) on t>0 and hence log-convexity of the negative generator derivative, then applies the checked Archimedean criterion. Actual density TP2 and parameter orders are covered below.
Table 3: Joe parameter orders Papers.AnsariRockel2024.joe_lowerOrthant_monotone; Papers.AnsariRockel2024.joe_schur_monotone verified For every finite 1≤θ≤η, Joe increases in lower-orthant order and in both-direction Schur order. Convexity of the transformed generator yields the power comparison on the full closed square; the verified CI equivalence gives both Schur directions.
Table 3: Joe actual density TP2 Papers.AnsariRockel2024.joe_toMeasure_density; Papers.AnsariRockel2024.joe_density_tp2 verified For every finite theta>=1, the measurable mixed-derivative density is TP2 and equals the actual copula density. Positivity and log-convexity of the second generator derivative give TP2. Two integrations on strictly interior rectangles and exhaustion of the boundary identify the measure, including parameters with a corner singularity.
Table 3: Gumbel-Hougaard actual density TP2 Papers.AnsariRockel2024.gumbel_toMeasure_density; Papers.AnsariRockel2024.gumbel_density_tp2 verified For every finite theta>=1, the measurable mixed-derivative density is TP2 and identifies the actual copula measure. The proof establishes positivity and log-convexity of the second generator derivative, integrates on interior rectangles, and exhausts the boundary. Independence at theta=1 is included.
Table 3: Nelsen 12 and 14 actual density TP2 Papers.AnsariRockel2024.nelsen12_density_tp2; Papers.AnsariRockel2024.nelsen14_density_tp2; Papers.AnsariRockel2024.nelsen12_toMeasure_density; Papers.AnsariRockel2024.nelsen14_toMeasure_density verified Both families have TP2 densities for every finite theta>=1. A shared full two-parameter BB1 proof establishes positivity and log-convexity of the second generator derivative, TP2 of the measurable density, and equality with the actual measure by interior-rectangle integration and boundary exhaustion. The common Clayton endpoint is included.
Table 3: Nelsen 14 parameter orders Papers.AnsariRockel2024.nelsen14_lowerOrthant_monotone; Papers.AnsariRockel2024.nelsen14_schur_monotone verified For every finite 1<=theta<=eta, the actual family increases in lower-orthant order on the closed square and in both-direction Schur order. Monotonicity of a normalized power increment gives the generator-comparison inequality; the established CI theorem then supplies both Schur directions.
Tables 1-2: Nelsen 16 constructor, CDF and zero endpoint Papers.AnsariRockel2024.nelsen16_cdf_full; Papers.AnsariRockel2024.nelsen16_zero; Papers.AnsariRockel2024.nelsen16_cdf_continuous_parameter; Papers.AnsariRockel2024.nelsen16_tendsto_zero verified An actual copula measure is constructed for every finite theta>=0. The printed square-root CDF holds on the full closed square with grounded axes, including the countermonotonic member at zero. CDFs depend continuously on the parameter and converge pointwise to W along every admissible parameter path tending to zero. Lower-orthant order and the infinite-parameter endpoint are covered below; CI sufficiency, Schur order on the CI range, and both tails are covered below; The exact CI and density-TP2 classifications are covered below.
Table 3: Nelsen 16 lower-orthant parameter order Papers.AnsariRockel2024.nelsen16_lowerOrthant_monotone verified Increasing lower-orthant order holds for every finite 0<=theta<=eta, including the countermonotonic endpoint. The quadratic equation for the CDF and its upper bound by the harmonic copula yield the comparison on the full closed square.
Table 2: Nelsen 16 infinite-parameter endpoint Papers.AnsariRockel2024.nelsen16_tendsto_atTop verified Along every nonnegative parameter path tending to infinity, the actual CDF converges pointwise on the full closed square to Clayton(1), the harmonic copula H. The proof bounds the scaled interior error by 2/theta; grounded axes are handled exactly.
Table 3: Nelsen 16 tail pair Papers.AnsariRockel2024.nelsen16_tails verified Lower-tail dependence is 1/2 for every finite theta>0 and zero at the theta=0 countermonotonic endpoint; upper-tail dependence is zero throughout theta>=0. A rationalized diagonal formula agrees with the actual CDF and has checked derivatives 1/2 at zero and 2 at one for positive parameters.
Table 3: Nelsen 16 CI sufficiency and Schur order Papers.AnsariRockel2024.nelsen16_ci; Papers.AnsariRockel2024.nelsen16_schur_monotone verified The actual family is CI for every finite theta>=3 and increases in both-direction Schur order for 3<=theta<=eta. The proof checks log-convexity of the negative inverse-generator derivative and applies the established Archimedean criterion; the lower-orthant order gives both Schur directions. CI necessity and density TP2 sufficiency are covered below.
Table 3: Nelsen 16 actual density and TP2 sufficiency Papers.AnsariRockel2024.nelsen16_toMeasure_density; Papers.AnsariRockel2024.nelsen16_density_tp2 verified The measurable mixed-derivative formula identifies the actual copula density for every finite theta>0. It is TP2 for theta>=3+2*sqrt(2), by log-convexity of the second generator derivative and the established interior-rectangle integration theorem. Necessity of the printed TP2 threshold is covered below.
Table 3: Nelsen 16 exact CI classification Papers.AnsariRockel2024.nelsen16_ci_iff verified For every finite theta>=0, the actual copula is CI exactly when theta>=3. The necessity proof derives an upper-edge curvature inequality from concavity of actual CDF sections; a one-sided derivative at the corner forces (theta+1)(theta-3)>=0. The countermonotonic zero endpoint is excluded separately.
Table 3: Nelsen 16 exact density-TP2 classification Papers.AnsariRockel2024.nelsen16_density_tp2_iff verified For every finite theta>=0, a TP2 density exists exactly when theta>=3+2sqrt(2). Almost-everywhere uniqueness and continuity transfer ordered minors from any density version to the explicit formula. A corner midpoint inequality forces (theta-1)^2>=4theta; the necessary CI range theta>=3 selects the upper branch.
Tables 1-2: Nelsen 19 constructor, CDF and zero limit Papers.AnsariRockel2024.nelsen19_cdf; Papers.AnsariRockel2024.nelsen19_zero; Papers.AnsariRockel2024.nelsen19_tendsto_zero verified An actual copula measure is constructed for every finite theta>=0. The printed logarithmic CDF holds for positive parameters on the full closed square with grounded axes. The zero member is Clayton(1), the harmonic copula H; every nonnegative parameter path tending to zero converges pointwise to H, including paths that attain zero. The infinite endpoint and parameter orders are covered below.
Table 3: Nelsen 19 conditional increase Papers.AnsariRockel2024.nelsen19_ci verified CI holds throughout theta>=0. For positive parameters the negative inverse-generator derivative is log-convex; the zero member inherits CI from Clayton(1). Density TP2 is covered below.
Table 3: Nelsen 19 tail pair Papers.AnsariRockel2024.nelsen19_tails verified Lower-tail dependence is 1 for theta>0 and 1/2 at theta=0. Upper-tail dependence is zero throughout theta>=0. The lower-tail proof sandwiches the actual diagonal ratio between theta/(theta+t*log(2)) and one; the upper-tail proof differentiates the actual diagonal at one.
Table 3: Nelsen 19 parameter orders Papers.AnsariRockel2024.nelsen19_lowerOrthant_monotone; Papers.AnsariRockel2024.nelsen19_schur_monotone verified Increasing lower-orthant and both-direction Schur order hold throughout 0<=theta<=eta. Convex power increments compare the positive-parameter CDFs; the checked zero limit extends the comparison to the harmonic endpoint. CI yields both Schur directions.
Table 2: Nelsen 19 infinite-parameter endpoint Papers.AnsariRockel2024.nelsen19_tendsto_atTop verified Along every nonnegative parameter path tending to infinity, the actual CDF tends pointwise on the full closed square to M. The proof bounds the CDF below by min(u,v)/(1+min(u,v)*log(2)/theta) for positive parameters and above by min(u,v).
Table 3: Nelsen 19 actual density TP2 Papers.AnsariRockel2024.nelsen19_toMeasure_density; Papers.AnsariRockel2024.nelsen19_density_tp2 verified The explicit mixed-derivative density is measurable, nonnegative and identified with the actual copula measure for every theta>0. Its TP2 inequality follows from checked log-convexity of the second inverse-generator derivative. The harmonic theta=0 member inherits an actual TP2 density from Clayton(1), completing the nonnegative parameter range.
Tables 1-2: Nelsen 20 constructor, CDF and zero member Papers.AnsariRockel2024.nelsen20_cdf; Papers.AnsariRockel2024.nelsen20_zero verified An actual copula measure is constructed for every finite theta>=0. The printed logarithmic-power CDF holds for positive parameters on the full closed square with grounded axes; the zero member is independence. Parameter convergence at zero and infinity, parameter orders and density TP2 are covered below.
Table 3: Nelsen 20 conditional increase Papers.AnsariRockel2024.nelsen20_ci verified CI holds for every finite theta>=0. For positive parameters the negative inverse-generator derivative is log-convex; the zero member is independence.
Table 3: Nelsen 20 tail pair Papers.AnsariRockel2024.nelsen20_tails verified Lower-tail dependence is 1 for every theta>0 and 0 at the independence member theta=0. Upper-tail dependence is zero throughout theta>=0. A logarithmic bound sandwiches the actual lower-tail ratio; differentiation of the actual diagonal at one gives the upper-tail coefficient.
Table 2: Nelsen 20 parameter limits Papers.AnsariRockel2024.nelsen20_tendsto_zero; Papers.AnsariRockel2024.nelsen20_tendsto_atTop verified Every nonnegative parameter path tending to zero gives pointwise convergence on the full closed square to independence, including paths attaining zero. Every nonnegative path tending to infinity gives convergence to M. The zero proof uses the derivative of the double logarithm; the infinite proof bounds the CDF below by min(u,v)*(1+log(2))^(-1/theta).
Table 3: Nelsen 20 parameter orders Papers.AnsariRockel2024.nelsen20_lowerOrthant_monotone; Papers.AnsariRockel2024.nelsen20_schur_monotone verified Increasing lower-orthant and both-direction Schur orders hold for every 0<=theta<=eta. A convex change between the generators gives the positive-parameter comparison. The checked zero limit extends it to independence, and CI gives both Schur directions.
Table 3: Nelsen 20 actual density TP2 Papers.AnsariRockel2024.nelsen20_toMeasure_density; Papers.AnsariRockel2024.nelsen20_density_tp2 verified The measurable nonnegative mixed-derivative density is identified with the actual copula measure for every positive parameter. Log-convexity of the second inverse-generator derivative proves TP2; the independence member at zero has its usual TP2 density. This covers the entire finite nonnegative parameter range.
Tables 1-2: Nelsen 17 constructor, full CDF and independence member Papers.AnsariRockel2024.nelsen17_cdf_full; Papers.AnsariRockel2024.nelsen17_neg_one verified An actual copula measure is constructed for every nonzero real theta, on both sign branches. The printed power CDF holds on the full closed square without an interior restriction, and theta=-1 is independence. Positivity, monotonicity, convexity and the inverse identity are checked for the generator. Exact conditional, quadrant-dependence and density-TP2 classifications and both tails are covered below; parameter orders and the limits at zero and both infinities are covered below.
Table 3: Nelsen 17 conditional monotonicity, sufficiency Papers.AnsariRockel2024.nelsen17_isCI; Papers.AnsariRockel2024.nelsen17_isCD verified For every nonzero parameter, CI holds when theta>=-1 and CD holds when theta<=-1. These are statements about the actual copula: log-convexity or log-concavity of the negative inverse-generator derivative yields concavity or convexity of its CDF sections. Necessity of these ranges is covered below.
Table 3: Nelsen 17 tail coefficients Papers.AnsariRockel2024.nelsen17_tails verified Both tail coefficients are zero for every finite nonzero real theta. A smooth real diagonal agrees with the actual copula on the entire closed interval; its endpoint derivatives are zero at 0 and two at 1. This covers both parameter branches.
Table 3: Nelsen 17 exact conditional and quadrant-dependence classifications Papers.AnsariRockel2024.nelsen17_isCI_iff; Papers.AnsariRockel2024.nelsen17_isCD_iff; Papers.AnsariRockel2024.nelsen17_isPQD_iff; Papers.AnsariRockel2024.nelsen17_isNQD_iff verified For every nonzero parameter, CI and PQD hold iff theta>=-1, while CD and NQD hold iff theta<=-1. Necessity follows from the actual CDF-section derivative at zero: its value at v=1/2 violates the quadrant bound outside the stated range, by strict convexity or concavity of the power function.
Table 3: Nelsen 17 actual density and exact TP2 classification Papers.AnsariRockel2024.nelsen17_toMeasure_density; Papers.AnsariRockel2024.nelsen17_density_tp2_iff verified The mixed-derivative formula is identified with the copula measure for every nonzero parameter by interior-rectangle integration and boundary exhaustion. A TP2 density exists iff theta>=-1. Sufficiency uses log-convexity of the positive second inverse-generator derivative; necessity follows from the exact CI classification and the general MTP2-density implication.
Table 3: Nelsen 17 lower-orthant and Schur parameter orders Papers.AnsariRockel2024.nelsen17_lowerOrthant_monotone; Papers.AnsariRockel2024.nelsen17_schur_monotone; Papers.AnsariRockel2024.nelsen17_schur_antitone verified Lower-orthant order increases for every ordered pair of nonzero real parameters, including pairs across zero. Both-direction Schur order increases on theta>=-1 and decreases on theta<=-1, with zero excluded. Convexity and superadditivity of the explicit generator comparison are proved using Bernoulli inequalities in all exponent sign cases.
Nelsen 17 full-square limits at zero and positive infinity Papers.AnsariRockel2024.nelsen17_tendsto_atTop; Papers.AnsariRockel2024.nelsen17_tendsto_zero verified At positive infinity the CDF converges to M, using a uniform lower bound with factor 4^(-1/theta). Along every nonzero parameter path tending to zero from either sign, the CDF converges to exp(log(1+u)*log(1+v)/log(2))-1. Both results hold on the full closed square, including the axes. The negative-infinity limit is covered below.
Nelsen 17 full-square negative-infinity limit Papers.AnsariRockel2024.nelsen17_tendsto_atBot verified The CDF converges to max(1,(1+u)*(1+v)/2)-1 on the entire closed square. Power bounds converge from both sides at every interior point, including the cutoff curve; groundedness handles the axes.
Tables 1-2: Nelsen 21 constructor, full CDF and countermonotonic member Papers.AnsariRockel2024.nelsen21_cdf_full; Papers.AnsariRockel2024.nelsen21_one verified An actual copula measure is constructed for every theta>=1. The inverse generator is its own inverse on [0,1], convex and decreasing there, and extended by zero beyond the cutoff. The printed nested-power CDF holds on the full closed square, and theta=1 is W. Conditional classifications, density-TP2 exclusions, both tails, parameter limits and increasing lower-orthant order are covered below; Schur nonmonotonicity in both directions is covered below; no incomparable pair is asserted.
Table 3: Nelsen 21 tails and exact conditional/quadrant classifications Papers.AnsariRockel2024.nelsen21_lowerTail; Papers.AnsariRockel2024.nelsen21_upperTail; Papers.AnsariRockel2024.nelsen21_not_pqd; Papers.AnsariRockel2024.nelsen21_not_ci; Papers.AnsariRockel2024.nelsen21_not_density_tp2; Papers.AnsariRockel2024.nelsen21_isCD_iff; Papers.AnsariRockel2024.nelsen21_isNQD_iff verified For every theta>=1, the lower tail is zero and the upper tail is 2-2^(1/theta). A positive zero-diagonal point excludes PQD, CI and any TP2 density throughout the range. The strictly positive upper tail for theta>1 excludes NQD and CD there; both hold exactly at theta=1. The upper-tail proof uses a checked derivative and continuous difference quotient, including the theta=1 boundary.
Nelsen 21 full-square parameter continuity and endpoint limits Papers.AnsariRockel2024.nelsen21_tendsto_atTop; Papers.AnsariRockel2024.nelsen21_tendsto_parameter; Papers.AnsariRockel2024.nelsen21_tendsto_one verified CDFs depend continuously on every finite parameter theta>=1, converge to W at theta=1, and converge to M as theta tends to infinity. The infinite endpoint uses a uniform CDF lower bound with factor (2*theta)^(1/theta), while the copula upper bound supplies the squeeze. Every result includes the entire closed square.
Table 3: Nelsen 21 increasing lower-orthant parameter order Papers.AnsariRockel2024.nelsen21_lowerOrthant_monotone verified The actual copulas increase in lower-orthant order for every 1<=theta<=eta. Convexity of the explicit generator comparison follows from the monotonicity of its positive derivative, with the sign reduced to Bernoulli inequality. Superadditivity is used only before the cutoff; beyond it the smaller CDF is zero. Schur nonmonotonicity in both directions is covered below; no incomparable pair is asserted.
Table 3: Nelsen 21 failure of both Schur parameter monotonicities Papers.AnsariRockel2024.nelsen21_not_schur_monotone; Papers.AnsariRockel2024.nelsen21_not_schur_antitone verified Neither increasing nor decreasing Schur order holds throughout theta>=1. At theta=2, a continuous section derivative strictly between zero and one makes the median conditional energy strictly below 1/2. W at theta=1 excludes increasing order; the full-square limit to M and a median-strip energy inequality exclude decreasing order. These statements do not supply an incomparable pair; that stronger reading of the unordered cell is not asserted (see the excluded row).
Tables 1-2: Nelsen 18 constructor and printed CDF Papers.AnsariRockel2024.nelsen18_cdf_full; Papers.AnsariRockel2024.nelsen18_cdf_of_lt_one verified An actual copula measure is constructed for every theta>=2. The inverse generator 1+theta/log(t) is continuous at zero, decreasing and convex up to exp(-theta), and zero beyond that cutoff. The printed logarithmic CDF holds for u,v<1, including grounded axes; the full-square formula uses the continuous generator endpoint phi(1)=0. Parameter limits, lower-orthant order and the unordered Schur entry are covered below.
Table 3: Nelsen 18 tails and dependence classifications Papers.AnsariRockel2024.nelsen18_lowerTail; Papers.AnsariRockel2024.nelsen18_upperTail; Papers.AnsariRockel2024.nelsen18_not_pqd; Papers.AnsariRockel2024.nelsen18_not_ci; Papers.AnsariRockel2024.nelsen18_not_density_tp2; Papers.AnsariRockel2024.nelsen18_not_nqd; Papers.AnsariRockel2024.nelsen18_not_cd verified Both tails hold throughout theta>=2: lower=0 and upper=1. At q=log(2)/(theta+log(2)), the diagonal CDF is zero, excluding PQD, CI and every TP2 density, and yielding the zero lower tail. The upper-tail ratio reduces near zero to 2-theta/(theta-t*log(2)); its limit one excludes NQD and CD. Thus neither conditional class applies, including theta=2.
Table 3: Nelsen 18 increasing lower-orthant parameter order Papers.AnsariRockel2024.nelsen18_lowerOrthant_monotone verified For every 2<=theta<=eta, the actual copulas increase in lower-orthant order. The inverse generators satisfy phi_eta=phi_theta^(eta/theta), and the corresponding inverse-function identity holds across the finite cutoff. The power-sum inequality proves the CDF comparison on the entire closed square. The unordered Schur entry is covered by the Nelsen 18 Schur row.
Nelsen 18 full-square parameter continuity and infinite endpoint Papers.AnsariRockel2024.nelsen18_tendsto_parameter; Papers.AnsariRockel2024.nelsen18_tendsto_atTop verified CDFs are continuous in every finite admissible parameter, including theta=2, and converge to the comonotonic copula as theta tends to infinity. The diagonal formula is normalized by theta to evaluate the limit; monotonicity of the copula CDF and its marginal upper bounds extend the result to every point of the closed square.
Tables 1-2: Nelsen 22 constructor, CDF and independence member Papers.AnsariRockel2024.nelsen22_zero; Papers.AnsariRockel2024.nelsen22_cdf_full; Papers.AnsariRockel2024.nelsen22_cdf_printed verified An actual copula is constructed for every theta in [0,1]. For theta>0 the base inverse generator 1-sin(t), truncated at pi/2, is raised to power 1/theta; theta=0 is independence. The printed piecewise arcsine CDF agrees with the measure on the entire closed square, including the cutoff and grounded axes. Convergence to this endpoint is checked below.
Table 3: Nelsen 22 tails and exact CI/density-TP2 ranges Papers.AnsariRockel2024.nelsen22_not_pqd; Papers.AnsariRockel2024.nelsen22_isCI_iff; Papers.AnsariRockel2024.nelsen22_density_tp2_iff; Papers.AnsariRockel2024.nelsen22_lowerTail; Papers.AnsariRockel2024.nelsen22_upperTail verified Both tail coefficients are zero for all theta in [0,1]. For theta>0 a positive zero-diagonal point excludes PQD, CI and TP2 density; CI and TP2 density each hold exactly at theta=0. The upper-tail proof checks the diagonal derivative at one, including the local cutoff condition. Parameter limits, CD and parameter orders are covered below.
Nelsen 22 full-square parameter continuity and independence limit Papers.AnsariRockel2024.nelsen22_tendsto_zero; Papers.AnsariRockel2024.nelsen22_tendsto_parameter verified CDFs are continuous throughout the closed parameter interval [0,1], including convergence to independence at zero. The logarithm of the positive trigonometric base has derivative log(u)+log(v) at zero; its continuous difference quotient gives the limiting power. The cutoff is inactive near zero at positive coordinates, and grounded axes are handled exactly. Arbitrary admissible parameter paths may include zero values.
Table 3: Nelsen 22 conditional decrease throughout the range Papers.AnsariRockel2024.nelsen22_isCD; Papers.AnsariRockel2024.nelsen22_isNQD verified CD and NQD hold for every theta in [0,1]. A derivative-ratio criterion admits the finite cutoff: the powered generator is differentiable there with derivative zero, while log(-psi derivative) is concave before the cutoff. A finite-interval convex-increment inequality proves the ratio comparison before cutoff, and its zero numerator handles the remaining case. The actual CDF sections are convex, giving CD without a density hypothesis. Parameter-order entries are covered below.
Table 3: Nelsen 22 lower-orthant and Schur parameter orders Papers.AnsariRockel2024.nelsen22_lowerOrthant_antitone; Papers.AnsariRockel2024.nelsen22_schur_monotone verified For every 0<=theta<=eta<=1, C_eta<=LO C_theta and C_theta<=Schur C_eta in both conditional directions. The exact generator comparison arcsin(1-(1-sin(t))^(eta/theta)) is concave and subadditive before its cutoff. Monotonicity of its squared derivative reduces to Bernoulli inequality; a separate cutoff bound handles zero regions. NQD supplies the theta=0 comparison, and the proved CD equivalence yields both Schur directions.
Table 4 Tawn limit / Table 5 shape order Papers.AnsariRockel2024.tawn_tendsto_atTop; Papers.AnsariRockel2024.tawn_lowerOrthant_monotone; Papers.AnsariRockel2024.tawn_tendsto_parameter verified For every pair of weights in [0,1], Tawn CDFs increase with the finite shape parameter, are continuous at every shape>=1, and converge to the Marshall-Olkin copula with the same weights as shape tends to infinity. The max-product constructor transfers Gumbel convergence and order; all results include the entire closed CDF square and weight endpoints. CI and both directional Schur shape orders are now verified in the row below.
Table 5: correction to the blanket Tawn density-TP2 exclusion Papers.AnsariRockel2024.tawn_one_one_density_tp2; Papers.AnsariRockel2024.tawn_one_one_not_independence; Papers.AnsariRockel2024.tawn_printed_tp2_exclusion_false verified At both weights equal to one, Tawn is Gumbel and has an actual TP2 density for every finite shape>=1. The strictly positive upper tail proves non-independence when shape>1. The shape=2, unit-weight member formally refutes the assertion that every non-independent Tawn member lacks TP2 density. This audits arXiv v3 Table 5. Other weights are covered only by the explicit non-TP2 witness (θ=2, α=β=1/2) below; the full classification is numerical-only in the source (see the excluded row).
Table 4: Tawn, Gumbel, Marshall-Olkin and Cuadras-Auge Pickands functions Papers.AnsariRockel2024.tawn_pickands; Papers.AnsariRockel2024.gumbel_pickands; Papers.AnsariRockel2024.marshallOlkin_pickands; Papers.AnsariRockel2024.cuadrasAuge_pickands verified The canonical Pickands functions extracted from the actual max-stable copulas equal their weighted logistic, logistic, and piecewise-linear expressions. The proof identifies the exponent on a logarithmic ray; it does not assume the representation formula for the named family. All t in [0,1], finite shapes>=1 and weights in [0,1] are included.
Table 5: Tawn CI and Schur shape order Papers.AnsariRockel2024.tawn_ci; Papers.AnsariRockel2024.tawn_schur_monotone; Papers.AnsariRockel2024.maxProduct_independence_ci verified Tawn is CI and increases in both directional conditional-CDF Schur orders as shape increases, for all finite shapes>=1 and weights in [0,1]. A three-point Jensen argument proves concavity of the power-perspective transform of any grounded concave section. Consequently max-product with independence preserves CI for every starting CI copula; no density or differentiability assumptions are used. This closes the Tawn CI/Schur gap; the density-TP2 cell is treated in the witness row and the excluded row below.
Table 3: Frank lower-orthant and Schur parameter orders Papers.AnsariRockel2024.frank_lowerOrthant_monotone; Papers.AnsariRockel2024.frank_schur_nonnegative; Papers.AnsariRockel2024.frank_schur_nonpositive verified The unified signed Frank family increases in lower-orthant order across the entire real parameter range. Both directional Schur orders increase on [0,infinity) and decrease on (-infinity,0], with independence included. The nonzero CDF order transfers the checked Nelsen 17 order through the increasing coordinate map 2^u-1 and logarithmic output map; CI/CD quadrant bounds handle zero. The Table 6 Kendall tau formula is audited below; the Debye-function rho formula is also audited below.
Table 4: Plackett construction and CDF; actual density Papers.AnsariRockel2024.plackett_cdf; Papers.AnsariRockel2024.plackett_one; Papers.AnsariRockel2024.plackett_density verified A copula measure is constructed for every theta>0. For theta!=1 its full-square CDF equals the printed square-root formula; theta=1 is independence. Strict positivity of the discriminant and nonnegativity of the mixed derivative prove the rectangle inequality. The mixed derivative theta*(1+(theta-1)*(u+v-2uv))/D^(3/2) is identified with the actual Lebesgue density for theta!=1. The conditional and quadrant classifications are verified in the next row. The complete TP2 classification, orders, limits and tails are verified below; the corrected rank formula is verified below.
Table 5: Plackett exact conditional and quadrant classifications Papers.AnsariRockel2024.plackett_ci_iff; Papers.AnsariRockel2024.plackett_cd_iff; Papers.AnsariRockel2024.plackett_pqd_iff; Papers.AnsariRockel2024.plackett_nqd_iff verified For all theta>0, CI and PQD each hold iff theta>=1; CD and NQD each hold iff theta<=1. The section second derivative has sign opposite theta-1, giving both conditional directions by symmetry. The exact midpoint CDF sqrt(theta)/(2*(sqrt(theta)+1)) proves the converse exclusions. Independence is included in all four classes.
Tables 4-5: Plackett parameter limits and tail coefficients Papers.AnsariRockel2024.plackett_tails; Papers.AnsariRockel2024.plackett_cdf_rationalized; Papers.AnsariRockel2024.plackett_tendsto_parameter; Papers.AnsariRockel2024.plackett_tendsto_zero; Papers.AnsariRockel2024.plackett_tendsto_atTop verified Both tails are zero at every finite theta>0, including independence. The rationalized CDF has a strictly positive denominator and proves continuity at every positive parameter, including theta=1. On the entire closed square, theta tending to zero gives W and theta tending to infinity gives M. The tail coefficients are actual endpoint limits derived from diagonal derivatives, not substitutions into parameter-limit copulas.
Table 5: Plackett exact orthant order and corrected Schur ranges Papers.AnsariRockel2024.plackett_lowerOrthant_iff; Papers.AnsariRockel2024.plackett_schur_above_one; Papers.AnsariRockel2024.plackett_schur_below_one verified On the full positive parameter range, C_theta<=LO C_eta iff theta<=eta. Both directional Schur orders increase on [1,infinity) and decrease on (0,1], including independence. The defining odds equation and copula bounds give the full-square orthant implication; the midpoint CDF gives necessity. The decreasing Schur range corrects the empty theta<=0 range printed in arXiv v3 Table 5; the journal cell remains unchecked.
Table 5 / Appendix A.4.1: Plackett TP2 exclusion outside [1,2] Papers.AnsariRockel2024.plackett_density_tp2_necessary; Papers.AnsariRockel2024.plackett_not_density_tp2_above_two verified Any TP2 Lebesgue density version of the actual Plackett measure requires 1<=theta<=2. CI necessity excludes theta<1. Above two, continuity transfers ordered minors from any TP2 version to the identified density. A shrinking rectangle (0,t)x(1-t,1) yields a normalized polynomial with limit 8theta^8(theta-1)*(2-theta), contradicting positivity. Sufficiency on [1,2] is proved in the next row, completing the classification.
Table 5: complete Plackett density-TP2 classification Papers.AnsariRockel2024.plackett_density_tp2_iff verified The actual Plackett measure admits a TP2 Lebesgue density iff 1<=theta<=2. For sufficiency, the mixed log-density derivative is nonnegative by an exact tensor Bernstein certificate: 150 nonnegative integer coefficients with degrees (5,4,4) on p=theta-1,u,v in [0,1]. Lean checks both the polynomial identity and coefficient signs. Two derivative-monotonicity arguments yield all ordered density minors, including boundary points; the identified density gives the measure-level result. Necessity excludes all other positive parameters. This replaces the source numerical-only positive range with a proof, including theta=2.
Table 6: corrected Plackett Spearman rho Papers.AnsariRockel2024.plackett_spearmanRho; Papers.AnsariRockel2024.plackett_spearmanRho_one; Papers.AnsariRockel2024.plackett_printed_rho_false verified Integration of the actual CDF gives (theta+1)/(theta-1)-2thetalog(theta)/(theta-1)^2 for theta>0, theta!=1; independence has rho=0. The odds equation supplies a section antiderivative, and Fubini gives the full integral. A checked theta=2 counterexample refutes the doubled logarithmic term printed in arXiv v3 Table 6. The journal cell remains unchecked.
Tables 1, 4-5 / Appendix A.4.1: Raftery source consistency Papers.AnsariRockel2024.raftery_printed_cdf_not_copula; Papers.AnsariRockel2024.raftery_zero_density; Papers.AnsariRockel2024.raftery_one_upperTail verified The literal Table 1 CDF cannot define a copula: delta=1/2 and u=v=7/8 give 5985/8192<3/4, violating the lower Frechet bound. Conditional on the stated endpoint identities, delta=0 has a TP2 Lebesgue density and delta=1 has upper-tail coefficient one, not zero. These are checked source inconsistencies. The corrected constructor and interior dependence classifications are verified below; the journal comparison is recorded in SOURCE_COMPARISON.md.
Tables 1 and 4: corrected Raftery constructor and CDF Papers.AnsariRockel2024.raftery_cdf; Papers.AnsariRockel2024.raftery_zero; Papers.AnsariRockel2024.raftery_one verified An actual copula measure is constructed for every delta in [0,1]. For delta<1 its full-square CDF equals min(u,v)+(1-delta)/(1+delta)(uv)^(1/(1-delta))*(1-max(u,v)^(-(1+delta)/(1-delta))). The factor 1/(1+delta) corrects the refuted source formula. With a=1/(1-delta), the construction mixes the product power CDF with the integral of products of power CDFs supported on [0,t]. Exact kernel means prove uniform margins; monotone kernels prove every rectangle increment is nonnegative. Delta=0 is independence and delta=1 is comonotonicity. Tail coefficients, parameter limits and Spearman rho are verified below; conditional and density classifications, parameter orders, and Kendall tau are also verified below; the journal comparison is recorded in SOURCE_COMPARISON.md.
Table 5: Raftery tail coefficients with corrected endpoint Papers.AnsariRockel2024.raftery_tails_lt_one; Papers.AnsariRockel2024.raftery_tails_one verified For every 0<=delta<1 the actual lower-tail coefficient is 2delta/(1+delta) and the upper-tail coefficient is zero. At delta=1 both coefficients are one. The diagonal is t+(1-delta)/(1+delta)(t^(2/(1-delta))-t); its endpoint derivatives prove the limits. This includes independence and excludes the comonotonic endpoint from the source zero-upper-tail claim.
Table 4: full-square Raftery parameter continuity and endpoint limits Papers.AnsariRockel2024.raftery_comonotonic_bounds; Papers.AnsariRockel2024.raftery_tendsto_parameter; Papers.AnsariRockel2024.raftery_tendsto_zero; Papers.AnsariRockel2024.raftery_tendsto_one verified The actual copula CDF depends continuously on delta throughout [0,1], including all boundary coordinates. Delta tending to zero gives independence and delta tending to one gives comonotonicity. The uniform bound min(u,v)-(1-delta)<=C_delta(u,v)<=min(u,v) controls the singular parameter limit at one; the corrected power formula proves continuity below one.
Table 6: Raftery Spearman rho Papers.AnsariRockel2024.raftery_spearmanRho verified The actual corrected copula has rho=delta*(4-3delta)/(2-delta)^2 throughout [0,1], including independence and comonotonicity. For a=1/(1-delta), each conditional power CDF has coordinate mean 1-at/(a+1). Bounded joint measurability justifies Fubini; integrating the product mixture gives CDF integral a*(a+2)/(3*(a+1)^2). This independently verifies the printed rho formula for the corrected family.
Table 5 / Appendix A.4.1: corrected Raftery density and TP2 classification Papers.AnsariRockel2024.raftery_density; Papers.AnsariRockel2024.raftery_absolutelyContinuous_iff; Papers.AnsariRockel2024.raftery_density_tp2_iff; Papers.AnsariRockel2024.raftery_printed_tp2_exclusion_false verified The corrected Raftery copula is absolutely continuous and has a TP2 Lebesgue density exactly for delta<1. For a=1/(1-delta), the density is a/(2a-1)min(u,v)^(a-1)(amax(u,v)^(a-1)+(a-1)*max(u,v)^(-a)). First and mixed derivatives match across the diagonal; interior-rectangle integration identifies the actual measure. Factoring into nonnegative coordinate weights and the antitone maximum factor a+(a-1)t^(1-2a) proves every TP2 minor. Delta=1 is singular comonotonicity. A non-independent delta=1/2 member formally refutes the printed universal TP2 exclusion.
Table 5: Raftery conditional and quadrant classifications Papers.AnsariRockel2024.raftery_ci; Papers.AnsariRockel2024.raftery_pqd; Papers.AnsariRockel2024.raftery_nqd_iff; Papers.AnsariRockel2024.raftery_cd_iff verified CI and PQD hold for every delta in [0,1]. The actual TP2 density implies CI below one; comonotonicity supplies the endpoint. CD and NQD each hold exactly at delta=0. The exact positive Spearman rho for delta>0 excludes NQD, hence excludes CD.
Table 5: Raftery lower-orthant and Schur parameter orders Papers.AnsariRockel2024.raftery_lowerOrthant_monotone; Papers.AnsariRockel2024.raftery_schur_monotone verified The corrected copulas increase in lower-orthant order and both directional Schur orders for all 0<=delta<=eta<=1. With a=1/(1-delta) and u<=v, the CDF is u-v*(u/v)^aintegral_v^1(t^(2a-2))dt. Both nonnegative factors in the subtracted term decrease with a. Symmetry covers the other triangle; quadrant dependence and the Frechet bound handle independence and comonotonicity. The verified CI property transfers orthant order to both Schur directions.
Table 6: Raftery Kendall tau Papers.AnsariRockel2024.raftery_kendallTau verified The corrected copula has tau=2delta/(3-delta) on the entire closed parameter interval. The actual identified density permits integration of the CDF against the copula measure. Symmetry reduces the integral to one triangle; the inner integral is a linear combination of powers v, v^(2a), and v^(4a-1), where a=1/(1-delta). Exact power integration gives integral (4a-1)/(4*(2a+1)), hence tau=2(a-1)/(2*a+1). Both singular/independence endpoint values are checked separately.
Theorem 3.4: universal extreme-value CI and unconditional Schur equivalences Papers.AnsariRockel2024.extremeValue_ci; Papers.AnsariRockel2024.extremeValue_schur_iff_pickands; Papers.AnsariRockel2024.extremeValue_schur_first_iff_pickands; Papers.AnsariRockel2024.extremeValue_schur_second_iff_pickands verified Every actual max-stable bivariate copula is CI, including singular and nonsmooth examples. Convex logarithmic sections admit supporting slopes in [0,1]; exponentiation and the real-power Bernoulli inequality give affine upper supports of the original CDF sections. The chord inequalities prove SI, and max-stability is preserved by transpose, giving both directions. Thus lower-orthant order, both directional Schur orders, and their conjunction are each equivalent to reverse canonical Pickands order, with no independent CI premise.
Remark 3.5: unconditional extreme-value xi comparisons Papers.AnsariRockel2024.extremeValue_pickands_xi_mono verified Reverse canonical Pickands order raises Chatterjee xi in both conditioning directions for arbitrary max-stable bivariate copulas. The newly proved universal CI theorem removes the hypotheses from the previous conditional result.
Section 2.1.2: canonical Pickands convexity on the closed interval Papers.AnsariRockel2024.extremeValue_pickands_real_coe; Papers.AnsariRockel2024.extremeValue_pickands_convex verified The real-coordinate extension agrees with the canonical function extracted from the actual copula, and is convex on [0,1]. Homogeneity expresses A(t) as t*L((1-t)/t,1) for t>0. Supporting lines of the convex logarithmic section produce affine lower supports of A at every interior point; their slope bound also handles t=0. Weighted support inequalities prove convexity including both endpoints. Together with the verified bounds, endpoint values and exponential representation, this establishes the defining Pickands properties without assuming a density.
Table 6 / Appendix A.5.1: Ali-Mikhail-Haq Chatterjee xi below theta=1 Papers.AnsariRockel2024.amh_conditionalCDF; Papers.AnsariRockel2024.amh_chatterjeeXi; Papers.AnsariRockel2024.amh_chatterjeeXi_zero verified For -1<=theta<1 and theta nonzero, the actual copula has xi=-theta/6-2/3+3/theta-2/theta^2-2*(theta-1)^2*log(1-theta)/theta^3. The copula CDF derivative is identified almost everywhere with the actual conditional CDF. A rational antiderivative evaluates its square integral, including theta=0 and negative theta; a polynomial/logarithmic antiderivative evaluates the outer integral. Independence gives xi=0 at theta=0. The theta=1 member and the parameter limit at zero are covered in the next row; AMH tau and rho are audited below.
Table 6 / Appendix A.5.1: AMH xi endpoint and independence limit Papers.AnsariRockel2024.amh_chatterjeeXi_one; Papers.AnsariRockel2024.amh_xi_bound_near_zero; Papers.AnsariRockel2024.amh_xi_tendsto_zero verified The actual theta=1 copula has xi=1/6, proved from its conditional CDF and a polynomial energy integral, without substituting into the singular logarithmic formula. Below one, xi also equals 2theta^2 times the integral of v^2(1-v)^2/(1-theta*(1-v)). This representation proves xi<=4*theta^2 for -1<=theta<=1/2. Nonnegativity and squeezing give the two-sided limit zero along every admissible parameter path tending to zero, including sign changes and exact zero values. The xi values are now covered on the full closed AMH parameter interval.
Table 6: AMH Kendall tau on the full closed parameter interval Papers.AnsariRockel2024.amh_kendallTau; Papers.AnsariRockel2024.amh_kendallTau_zero; Papers.AnsariRockel2024.amh_kendallTau_one verified For -1<=theta<1 and theta nonzero, tau=1-2/(3theta)-2(1-theta)^2log(1-theta)/(3theta^2). The actual conditional CDF product is integrated using a rational inner primitive and a logarithmic outer primitive. Independence gives tau=0 at theta=0. At theta=1, the conditional product integral directly gives tau=1/3, with no substitution into a singular formula. The AMH rho formula is audited below.
Table 6: AMH rho reduction to one integral Papers.AnsariRockel2024.amh_spearmanRho_integral; Papers.AnsariRockel2024.amh_spearmanRho_zero verified For -1<=theta<1, theta nonzero, a logarithmic antiderivative integrates the actual CDF in one coordinate. Fubini gives rho=12 times the remaining explicit one-dimensional integral minus 3. The exceptional section v=1 has measure zero and is handled almost everywhere. Independence gives rho=0 at theta=0. This is an intermediate reduction: the printed logarithmic-integral identity is audited below; the theta=1 value is audited below.
Table 6: AMH Spearman rho logarithmic-integral formula Papers.AnsariRockel2024.amh_spearmanRho verified For -1<=theta<1 and theta nonzero, rho=12*(1+theta)/theta^2 times the oriented integral from 1 to 1-theta of log(t)/(1-t), minus 24*(1-theta)log(1-theta)/theta^2 and 3(theta+12)/theta. This is the printed Table 6 identity. A derivative-slope extension proves integrability of the removable singularity, the boundary limit justifies integration by parts, and an affine substitution handles both signs of theta. The zero value is audited above. The theta=1 endpoint is established separately in the following row.
Table 6: AMH rho endpoint and full closed parameter range Papers.AnsariRockel2024.amh_spearmanRho_one; Papers.AnsariRockel2024.amh_spearmanRho_closed verified At theta=1, rho=24 times the oriented integral from 1 to 0 of log(t)/(1-t), minus 39. Integrability is proved separately near each endpoint; continuity of x*log(x) supplies the boundary term at one. The actual copula CDF integral is evaluated, rather than substituting into the below-one proof. The logarithmic-integral formula therefore extends to every nonzero theta in [-1,1], using the continuous extension of the vanishing log coefficient at one. Together with the separate zero values, all three AMH Table 6 association formulas are covered on the full closed parameter interval.
Table 6: Frank Kendall tau on the full signed parameter range Papers.AnsariRockel2024.frank_conditionalCDF; Papers.AnsariRockel2024.frank_kendallTau; Papers.AnsariRockel2024.frank_kendallTau_zero verified For every nonzero real theta, the actual signed Frank copula has tau=1-4/theta*(1-D1(theta)), where D1(theta)=(1/theta) times the oriented integral from zero to theta of t/(exp(t)-1). The CDF derivative identifies the actual conditional distribution almost everywhere. A logarithmic antiderivative gives the conditional-product inner integral 1/theta-v/(exp(theta*v)-1). A continuous derivative-slope extension justifies the removable singularity at zero, and affine substitution yields the Debye normalization for either sign. The theta=0 copula has tau=0. Frank rho is audited below.
Table 6: signed Debye support for Frank association formulas Papers.AnsariRockel2024.frank_debyeTwo_kernel_integral; Papers.AnsariRockel2024.frank_debyeOne_neg; Papers.AnsariRockel2024.frank_debyeTwo_neg verified The second Debye function has exactly the printed normalization 2/theta^2 times the oriented integral of t^2/(exp(t)-1). Its regular kernel integral is proved, with the removable singularity handled by the reciprocal exponential derivative slope. For nonzero theta, D1(-theta)=D1(theta)+theta/2 and D2(-theta)=D2(theta)+2*theta/3. These are analytic support for the rho calculation audited below.
Frank association reflection and independence Papers.AnsariRockel2024.frank_kendallTau_neg; Papers.AnsariRockel2024.frank_spearmanRho_zero; Papers.AnsariRockel2024.frank_spearmanRho_neg verified The actual signed Frank family has odd Kendall tau and odd Spearman rho on the entire real line; both are zero at independence. Tau follows from the verified Debye formula and its reflection identity. Rho follows from the actual negative-parameter copula constructor and the rank coefficient reflection theorem. The nonzero rho formula is audited below.
Table 6: Frank Spearman rho on the full signed parameter range Papers.AnsariRockel2024.frank_spearmanRho verified For every nonzero real theta, the actual signed Frank copula has rho=1-12/theta*(D1(theta)-D2(theta)), with exactly the oriented-integral normalizations printed in Table 6. A logarithmic antiderivative integrates the actual conditional CDF in its threshold coordinate. The general conditional-CDF formula for rho, Fubini, and unit-interval reflection reduce the weighted integral to the first and second Debye integrals. No sign restriction or numerical integration is used. The separate independence result gives rho=0 at theta=0. Together with tau, this completes the printed Frank Table 6 formulas.
Table 6: positive-Clayton Kendall tau and endpoint values Papers.AnsariRockel2024.clayton_positive_conditionalCDF; Papers.AnsariRockel2024.clayton_positive_kendallTau; Papers.AnsariRockel2024.clayton_zero_kendallTau; Papers.AnsariRockel2024.clayton_negative_one_kendallTau verified For every theta>0, the actual Clayton copula has tau=theta/(theta+2). The analytic CDF derivative identifies its actual conditional CDF almost everywhere. A power of the actual clamped CDF supplies a continuous primitive whose nonnegative derivative is the conditional-CDF product. Its integral is v/(theta+2), including the grounded endpoint by continuity; the outer integral gives tau. Independence has tau=0, and the theta=-1 member has tau=-1. The negative branch is audited below; the positive-parameter hypergeometric xi formula is audited below.
Table 6: negative-Clayton Kendall tau and completion of the signed formula Papers.AnsariRockel2024.clayton_negative_conditionalCDF; Papers.AnsariRockel2024.clayton_negative_kendallTau verified For every -1<=theta<0, the actual negative-Clayton copula has tau=theta/(theta+2). For the interior parameters, the positive-part power is differentiable even at its cutoff, proved by matching the two one-sided derivatives. This identifies the actual conditional CDF throughout the truncated region and yields a continuous CDF-power primitive for its product. The primitive gives v/(theta+2); the separate lower-Frechet endpoint handles theta=-1. Together with the positive and independence rows, the tau formula is now checked on the entire admissible interval [-1,infinity). The positive-parameter hypergeometric xi expression is audited below.
Table 6 and Appendix A.5.1, equation (26): positive Clayton xi Papers.AnsariRockel2024.clayton_positive_chatterjeeXi verified For every theta>0, xi is six times the integral of the printed hypergeometric expression minus two. The function is defined by the exact gamma-normalized Euler integral in equation (26). The actual conditional CDF is squared and rewritten, the unit-interval power substitution is proved including its potentially singular endpoint, and the Gamma recurrence gives the required normalization.
Table 6 Gumbel-Hougaard tau: conditional law and generator-coordinate reduction Papers.AnsariRockel2024.gumbel_conditionalCDF; Papers.AnsariRockel2024.gumbel_kendallTau_generator_integral verified For every finite theta>=1, the actual conditional CDF equals the analytic partial derivative almost everywhere. Symmetry and disintegration give the cross-conditional product integral. The substitution u=exp(-x^(1/theta)) in both coordinates cancels the generator weights and reduces tau to one minus four times the positive-quadrant integral of the squared inverse-generator derivative at x+y. Evaluation to (theta-1)/theta is audited below; the printed rho integral is audited below.
Table 6: Gumbel-Hougaard Kendall tau Papers.AnsariRockel2024.gumbel_kendallTau verified For every finite theta>=1, including independence at theta=1, the actual copula has tau=(theta-1)/theta. A nonnegative quadrant-integration identity reduces the squared inverse-generator derivative to its first weighted moment. Power substitution and the Gamma integral evaluate this moment as 1/(4*theta); integrability follows from its nonzero checked value.
Table 6 Gumbel-Hougaard rho: single-integral reduction Papers.AnsariRockel2024.gumbel_spearmanRho_ratio_integral verified For every finite theta>=1, rho equals 12 times the integral over s>0 of 1/(1+s+(1+s^theta)^(1/theta))^2, minus three. The proof starts from the actual copula CDF, substitutes logarithmic coordinates, establishes integrability by an exponential bound, and uses a checked quadrant scaling and homogeneity argument. The radial integral is evaluated by the Gamma identity. The final change to the unit-interval expression printed in Table 6 is audited below.
Table 6: Gumbel-Hougaard Spearman rho Papers.AnsariRockel2024.gumbel_spearmanRho verified The exact printed unit-interval integral holds for every finite theta>=1. Starting from the verified ratio integral, power substitution and the bijection t -> t/(1-t) map the positive half-line onto the open unit interval. The derivative and image are checked, and real-power identities give the printed integrand and factor 12/theta. Measure-zero endpoints require no extra smoothness assumption. Together with the tau row, both printed Gumbel-Hougaard Table 6 entries are complete.
Gaussian family: actual construction and benchmark members Papers.AnsariRockel2024.gaussian_correlation_admissible; Papers.AnsariRockel2024.gaussian_zero; Papers.AnsariRockel2024.gaussian_one; Papers.AnsariRockel2024.gaussian_symmetric; Papers.AnsariRockel2024.gaussian_zero_association; Papers.AnsariRockel2024.gaussian_one_association verified The matrix with diagonal one and off-diagonal r is positive semidefinite exactly when -1<=r<=1. The actual Gaussian probability-integral-transform construction therefore defines the family on its full signed range. The zero member is independence, the one member is comonotonic, and every member is symmetric. Rho, tau and xi are all zero at r=0 and one at r=1. The negative endpoint and rank sign identities are audited below; all three general rank formulas are now proved below, with the corrected xi expression; the remaining Gaussian dependence cells are verified in the rows below.
Table 6 Gaussian xi: printed real-domain failure Papers.AnsariRockel2024.gaussian_printed_xi_argument_outside_domain; Papers.AnsariRockel2024.gaussian_printed_xi_argument_counterexample verified The literal arcsine argument 1/2+r^2/(1+r) exceeds one for every -1<r<-1/2, although these are admissible Gaussian correlations. At r=-3/4 it is exactly 11/4. Thus the printed expression is outside the classical real arcsine domain on this interval. This checks a source-domain failure, not a corrected Gaussian xi formula or a value obtained by totalizing arcsine outside its domain. The arXiv v3 PDF page 19 and HTML agree; the journal cell remains unchecked.
Gaussian signed family: reflection, negative endpoint and rank symmetries Papers.AnsariRockel2024.gaussian_neg; Papers.AnsariRockel2024.gaussian_negative_one; Papers.AnsariRockel2024.gaussian_negative_one_association; Papers.AnsariRockel2024.gaussian_xi_neg; Papers.AnsariRockel2024.gaussian_rho_neg; Papers.AnsariRockel2024.gaussian_tau_neg verified Negating the second Gaussian coordinate changes correlation r to -r, proved by Gaussian mean/covariance uniqueness. The normal CDF complement identity transfers this to reflection of the actual copula. Hence the r=-1 member is countermonotonic, with rho=tau=-1 and xi=1. On the full closed correlation interval, xi is even and rho/tau are odd.
Table 6 Gaussian xi: contradiction inside the arcsine domain Papers.AnsariRockel2024.gaussian_printed_xi_formula_false verified The literal printed formula cannot hold for the actual Gaussian family on its signed parameter range. It gives one at r=-1/2 and strictly less than one at r=1/2, contradicting the proved equality of actual xi at opposite correlations. Both arguments (one and two-thirds) lie in [-1,1], so this refutation does not depend on conventions for arcsine outside its domain. The corrected general Gaussian xi formula is proved below.
Gaussian actual law and Table 6 rho reduction Papers.AnsariRockel2024.gaussian_toMeasure_independent; Papers.AnsariRockel2024.gaussian_rho_normal_integral verified For every r in [-1,1], the actual Gaussian copula measure is the law of the normal CDFs of X and rX+sqrt(1-r^2)Y for independent standard normals X,Y. Gaussian mean/covariance uniqueness verifies the linear map, including both singular endpoints. Spearman rho is then 12 times the expectation of the product of those two CDF values minus three. The arcsine evaluation is proved below.
Gaussian rank-formula support: wedge and normal-CDF integrals Papers.AnsariRockel2024.gaussian_wedge_probability; Papers.AnsariRockel2024.gaussian_halfline_cdf_integral verified For independent standard normals, the first-quadrant wedge with slope a>=0 has probability arctan(a)/(2pi). Quadrant scaling and a radial power substitution reduce its density integral to the arctangent primitive; exponential domination establishes integrability. Consequently the integral of Phi(ax) over positive x against the standard normal law is 1/4+arctan(a)/(2*pi), for every real a, using reflection for negative slopes. These analytic identities support the Kendall tau, Spearman rho and corrected xi formulas below.
Table 6 Gaussian Kendall tau: full signed parameter range Papers.AnsariRockel2024.gaussian_kendallTau verified The actual Gaussian copula has tau=(2/pi)*arcsin(r) for every r in [-1,1]. The normal half-line integral gives both Gaussian quadrant probabilities. Strict monotonicity of the normal CDF transfers coordinate comparisons to the original Gaussian variables. A characteristic-function proof shows that the normalized difference of two independent centered Gaussian copies has the same law; the general Kendall probability identity then gives the formula. The singular endpoints use the checked comonotonic and countermonotonic members.
Table 6 Gaussian Spearman rho: full signed parameter range Papers.AnsariRockel2024.gaussian_spearmanRho verified The actual Gaussian copula has rho=(6/pi)*arcsin(r/2) for every r in [-1,1]. A cross-CDF probability identity compares the copula with an independent copula. Characteristic functions show that a normalized difference of independent Gaussian pairs with correlations r and s has correlation (r+s)/2. Taking one correlation to be zero reduces rho to the checked lower-quadrant probability at r/2, including the original singular endpoints.
Gaussian conditional CDF and xi reduction Papers.AnsariRockel2024.gaussian_cdf_normal; Papers.AnsariRockel2024.gaussian_conditionalCDF_normal; Papers.AnsariRockel2024.gaussian_xi_normal_integral verified For -1<r<1, the actual copula CDF at (Phi(a),Phi(b)) is the integral over x<=a of Phi((b-r*x)/sqrt(1-r^2)) against the standard normal law. Equality of all lower-interval integrals identifies the actual conditional CDF almost everywhere in normal coordinates. The probability integral transform then reduces actual xi to six times the double normal expectation of that conditional CDF squared, minus two. The corrected arcsine evaluation is proved below.
Table 6 Gaussian Chatterjee xi: corrected full signed formula Papers.AnsariRockel2024.gaussian_chatterjeeXi verified The actual Gaussian copula has xi=(3/pi)*arcsin((1+r^2)/2)-1/2 for every r in [-1,1]. Four independent standard normals represent the squared conditional-CDF integral as a quadrant event. Characteristic functions identify its normalized Gaussian pair as having correlation (1+r^2)/2, and the checked quadrant formula evaluates the probability. Both singular endpoints give xi=1. This proves the corrected expression, while the literal arXiv v3 expression remains formally refuted above. Gaussian rho, tau and corrected xi formulas are now complete.
Gaussian conditional CDF in copula coordinates and interior monotonicity Papers.AnsariRockel2024.gaussian_conditionalCDF_quantile; Papers.AnsariRockel2024.gaussian_conditional_antitoneOn; Papers.AnsariRockel2024.gaussian_conditional_monotoneOn verified A measurable normal quantile is a two-sided inverse on the open unit interval and is strictly increasing there. For -1<r<1 and an interior response threshold, the actual conditional CDF equals Phi((Phi-inverse(v)-r*Phi-inverse(u))/sqrt(1-r^2)) almost everywhere under uniform conditioning. This version is antitone on interior conditioning points for r>=0 and monotone there for r<=0. Extension across null endpoints and the exact CI/CD classifications are proved below.
Gaussian exact conditional and quadrant dependence classifications Papers.AnsariRockel2024.gaussian_isCI_iff; Papers.AnsariRockel2024.gaussian_isCD_iff; Papers.AnsariRockel2024.gaussian_isPQD_iff; Papers.AnsariRockel2024.gaussian_isNQD_iff verified On the entire closed correlation interval [-1,1], the actual Gaussian copula is CI and PQD exactly when r>=0, and CD and NQD exactly when r<=0. The identified conditional CDF extends antitonically across null conditioning endpoints; integration proves the concavity inequalities for nonnegative r. Symmetry gives both coordinate directions and reflection gives the decreasing case. The checked Spearman formula excludes the opposite parameter signs. Independence belongs to both classes, and both singular endpoints are included.
Gaussian normal-coordinate density and exact absolute-continuity range Papers.AnsariRockel2024.gaussian_toMeasure_normal_density; Papers.AnsariRockel2024.gaussian_absolutelyContinuous_iff verified For -1<r<1 the actual copula measure is the normal-CDF pushforward of the joint density phi(x)phi_{rx,1-r^2}(y). Affine normal laws and Tonelli identify this density as a measure, rather than only checking a formal derivative. Mutual absolute continuity of standard normal and Lebesgue measures and the CDF pushforward give absolute continuity on the copula square. It holds exactly in the interior: the two singular benchmark endpoints are excluded. The explicit unit-square density is checked separately below; density TP2 is checked separately below.
Gaussian unit-square density Papers.AnsariRockel2024.gaussian_density verified The conditional-normal density divided by the standard normal density, evaluated at measurable normal quantiles, is identified with the actual copula measure for -1<r<1. Boundary values are set to zero. Its TP2 classification is checked separately below.
Gaussian exact density-TP2 classification Papers.AnsariRockel2024.gaussian_hasMTP2Density_iff verified The actual Gaussian copula has a TP2 Lebesgue density exactly for 0<=r<1. The normal conditional density is TP2 for nonnegative correlation, positive coordinate factors preserve TP2, and increasing normal quantiles transfer it to the copula square. Zero boundary values preserve the inequality. Negative correlations are excluded by PQD, and the singular endpoint by absolute continuity.
Gaussian radial symmetry and both tail coefficients Papers.AnsariRockel2024.gaussian_radiallySymmetric; Papers.AnsariRockel2024.gaussian_lowerTail; Papers.AnsariRockel2024.gaussian_upperTail verified On the full closed correlation interval, both tail coefficients are zero for r<1 and one at r=1. Symmetry bounds the diagonal probability by twice a triangular probability. Conditioning evaluates the triangle and gives the bound C(Phi(a),Phi(a)) <= 2*Phi(a)*Phi((1-r)*a/sqrt(1-r^2)). The measurable normal quantile tends to minus infinity at zero, proving the interior lower-tail limit, including positive correlations. Radial symmetry transfers it to the upper tail; both singular endpoints are checked.
Gaussian exact lower-orthant and Schur parameter orders Papers.AnsariRockel2024.gaussian_lowerOrthant_iff; Papers.AnsariRockel2024.gaussian_schur_iff; Papers.AnsariRockel2024.gaussian_schurBoth_iff verified Throughout [-1,1], lower-orthant order is equivalent to r<=s, while either-direction and both-direction Schur order are equivalent to abs(r)<=abs(s). A single-crossing comparison of the actual conditional normal CDFs gives the forward orthant order; equal total conditional integrals and increasing standardized correlation slopes are checked. The exact Kendall formula proves the converse. Measure-preserving reflection gives Schur equivalence of opposite correlations, and the CI/orthant equivalence on nonnegative correlations proves the full signed Schur classification. Singular endpoints and square boundaries are included.
Gaussian parameter continuity and benchmark limits Papers.AnsariRockel2024.gaussian_cdf_continuous; Papers.AnsariRockel2024.gaussian_cdf_tendsto_zero; Papers.AnsariRockel2024.gaussian_cdf_tendsto_one; Papers.AnsariRockel2024.gaussian_cdf_tendsto_negative_one verified For every point of the closed unit square the actual CDF is continuous in correlation on [-1,1]. The independent-normal construction gives a common probability space; dominated convergence applies to the rectangle indicator because the varying coordinate has an atomless uniform marginal at the limiting correlation, including singular endpoints. Thus r tends to 0, 1, or -1 gives independence, M, or W respectively, along every admissible parameter approach.
Student-t construction and positive singular endpoint Papers.AnsariRockel2024.student_isSklarCopula; Papers.AnsariRockel2024.student_one; Papers.AnsariRockel2024.student_one_isCI verified An actual bivariate Student-t copula is constructed for -1<=r<=1 and every real nu>0, using independent gamma precision and a Gaussian vector. Its Sklar factorization is checked. The r=1 member is M, proved from almost-sure equality of the scaled coordinates and their marginal transforms, and hence is CI. The blanket not-CI entry requires an endpoint qualification. The negative endpoint and common marginal law are checked below. Subsequent rows prove the corrected joint density, exact CI/CD classification, density-TP2 exclusion, correlation order, Kendall tau and the scale-expectation rho formula. Both tail coefficients are proved below; the Table 6 rho correspondence is verified in the Heinen–Valdesogo row.
Gaussian negative-endpoint tail correction Papers.AnsariRockel2024.gaussian_negative_one_not_lowerTail_one; Papers.AnsariRockel2024.gaussian_negative_one_not_upperTail_one verified Appendix A.3.3 of arXiv v3 states tail coefficient one at both signed Gaussian endpoints. The r=-1 member is W and has both coefficients zero. Uniqueness of the checked limits formally excludes coefficient one at that endpoint. Journal correspondence remains unchecked.
Student-t negative endpoint and common marginal law Papers.AnsariRockel2024.student_negative_one; Papers.AnsariRockel2024.student_negative_one_isCD; Papers.AnsariRockel2024.student_marginal verified For every real nu>0 the r=-1 member is W and is CD. The proof transports almost-sure negation of the Gaussian coordinates through the positive scale mixture and then through atomless marginal CDFs. Each coordinate marginal is the same gamma-precision mixture of a standard normal, independently of r and the coordinate index. Both closed-interval singular benchmark identities are now checked; the interior CI/CD and density-TP2 exclusions are proved below.
Student-t marginal CDF, strict monotonicity and reflection Papers.AnsariRockel2024.student_marginal_cdf; Papers.AnsariRockel2024.student_marginal_cdf_strictMono; Papers.AnsariRockel2024.student_marginal_cdf_neg verified The actual marginal CDF is the gamma-precision expectation of Phi(a*sqrt(t)), proved by mapping the product law and Tonelli/Fubini. It is strictly increasing for every real nu>0: positive scales preserve the strict normal-CDF inequality almost everywhere, and equality of integrals is excluded. Its reflection identity is F(-a)=1-F(a). These results hold for both coordinates and every admissible correlation, including singular endpoints. The corrected bivariate density, correlation order, conditional-dependence classifications and both tail coefficients are proved below.
Student-t joint CDF and correlation lower-orthant order Papers.AnsariRockel2024.student_joint_cdf; Papers.AnsariRockel2024.student_lowerOrthant_monotone verified For every fixed real nu>0, the actual Student-t copulas increase in lower-orthant order throughout -1<=r<=q<=1. The joint distribution is the gamma-precision expectation of the Gaussian copula CDF at the two scaled normal-CDF arguments. Fubini and the positive scale identify this formula as a probability. Gaussian lower-orthant order survives integration, and a general checked Sklar comparison transfers ordered distributions with identical continuous marginals to copulas by density of the marginal-CDF ranges. Both singular endpoints and the full closed unit square are included.
Table 6 Student-t Kendall tau and exact correlation order Papers.AnsariRockel2024.student_kendallTau; Papers.AnsariRockel2024.student_lowerOrthant_iff verified For every real nu>0 and -1<=r<=1, actual Kendall tau is (2/pi)*arcsin(r). Strict marginal CDFs transfer coordinate comparisons to the copula. Regrouping the independent samples and conditioning on their positive scales reduces the comparison probability to a Gaussian quadrant. Characteristic functions prove that the normalized weighted Gaussian difference has the original correlation law, including singular covariance matrices. The formula and Kendall monotonicity also prove the converse to lower-orthant correlation order: it holds exactly when r<=q.
Student-t signed correlation reflection and rank symmetries Papers.AnsariRockel2024.student_reflect_second; Papers.AnsariRockel2024.student_rho_neg; Papers.AnsariRockel2024.student_tau_neg; Papers.AnsariRockel2024.student_xi_neg verified For every real nu>0 and correlation in [-1,1], negating correlation reflects the second copula coordinate. The proof uses the actual Gaussian scale-mixture measure and its symmetric continuous marginal CDF. Spearman rho and Kendall tau are odd in correlation; directional Chatterjee xi is even. The actual conditional-dependence classifications and scale-expectation rho formula are proved below; the Bessel density and Heinen–Valdesogo rho correspondences are verified in separate rows.
Laplace scale-mixture construction and singular endpoints Papers.AnsariRockel2024.laplace_isSklarCopula; Papers.AnsariRockel2024.laplace_one; Papers.AnsariRockel2024.laplace_negative_one verified The checked family is the Gaussian mixture with independent gamma(1,1), equivalently exponential(1), variance. Its Sklar factorization and the identities C(-1)=W and C(1)=M hold on the closed correlation interval. Identification with the printed Bessel density is verified in a separate row below.
Tables 5 and 6 Laplace correlation order and Kendall tau Papers.AnsariRockel2024.laplace_kendallTau; Papers.AnsariRockel2024.laplace_lowerOrthant_monotone; Papers.AnsariRockel2024.laplace_lowerOrthant_iff verified For every correlation r in [-1,1], actual Kendall tau is (2/pi)*arcsin(r). Lower-orthant order holds exactly when r<=q. These specialize the proved positive Gaussian scale-mixture comparison and common-marginal Sklar results, including both singular endpoints.
Laplace reflection and signed rank symmetries Papers.AnsariRockel2024.laplace_reflect_second; Papers.AnsariRockel2024.laplace_rho_neg; Papers.AnsariRockel2024.laplace_tau_neg; Papers.AnsariRockel2024.laplace_xi_neg verified Negating correlation reflects the second coordinate. Spearman rho and Kendall tau are odd, and directional Chatterjee xi is even. The explicit scale expectation for rho is proved below; its Heinen–Valdesogo form and the interior dependence exclusions are verified in later rows.
Student-t and Laplace exchangeability, radial symmetry and tail equivalence Papers.AnsariRockel2024.student_transpose; Papers.AnsariRockel2024.student_radiallySymmetric; Papers.AnsariRockel2024.student_upperTail_iff_lowerTail; Papers.AnsariRockel2024.laplace_transpose; Papers.AnsariRockel2024.laplace_radiallySymmetric; Papers.AnsariRockel2024.laplace_upperTail_iff_lowerTail verified Both actual copula families are invariant under transposition and simultaneous reflection throughout [-1,1] (every real nu>0 for Student-t). Exchangeability follows from the Gaussian-mixture joint CDF, then extends through dense marginal-CDF ranges. Correlation reflection gives radial symmetry. An upper tail coefficient exists with value lambda exactly when the lower tail coefficient does. The Student-t tail limits and printed interior coefficient are proved below; this symmetry statement alone does not supply the remaining Laplace limits.
Preparatory Gaussian comparison for elliptical Spearman rho Papers.AnsariRockel2024.elliptical_rho_conditional_comparison verified Conditional on fixed scales a,b,c with a^2+b^2>0 and a^2+c^2>0, the probability of both independently perturbed Gaussian coordinates being nonnegative is 1/4+arcsin(q)/(2pi), where q=ra^2/(sqrt(a^2+b^2)*sqrt(a^2+c^2)). Characteristic functions identify the normalized pair as a Gaussian with correlation q; admissibility and the closed-interval quadrant formula are checked. The following row integrates this identity over the random scales and identifies the actual Student-t/Laplace Spearman rho.
Student-t and Laplace actual Spearman rho as explicit scale expectations Papers.AnsariRockel2024.student_spearmanRho; Papers.AnsariRockel2024.laplace_spearmanRho verified On the full closed correlation interval (all real nu>0 for Student-t), rho equals (6/pi) times the expectation of arcsin(r*A^2/(sqrt(A^2+B^2)*sqrt(A^2+C^2))). A,B,C are independent copies of the positive scale: inverse square root of gamma(nu/2,nu/2) precision for Student-t, square root of gamma(1,1) variance for Laplace. The proof identifies the actual copula integral, expands both marginal CDFs, applies Fubini with proved bounded integrability, and uses the Gaussian comparison law. This gives an explicit probability-law version of the Table 6 expectation; the Heinen–Valdesogo form is verified in a separate row below.
Student-t and Laplace actual marginal density and null sets Papers.AnsariRockel2024.student_marginal_withDensity; Papers.AnsariRockel2024.student_marginal_equivalent_volume; Papers.AnsariRockel2024.laplace_marginal_withDensity; Papers.AnsariRockel2024.laplace_marginal_equivalent_volume verified Every marginal is identified with Lebesgue measure weighted by the integral of its scaled normal density over the independent gamma mixing law. Tonelli and the scaled-normal pushforward prove equality of measures. The mixture density is positive everywhere, so the marginal and Lebesgue measure have the same null sets, for every admissible correlation and every real nu>0 for Student-t. The Student-t evaluation is proved in the next row; the Laplace radial evaluation and its printed Bessel form are verified below.
Student-t standard marginal density Papers.AnsariRockel2024.student_marginal_standard_density verified Each actual marginal has density Gamma((nu+1)/2)/(sqrt(nu*pi)*Gamma(nu/2)) times (1+x^2/nu)^(-(nu+1)/2), for every real nu>0 and every correlation in [-1,1]. The Gaussian precision-density identity and a proved power-weighted gamma Laplace integral evaluate the actual mixture, then algebra gives the standard form. No finite-moment assumption is used. The actual standard bivariate Student-t density is evaluated below. The printed Table 1 density uses the correlation symbol where the dimension two belongs; the verified exponent is −(ν+2)/2.
Student-t and Laplace actual joint mixture density Papers.AnsariRockel2024.student_joint_withDensity; Papers.AnsariRockel2024.student_joint_equivalent_volume; Papers.AnsariRockel2024.laplace_joint_withDensity; Papers.AnsariRockel2024.laplace_joint_equivalent_volume verified For -1<r<1 (every real nu>0 for Student-t), the actual bivariate distribution, represented on real pairs, equals planar Lebesgue measure weighted by the positive mixture of scaled Gaussian joint densities. Conditioning and two affine normal pushforwards identify each fixed-scale density; Tonelli identifies the mixed measure. Positivity proves both directions of absolute continuity. The Student-t mixture is evaluated in the following row; the Laplace radial integral and its Bessel form are verified below.
Student-t standard bivariate density Papers.AnsariRockel2024.student_joint_standard_density verified The actual Student-t joint law has density (2pisqrt(1-r^2))^(-1) times (1+(x^2-2rxy+y^2)/(nu(1-r^2)))^(-(nu+2)/2), for every real nu>0 and -1<r<1. The proof combines the scaled Gaussian density factors, evaluates the gamma precision integral, and uses Gamma(a+1)=a*Gamma(a). This proves the standard dimension-two density; the literal arXiv v3 HTML Table 1 expression is refuted below. Singular endpoints are represented by their checked M/W copulas rather than a planar density.
Student-t and Laplace exact copula absolute continuity Papers.AnsariRockel2024.student_absolutelyContinuous_iff; Papers.AnsariRockel2024.laplace_absolutelyContinuous_iff verified The actual copulas are absolutely continuous with respect to unit-square Lebesgue measure exactly for -1<r<1 (every real nu>0 for Student-t). The joint density gives domination by planar Lebesgue measure, positive marginal densities give domination by the product of marginals, and the injective marginal CDF transform maps that product to the independence measure. The r=-1 and r=1 members are the singular W and M copulas. This does not prove density TP2 or the remaining CI/CD exclusions.
arXiv v3 HTML Table 1 Student-t density symbol discrepancy Papers.AnsariRockel2024.student_joint_printed_density_counterexample; Papers.AnsariRockel2024.student_joint_printed_formula_false verified The literal expression places correlation r in the dimension slots: Gamma((nu+r)/2), nu^(r/2), pi^(r/2), and exponent -(nu+r)/2. At r=0, nu=2 and (x,y)=(0,0), it equals 1, while the proved standard density equals 1/(2*pi)<1. Thus the universal pointwise identity with that literal expression is false. This is a pointwise formula refutation, not a standalone assertion about equality of measures from a single point. The standard dimension-two density is proved above; PDF/journal correspondence for this discrepancy remains unchecked.
Student-t posterior precision and normalized conditional density Papers.AnsariRockel2024.student_precision_measure_update; Papers.AnsariRockel2024.student_joint_density_factorization; Papers.AnsariRockel2024.student_conditional_density_normalized verified Weighting gamma(nu/2,nu/2) precision by the observed normal density at x gives the actual marginal density at x times gamma((nu+1)/2,(nu+x^2)/2). The actual joint density factors into this marginal density and the resulting normal-mixture conditional density, which integrates to one for every x, every real nu>0 and -1<r<1. The proof uses the checked gamma power-tilt identity, equality of weighted measures and Tonelli. Identification with a shifted/scaled Student-t CDF is proved below; the actual copula conditional CDF is identified below, and the exact CI/CD classifications are proved below.
Student-t normalized conditional-law CDF Papers.AnsariRockel2024.student_conditional_cdf_mixture verified For every x,y, real nu>0 and -1<r<1, the CDF of the normalized density from the preceding factorization is the gamma((nu+1)/2,(nu+x^2)/2) expectation of Phi((y-r*x)*sqrt(t)/sqrt(1-r^2)). A checked translated Gaussian scale-mixture measure has exactly that density; its CDF follows from the probability integral and affine threshold identity. The shifted/scaled Student-t(nu+1) CDF form is proved below; identification with the actual copula conditional CDF is proved below.
Student-t standardized conditional-law CDF Papers.AnsariRockel2024.student_conditional_cdf_standard verified For all real nu>0, -1<r<1 and x,y, the normalized conditional density has CDF equal to the actual Student-t(nu+1) marginal CDF at (y-rx)/sqrt((nu+x^2)(1-r^2)/(nu+1)). A checked gamma scaling identity transports the posterior precision law to gamma((nu+1)/2,(nu+1)/2). This closes the standard Student-t form of the density-factorization conditional law; the actual copula conditional CDF is identified below, and the exact CI/CD classifications are proved below.
Student-t conditional kernel and joint-law disintegration Papers.AnsariRockel2024.student_joint_disintegration; Papers.AnsariRockel2024.student_conditional_kernel_isMarkov; Papers.AnsariRockel2024.student_joint_eq_compProd; Papers.AnsariRockel2024.student_joint_rectangle_conditional verified For every real nu>0 and -1<r<1, the normalized conditional density is jointly measurable and defines a Markov kernel. The actual bivariate Student-t law on real pairs is exactly the composition-product of its first marginal and this kernel. The iterated-integral identity holds for every nonnegative measurable function, and lower-rectangle probabilities are the marginal integrals of the conditional CDF. Thus the shifted/scaled Student-t(nu+1) formula above describes a conditional law of the actual joint distribution; transportation to the actual copula conditional CDF is proved below; The exact CI/CD classifications are proved below.
Student-t actual copula conditional CDF Papers.AnsariRockel2024.student_cdf_conditional; Papers.AnsariRockel2024.student_conditionalCDF_standard verified For every real nu>0, -1<r<1 and real response threshold b, the actual copula conditional CDF at the two marginal CDF coordinates equals the Student-t(nu+1) marginal CDF at (b-rx)/sqrt((nu+x^2)(1-r^2)/(nu+1)), almost everywhere in the Student-t conditioning marginal. The proof transports the checked joint-law rectangle identity through continuous strictly increasing marginal CDFs, then uses equality of all lower-interval integrals. The almost-everywhere statement is proved separately for every b; The exact CI/CD classifications are proved below.
Table 5 Student-t exact CI/CD classification and density-TP2 exclusion Papers.AnsariRockel2024.student_isSI_iff; Papers.AnsariRockel2024.student_isCI_iff; Papers.AnsariRockel2024.student_isSD_iff; Papers.AnsariRockel2024.student_isCD_iff; Papers.AnsariRockel2024.student_not_hasMTP2Density verified For every real nu>0 and r in [-1,1], the actual Student-t copula is SI/CI exactly at r=1 and SD/CD exactly at r=-1; it has no MTP2 Lebesgue density anywhere in this interval. For interior r, at response threshold 3*sqrt(nu) the standardized conditional threshold increases between -sqrt(nu) and zero. The strictly increasing Student-t(nu+1) CDF transfers this counterexample to a continuous conditional-CDF version. Positive marginal density and a dense-set argument rule out any almost-everywhere antitone version. Reflection gives the decreasing exclusion. The singular endpoint identities complete the classifications; MTP2 density would imply CI and absolute continuity, excluding both interior and endpoint parameters. This supplies the required interior qualification to the source blanket not-CI claim.
Student-t exact diagonal and tail-ratio integral Papers.AnsariRockel2024.student_diagonal_integral; Papers.AnsariRockel2024.student_lowerTailRatio_integral verified For every real nu>0, -1<r<1 and real threshold a, the copula diagonal at F_nu(a) is twice the marginal integral over x<=a of the Student-t(nu+1) CDF at (x-rx)/sqrt((nu+x^2)(1-r^2)/(nu+1)). Dividing by F_nu(a) gives the actual lower-tail ratio. Exchangeability splits the diagonal square into two equal triangles; absolute continuity makes their diagonal overlap null. The checked conditional kernel evaluates the triangle integral. This is an exact finite-threshold reduction; its limiting coefficient is proved in the following row.
Table 3 Student-t lower and upper tail coefficients Papers.AnsariRockel2024.student_lowerTail_interior; Papers.AnsariRockel2024.student_upperTail_interior; Papers.AnsariRockel2024.student_lowerTail; Papers.AnsariRockel2024.student_upperTail verified Both actual tail limits exist for every real nu>0 and r in [-1,1]. For -1<r<1 they equal 2-2t_(nu+1)(sqrt((nu+1)(1-r)/(1+r))), where t_(nu+1) is the actual standardized Student-t marginal CDF. At r=1 both equal one; at r=-1 both equal zero. The proof combines the exact diagonal integral, the limit of the standardized conditional threshold as x tends to minus infinity, continuity and symmetry of the Student-t CDF, and a checked tail-average limit. A continuous strictly increasing CDF inverse transfers the real-threshold limit to the actual copula tail filter. Radial symmetry gives the upper tail; singular endpoints are handled separately.
Student-t and Laplace correlation continuity and singular limits Papers.AnsariRockel2024.student_cdf_continuous; Papers.AnsariRockel2024.laplace_cdf_continuous; Papers.AnsariRockel2024.student_cdf_tendsto_one; Papers.AnsariRockel2024.student_cdf_tendsto_negative_one; Papers.AnsariRockel2024.laplace_cdf_tendsto_one; Papers.AnsariRockel2024.laplace_cdf_tendsto_negative_one verified At every point of the closed unit square, both actual copula CDFs depend continuously on correlation throughout [-1,1], with every fixed real nu>0 for Student-t. As correlation tends to one they converge to M, and as it tends to minus one they converge to W. The general positive Gaussian-scale-mixture proof uses correlation-independent continuous marginals, their interior CDF surjectivity and dominated convergence of the Gaussian CDF integral; square boundaries are handled by copula boundary identities. The separate Student degrees-of-freedom limit as nu tends to infinity is proved below.
Table 5 Laplace non-CI range, zero-correlation dependence and signed exclusions Papers.AnsariRockel2024.laplace_not_independent_zero; Papers.AnsariRockel2024.laplace_not_isPQD_nonpositive; Papers.AnsariRockel2024.laplace_not_isNQD_nonnegative; Papers.AnsariRockel2024.laplace_not_isCI_nonpositive; Papers.AnsariRockel2024.laplace_not_isCD_nonnegative; Papers.AnsariRockel2024.laplace_not_hasMTP2Density_nonpositive verified The actual Laplace copula is neither PQD nor CI for -1<=r<=0, neither NQD nor CD for 0<=r<=1, and has no MTP2 density for nonpositive r. The zero-correlation copula is dependent: its diagonal mixture integral is a second moment of Phi(1/sqrt(t)); independence would force variance zero, hence constancy on the gamma law positive support, contradicted at t=1 and t=4. This argument applies to every positive gamma shape and rate. Zero Kendall tau and strict concordance exclude quadrant dependence at zero; the checked arcsine tau formula excludes the remaining parameter signs. The full MTP2-density exclusion is proved below; remaining Laplace analytic formulas are separate claims.
Laplace joint radial integral Papers.AnsariRockel2024.laplace_joint_radial_density; Papers.AnsariRockel2024.laplace_radial_density_antitone verified For -1<r<1, the actual joint law has density (2pisqrt(1-r^2))^(-1) times the nonnegative integral over t>0 of exp(-t-Q/(2t))/t, where Q=(x^2-2rxy+y^2)/(1-r^2). The proof evaluates the scaled Gaussian product and the gamma(1,1) mixing density and identifies the weighted planar measure. The radial integral is decreasing in Q. It is allowed to take the extended value infinity; no finiteness at the origin is assumed. Identification with the printed Bessel function is verified below; the full MTP2 exclusion is proved below.
Laplace radial density finiteness, continuity and origin blow-up Papers.AnsariRockel2024.laplace_radial_density_finite; Papers.AnsariRockel2024.laplace_radial_density_origin; Papers.AnsariRockel2024.laplace_radial_density_blowup; Papers.AnsariRockel2024.laplace_radial_density_continuous verified The radial integral is finite and continuous at every positive quadratic radius, equals infinity at zero, and tends to infinity as the radius tends to zero. A bound by (2/q)*exp(-t) proves integrability for q>0; comparison with 1/t on (0,1) proves divergence at zero. Fatou proves the full blow-up limit, and local domination proves continuity away from zero. These analytic properties of the identified joint density support the full MTP2-density exclusion proved below.
Laplace explicit joint-density TP2 counterexample Papers.AnsariRockel2024.laplace_joint_density_tp2_counterexample verified For every -1<r<1, there exists 0<t<1 for which the actual normalized Gaussian-mixture joint density satisfies f(-1,0)*f(t,1)<f(-1,1)*f(t,0), violating TP2 at four nonzero points. The radial factor is positive everywhere, finite and continuous away from zero, and diverges near zero; a limit comparison gives the strict witness and the positive finite normalizer cancels. This result concerns the explicit density version. The next rows exclude all equivalent joint-density versions and transfer the exclusion to the copula.
Laplace joint-law TP2 exclusion for every density version Papers.AnsariRockel2024.laplace_joint_no_tp2_density_version verified For every interior correlation, no nonnegative measurable real-valued TP2 density represents the actual joint Laplace law. Equality of weighted measures gives almost-everywhere equality with the explicit mixture density. A general real-plane continuity lemma transfers almost-everywhere ordered minors to strict rectangles of continuity, contradicting the checked four-point witness. This excludes arbitrary null-set changes, not merely the displayed density version. The next row transfers this exclusion to the copula.
Table 5 full Laplace copula density-TP2 exclusion Papers.AnsariRockel2024.laplace_not_hasMTP2Density verified No Laplace copula with -1<=r<=1 has an MTP2 Lebesgue density. For interior correlation, a general positive Gaussian-scale-mixture transfer theorem pulls any copula TP2 density back through the injective marginal CDFs and multiplies by the nonnegative marginal density factors, producing a joint TP2 density, which the checked joint-law exclusion rules out. The proof identifies the pulled-back measure and preserves TP2 without assuming a closed marginal formula. At both singular endpoints, absolute continuity is impossible. This completes the Laplace density-TP2 column, including all positive correlations.
Student Gaussian-limit support: gamma precision concentration Papers.AnsariRockel2024.student_precision_centered_second_moment; Papers.AnsariRockel2024.student_precision_concentration_bound; Papers.AnsariRockel2024.student_precision_concentrates verified For every real nu>0, the actual gamma(nu/2,nu/2) precision has centered second moment 2/nu, and P(abs(T-1)>=epsilon)<=2/(nu*epsilon^2) for every epsilon>0. The probability tends to zero along every positive degrees-of-freedom parameter tending to infinity. Gamma power integrals prove both raw moments and integrability, followed by Markov applied to the centered square. These supporting results are used in the Student marginal, joint and copula Gaussian limits below.
Student degrees-of-freedom Gaussian limit Papers.AnsariRockel2024.student_marginal_gaussian_limit; Papers.AnsariRockel2024.student_joint_gaussian_limit; Papers.AnsariRockel2024.student_copula_gaussian_limit_interior; Papers.AnsariRockel2024.student_copula_gaussian_limit verified For every fixed correlation in [-1,1], every positive real degrees-of-freedom parameter tending to infinity, and every point of the closed unit square, the actual Student copula CDF tends to the actual Gaussian copula CDF. Both actual Student marginal CDFs tend to the standard normal CDF, and all joint lower-rectangle probabilities tend to the corresponding Gaussian values. Gamma precision concentration yields convergence of bounded expectations continuous at precision one. Sklar factorization and the universal copula Lipschitz bound replace moving marginal coordinates with fixed interior coordinates; boundary identities handle the square edges. Singular correlations are included.
Tables 1 and 4: actual Galambos constructor and full-square CDF Papers.AnsariRockel2024.galambos_cdf_full; Papers.AnsariRockel2024.galambos_cdf_interior; Papers.AnsariRockel2024.galambos_survivalClayton_maxima_limit verified For every delta>0, an actual copula measure is constructed with interior CDF uvexp(((-log u)^(-delta)+(-log v)^(-delta))^(-1/delta)), grounded axes, and uniform upper edges. The construction takes normalized maxima of independent survival-Clayton copies. The exact finite-block CDF, scaled Clayton lower-tail limit, power-root asymptotic and exponential power limit give pointwise convergence on the closed square; copula compactness identifies a measure with that CDF. Max-stability, CI and the interior Pickands correspondence are checked below; both parameter limits are checked below.
Tables 4–5: Galambos max-stability, CI and Pickands formula Papers.AnsariRockel2024.galambos_isExtremeValue; Papers.AnsariRockel2024.galambos_isCI; Papers.AnsariRockel2024.galambos_pickands_interior verified Max-stability holds on the entire closed unit square for every delta>0. The general extreme-value theorem gives CI without a density hypothesis. The canonical Pickands function equals 1-(t^(-delta)+(1-t)^(-delta))^(-1/delta) for 0<t<1. Both parameter limits are checked below.
Table 5: Galambos tail coefficients Papers.AnsariRockel2024.galambos_power_diagonal; Papers.AnsariRockel2024.galambos_extremalCoefficient; Papers.AnsariRockel2024.galambos_tails verified For every delta>0 the full closed-interval diagonal is t^(2-2^(-1/delta)), with that exponent as extremal coefficient. The exponent is strictly above one, so the lower-tail coefficient is zero; the upper-tail coefficient is 2^(-1/delta).
Table 5: exact Galambos parameter orders Papers.AnsariRockel2024.galambos_pickands_antitone; Papers.AnsariRockel2024.galambos_lowerOrthant_mono; Papers.AnsariRockel2024.galambos_schurBoth_mono; Papers.AnsariRockel2024.galambos_lowerOrthant_iff; Papers.AnsariRockel2024.galambos_schurBoth_iff verified For all positive delta and epsilon, lower-orthant order and both-direction Schur order hold exactly when delta<=epsilon. The canonical Pickands function decreases with the parameter by the two-variable power-norm inequality. Max-stability and CI transfer this comparison to copula orders; the upper-tail coefficient proves the converse. Both parameter limits are checked below.
Table 4: Galambos limit at infinity Papers.AnsariRockel2024.galambos_limit_comonotonic verified For every positive parameter family tending to infinity along any filter, the actual Galambos CDF tends to the comonotonic CDF at every point of the closed unit square. A general diagonal squeeze transfers convergence of the power-diagonal exponent to one into full CDF convergence. The independence limit as delta tends to zero is checked below.
Table 4: Galambos independence limit at zero Papers.AnsariRockel2024.galambos_limit_independence_interior; Papers.AnsariRockel2024.galambos_limit_independence verified For every positive parameter family tending to zero along any filter, the actual Galambos CDF tends to independence at every point of the closed unit square. The positive-logarithm correction is bounded by max(x,y)*2^(-1/delta), which tends to zero. Interior CDF convergence and copula boundary identities complete the proof. Both Galambos parameter limits are now checked.
Tables 1, 4 and 5: asymmetric Joe extreme-value constructor, CDF and CI Papers.AnsariRockel2024.joeExtremeValue_isExtremeValue; Papers.AnsariRockel2024.joeExtremeValue_isCI; Papers.AnsariRockel2024.joeExtremeValue_cdf_product; Papers.AnsariRockel2024.joeExtremeValue_cdf_interior; Papers.AnsariRockel2024.joeExtremeValue_unit_weights; Papers.AnsariRockel2024.joeExtremeValue_zero_weight verified An actual copula is constructed for delta>0 and both weights in [0,1] as a power-weighted maximum product of Galambos and independence. Its full-square product CDF is checked; on positive weights and interior coordinates it equals uvexp(((alpha*(-log u))^(-delta)+(beta*(-log v))^(-delta))^(-1/delta)). It is max-stable and CI on the entire weight range. Unit weights give Galambos, and either zero weight gives independence. Parameter orders in delta and both parameter limits are checked below; Pickands correspondence is checked below; explicit tails are checked below; weight orders are checked below. This is the extreme-value Joe family, distinct from the Archimedean Joe family above.
Tables 4–5: asymmetric Joe extreme-value orders and parameter limits Papers.AnsariRockel2024.joeExtremeValue_lowerOrthant_mono; Papers.AnsariRockel2024.joeExtremeValue_schurBoth_mono; Papers.AnsariRockel2024.joeExtremeValue_limit_marshallOlkin; Papers.AnsariRockel2024.joeExtremeValue_limit_independence verified For each fixed pair of weights in [0,1], increasing delta increases the copula in lower-orthant and both-direction Schur order. As delta tends to zero, its CDF tends to independence; as delta tends to infinity, it tends to Marshall–Olkin with the same weights. Both limits hold along arbitrary positive parameter families and on the entire closed square, including degenerate weights. The proofs transfer Galambos order and limits through the actual maximum-product construction.
Table 4: asymmetric Joe extreme-value Pickands correspondence Papers.AnsariRockel2024.joeExtremeValue_pickands_interior; Papers.AnsariRockel2024.joeExtremeValue_pickands_zero_weight; Papers.AnsariRockel2024.joeExtremeValue_pickands_endpoints verified The canonical Pickands function of the actual copula equals 1-((alpha*(1-t))^(-delta)+(beta*t)^(-delta))^(-1/delta) for positive weights and 0<t<1. It equals one at both endpoints for all weights, and is identically one if either weight is zero. The boundary cases supply the continuous extension instead of evaluating negative real powers at zero.
Table 5: asymmetric Joe extreme-value tail coefficients Papers.AnsariRockel2024.joeExtremeValue_extremalCoefficient; Papers.AnsariRockel2024.joeExtremeValue_tails verified For delta>0 and positive weights, the extremal coefficient is 2-(alpha^(-delta)+beta^(-delta))^(-1/delta), strictly greater than one. The lower-tail coefficient is zero for every weight pair; the upper-tail coefficient is (alpha^(-delta)+beta^(-delta))^(-1/delta) for positive weights and zero if either weight is zero. A general checked identity equates the extremal coefficient with twice the canonical Pickands midpoint.
Table 5: asymmetric Joe extreme-value weight and joint parameter orders Papers.AnsariRockel2024.joeExtremeValue_weight_lowerOrthant_mono; Papers.AnsariRockel2024.joeExtremeValue_weight_schurBoth_mono; Papers.AnsariRockel2024.joeExtremeValue_allParameters_lowerOrthant_mono; Papers.AnsariRockel2024.joeExtremeValue_allParameters_schurBoth_mono verified Increasing either or both weights increases the actual copula in lower-orthant and both-direction Schur order, on the entire [0,1] weight square. The same conclusions hold when delta and both weights increase together. Positive weights use the canonical Pickands formula and two reversals of negative-power order; zero-weight starting copulas use independence and CI-implied positive quadrant dependence.
Figure 2 discussion / Table 4: uniform Galambos and Joe extreme-value endpoint limits Papers.AnsariRockel2024.galambos_limit_independence_uniform; Papers.AnsariRockel2024.galambos_limit_comonotonic_uniform; Papers.AnsariRockel2024.joeExtremeValue_limit_independence_uniform; Papers.AnsariRockel2024.joeExtremeValue_limit_marshallOlkin_uniform verified The Galambos limits to independence and comonotonicity, and the asymmetric Joe limits to independence and Marshall–Olkin, hold uniformly on the entire closed square. The Joe results include every fixed weight pair in [0,1]. A general fixed-dimensional copula lemma upgrades pointwise CDF convergence to uniform convergence: the common Lipschitz bound gives equicontinuity, and the domain is compact. This verifies the stronger uniform convergence asserted for Joe in the Figure 2 discussion.
Appendix A.2.3: Galambos midpoint correction Papers.AnsariRockel2024.galambos_pickands_midpoint; Papers.AnsariRockel2024.galambos_pickands_midpoint_gt_half; Papers.AnsariRockel2024.galambos_printed_midpoint_counterexample; Papers.AnsariRockel2024.galambos_printed_midpoint_false verified The actual canonical midpoint is 1-2^(-1/delta)/2, strictly greater than 1/2 for every delta>0. At delta=1 it equals 3/4, while the literal arXiv v3 appendix expression 2^((1-delta)/delta) equals one. The universal printed equality is formally refuted. The intended lower-tail conclusion remains valid by the corrected midpoint and the independently checked tail limit. Journal correspondence for this expression remains unchecked.
BB5 construction support: logarithmic exponent Papers.AnsariRockel2024.bb5_exponent_formula; Papers.AnsariRockel2024.bb5_exponent_bounds; Papers.AnsariRockel2024.bb5_exponent_homogeneous; Papers.AnsariRockel2024.bb5_exponent_shape_one verified The analytic exponent agrees with the printed power expression. For theta>=1, delta>0 and positive coordinates it lies between max(x,y) and x+y and is homogeneous of degree one. At theta=1 it reduces to the Galambos exponent. The actual copula construction and CDF are checked below; canonical Pickands identification and several family properties are checked below.
BB5 construction support: exponent submodularity Papers.AnsariRockel2024.bb5_exponent_eq_power_log; Papers.AnsariRockel2024.bb5_exponent_submodular verified The printed BB5 exponent is identified with the Galambos stable-tail function after coordinate powers and a reciprocal power root. A general increasing-concave four-point lemma proves submodularity of this transformed exponent, for theta>=1, delta>0 and positive ordered coordinates. This supplies the logarithmic rectangle inequality without assuming a BB5 density. Nonnegative interior CDF rectangles are checked below; the full copula construction is checked below.
BB5 construction support: nonnegative interior CDF rectangles Papers.AnsariRockel2024.bb5_exponent_exp_rectangle; Papers.AnsariRockel2024.bb5_interior_rectangle_nonneg verified For theta>=1 and delta>0, every ordered rectangle strictly inside (0,1)^2 has a nonnegative increment under the printed BB5 CDF. A general exponential four-point inequality converts exponent monotonicity and submodularity to the CDF inequality; negative logarithms reverse both coordinate orders. The general power-transform result also includes zero logarithmic coordinates. Grounded boundaries, the full classical copula conditions and the actual copula constructor are checked below.
BB5 actual copula and closed-square CDF Papers.AnsariRockel2024.bb5_cdf_interior; Papers.AnsariRockel2024.bb5_cdf_full verified For theta>=1 and delta>0, an actual probability-measure copula has the printed interior CDF and correct grounded boundaries and uniform margins. A general power transformation of a bivariate extreme-value copula satisfies all classical copula conditions, including rectangles meeting the boundary. Max-stability, CI, canonical Pickands identification and tails are checked below; parameter orders and limits are checked below.
BB5 max-stability, conditional increase and Pickands function Papers.AnsariRockel2024.bb5_isExtremeValue; Papers.AnsariRockel2024.bb5_isCI; Papers.AnsariRockel2024.bb5_pickands_interior verified For every theta>=1 and delta>0, the actual BB5 copula is max-stable on the closed square and conditionally increasing in both directions. Its canonical Pickands function on (0,1) is the printed BB5 exponent at (1-t,t).
BB5 extremal coefficient and tails Papers.AnsariRockel2024.bb5_extremalCoefficient; Papers.AnsariRockel2024.bb5_tails verified The actual extremal coefficient is (2-2^(-1/delta))^(1/theta), strictly greater than one. The lower tail is zero and the upper tail is 2-(2-2^(-1/delta))^(1/theta), for every finite theta>=1 and delta>0.
BB5 parameter orders Papers.AnsariRockel2024.bb5_pickands_antitone; Papers.AnsariRockel2024.bb5_lowerOrthant_mono; Papers.AnsariRockel2024.bb5_schurBoth_mono verified For fixed theta>=1, increasing positive delta decreases the canonical Pickands function and increases the actual copula in lower-orthant and both directional Schur orders. The comparison transfers the proved Galambos CDF order through logarithms and the positive power root.
BB5 parameter limits Papers.AnsariRockel2024.bb5_limit_comonotonic; Papers.AnsariRockel2024.bb5_limit_gumbel_interior; Papers.AnsariRockel2024.bb5_limit_gumbel; Papers.AnsariRockel2024.bb5_limit_comonotonic_uniform; Papers.AnsariRockel2024.bb5_limit_gumbel_uniform verified For fixed theta>=1, the actual BB5 CDF tends uniformly on the closed square to Gumbel-Hougaard as positive delta tends to zero and to comonotonicity as delta tends to infinity. Arbitrary parameter nets are covered. The infinity limit follows from the power diagonal, and the zero limit from the vanishing Galambos kernel, with all boundary cases included.
BB5 shape-one special case Papers.AnsariRockel2024.bb5_shape_one verified At theta=1 the actual BB5 copula equals Galambos for every delta>0, including equality of the copula measures.
Huesler-Reiss construction support: normalized lognormal spectrum Papers.AnsariRockel2024.huslerReiss_spectral_isExtremeValue; Papers.AnsariRockel2024.huslerReiss_spectral_isCI; Papers.AnsariRockel2024.huslerReiss_pickands_spectral verified A normalized lognormal spectral expectation gives an actual copula for each delta>0, with max-stability, CI and its canonical Pickands expectation checked. General spectral-tail monotonicity, submodularity, margins and homogeneity yield all classical copula conditions. Identification with the printed Gaussian-CDF formula is checked below. The tails and both uniform endpoint limits are checked below; positive-parameter orders are checked below; the delta=0 extension is checked below; the starred density-TP2 claim is numerical-only and excluded (see the excluded row).
Huesler-Reiss actual interior CDF and canonical Pickands formula Papers.AnsariRockel2024.huslerReiss_pickands_interior; Papers.AnsariRockel2024.huslerReiss_cdf_interior verified For delta>0 the normalized lognormal spectral copula is identified with the printed Huesler-Reiss family: its canonical Pickands function is (1-t)Phi(1/delta+delta/2log((1-t)/t))+tPhi(1/delta+delta/2log(t/(1-t))). Gaussian exponential tilting and truncated lognormal integration evaluate the spectral maximum, yielding the actual interior CDF.
Huesler-Reiss extremal coefficient and tails Papers.AnsariRockel2024.huslerReiss_extremalCoefficient; Papers.AnsariRockel2024.huslerReiss_tails verified For every delta>0 the actual extremal coefficient is 2Phi(1/delta)>1, giving lower-tail coefficient zero and upper-tail coefficient 2-2Phi(1/delta).
Huesler-Reiss uniform endpoint limits Papers.AnsariRockel2024.huslerReiss_limit_comonotonic; Papers.AnsariRockel2024.huslerReiss_limit_independence_interior; Papers.AnsariRockel2024.huslerReiss_limit_independence; Papers.AnsariRockel2024.huslerReiss_limit_comonotonic_uniform; Papers.AnsariRockel2024.huslerReiss_limit_independence_uniform verified The actual CDF tends uniformly on the closed square to independence as positive delta tends to zero and to comonotonicity as delta tends to infinity. The zero limit uses the explicit Gaussian-CDF formula and includes every boundary; the infinity limit follows from the power diagonal and normal-CDF continuity.
Huesler-Reiss exact positive-parameter orders Papers.AnsariRockel2024.huslerReiss_pickands_antitone; Papers.AnsariRockel2024.huslerReiss_lowerOrthant_mono; Papers.AnsariRockel2024.huslerReiss_schurBoth_mono; Papers.AnsariRockel2024.huslerReiss_lowerOrthant_iff; Papers.AnsariRockel2024.huslerReiss_schurBoth_iff verified For positive parameters the actual copulas are ordered in lower-orthant order and both directional Schur orders exactly when delta<=epsilon. The Pickands function decreases by a checked derivative: the Gaussian density balance cancels the logarithmic terms. The converse follows from the upper-tail formula and strict normal-CDF monotonicity.
Huesler-Reiss full nonnegative-parameter family Papers.AnsariRockel2024.huslerReiss_zero; Papers.AnsariRockel2024.huslerReiss_positive; Papers.AnsariRockel2024.huslerReiss_closed_isExtremeValue; Papers.AnsariRockel2024.huslerReiss_closed_isCI; Papers.AnsariRockel2024.huslerReiss_closed_tails verified The actual family is extended to delta=0 by independence, with exact agreement with the spectral constructor for delta>0. Max-stability and CI hold throughout delta>=0. Both tails are zero at zero; the positive-parameter formulas above hold elsewhere.
Huesler-Reiss orders including independence Papers.AnsariRockel2024.huslerReiss_closed_lowerOrthant_mono; Papers.AnsariRockel2024.huslerReiss_closed_schurBoth_mono; Papers.AnsariRockel2024.huslerReiss_closed_lowerOrthant_iff; Papers.AnsariRockel2024.huslerReiss_closed_schurBoth_iff verified On the full nonnegative parameter range, lower-orthant and both directional Schur orders hold exactly when delta<=epsilon. The zero endpoint uses CI-implied quadrant dependence, while the converse excludes ordering a positive parameter below independence using its strictly positive upper-tail coefficient.
t-EV construction support: normalized Gaussian positive powers Papers.AnsariRockel2024.tEV_spectral_isExtremeValue; Papers.AnsariRockel2024.tEV_spectral_isCI; Papers.AnsariRockel2024.tEV_pickands_spectral verified Positive powers of the positive part of a standard Gaussian have finite, strictly positive moments. Normalized powers of correlated Gaussian coordinates therefore give an actual spectral copula for every nu>0 and correlation in [-1,1], with max-stability, CI and its canonical Pickands expectation checked. The printed Student-t form and the remaining t-EV family claims are verified in the t-EV rows below.
t-EV construction support: explicit spectral normalization Papers.AnsariRockel2024.tEV_gaussian_moment; Papers.AnsariRockel2024.tEV_gaussian_moment_add_two verified The normalizing positive Gaussian moment is evaluated as (sqrt(2*pi))^(-1)*2^((nu+1)/2)*Gamma((nu+1)/2)/2 for nu>0, and its increment-two recurrence is m(nu+2)=(nu+1)*m(nu). A square change of variables proves the general Gaussian power integral. These are normalization support results; the Student-t CDF identification is verified in the t-EV rows below.
Definition 2.3 and Lemma 2.4: rearrangement Schur order equals the convex-test order Papers.AnsariRockel2024.paperSchurLE_iff; Papers.AnsariRockel2024.paperSchurBothLE_iff; Papers.AnsariRockel2024.rearrSchurLE_congr; Papers.AnsariRockel2024.schur_endpoint_trivial verified The paper's order, defined through decreasing rearrangements of the conditional CDFs for 0<v<1, is equivalent to the library's convex-test SchurLE; the two-direction version matches SchurBothLE. Hardy–Littlewood–Pólya on [0,1] is proved for measurable [0,1]-valued functions. The order depends only on the a.e. class of the conditional CDFs, and the endpoint thresholds v∈{0,1} are trivial.
Lemma 2.7 (i)–(iv) and the formula for E↑: rearranged copulas Papers.AnsariRockel2024.rearranged_extremal; Papers.AnsariRockel2024.rearranged_mem; Papers.AnsariRockel2024.rearranged_unique_max; Papers.AnsariRockel2024.rearranged_unique_min; Papers.AnsariRockel2024.upRearr_cis; Papers.AnsariRockel2024.downRearr_formula; Papers.AnsariRockel2024.rearranged_schur_equiv; Papers.AnsariRockel2024.upRearr_formula verified For every copula E, the increasing and decreasing rearranged copulas E↑ and E↓ are actual copulas in the class {D : D ≤_∂S E}. They are its lower-orthant maximum and minimum, and each extremum is unique. E↑ is CIS, E↓(u,v)=v−E↑(1−u,v), E↑ and E↓ are Schur-equivalent to E, and E↑(u,v) is the integral over [0,u] of the decreasing rearrangement of ∂₁E(·,v).
Proposition 3.1: Schur order through rearranged copulas Papers.AnsariRockel2024.prop31 verified D ≤_∂S E ⇔ D↑ ≤_lo E↑ ⇔ E↓ ≤_lo D↓, for arbitrary bivariate copulas.
Proposition 3.3 (i)–(iii): Archimedean lower-orthant and Schur order Papers.AnsariRockel2024.archimedean_lowerOrthant_iff_generator; Papers.AnsariRockel2024.archimedean_lowerOrthant_iff_subadditive; Papers.AnsariRockel2024.LogConvexNegDeriv.isCI; Papers.AnsariRockel2024.LogConcaveNegDeriv.isCD; Papers.AnsariRockel2024.archimedean_schur_iff_subadditive_of_logconvex; Papers.AnsariRockel2024.archimedean_schur_iff_subadditive_of_logconcave verified (i) is proved in generator coordinates for arbitrary bivariate generators, and as subadditivity of φ₁∘ψ₂ on [0,∞) for strict generators (where the composition is defined everywhere). (ii) and (iii) take the paper's smooth hypothesis, log-convex or log-concave −ψ′, derive CI or CD, and characterize the two-direction Schur order (reversed in (iii)) by the same subadditivity.
Table 3: Clayton lower-orthant and Schur parameter orders; Table 2 limit θ→0⁻ Papers.AnsariRockel2024.clayton_signed_positive; Papers.AnsariRockel2024.clayton_signed_zero; Papers.AnsariRockel2024.clayton_signed_negative; Papers.AnsariRockel2024.clayton_lowerOrthant_mono; Papers.AnsariRockel2024.clayton_schur_nonnegative; Papers.AnsariRockel2024.clayton_schur_nonpositive; Papers.AnsariRockel2024.clayton_negative_tendsto_zero verified Verification.claytonSigned is the positive family for θ>0, Π at 0 and the truncated branch on [−1,0). The lower-orthant order increases on all of [−1,∞): convexity of x^r within the positive branch, the concave four-point inequality within the negative branch, and NQD/PQD across zero. Schur order increases on θ≥0 and decreases on −1≤θ≤0 (CI/CD plus Lemmas 2.6/2.8, applied in both directions). Negative parameters tending to 0 give Π pointwise on the square.
Table 3: Genest–Ghoudi (Nelsen 15) increasing lower-orthant order Papers.AnsariRockel2024.genestGhoudi_lowerOrthant_mono verified For all 1≤θ≤η, the actual copulas satisfy C_θ ≤_lo C_η on the whole closed square. The generator ratio φ_θ/φ_η is nondecreasing on (0,1): its logarithmic derivative compares z/(1−z) at two ordered powers of t. Also φ_η≤φ_θ. The classical ratio argument (Nelsen, Cor. 4.4.6) is carried out explicitly, including the zero region of the non-strict generator.
Table 3 (* cells): Nelsen 2, Nelsen 8 and Genest–Ghoudi are not Schur-ordered Papers.AnsariRockel2024.nelsen2_not_schur_monotone; Papers.AnsariRockel2024.nelsen2_not_schur_antitone; Papers.AnsariRockel2024.nelsen8_not_schur_monotone; Papers.AnsariRockel2024.nelsen8_not_schur_antitone; Papers.AnsariRockel2024.nelsen8_five_quarter_energy; Papers.AnsariRockel2024.genestGhoudi_not_schur_monotone; Papers.AnsariRockel2024.genestGhoudi_not_schur_antitone verified Neither increasing nor decreasing directional Schur order holds on the parameter range; for these Archimedean families the directional and two-direction orders agree. Nelsen 2 and Genest–Ghoudi start at W and tend to M. A member with median conditional energy below 1/2 excludes both directions, using W's energy 1/2 and the median-strip energy inequality near M. Nelsen 8 uses the exact energy 279/3600 at θ=5, threshold 1/4, and its Clayton(1) limit. The unordered cell is read as failure of both monotonicities; no incomparable pair is asserted.
Table 3 (* cell): Nelsen 18 is not Schur-ordered Papers.AnsariRockel2024.nelsen18_not_schur_antitone; Papers.AnsariRockel2024.nelsen18_two_not_schurLE_four; Papers.AnsariRockel2024.nelsen18_not_schur_monotone verified Not decreasing: the θ=2 member has median energy below 1/2 and the family tends to M. Not increasing: C₂ ≰_∂S C₄. At threshold 1/9, the θ=4 conditional CDF is at most 5/8 almost everywhere, because on the positive region it equals p(1+(−log p)/(−L))² ≤ (2/5)(1+log(5/2)/4)² ≤ 5/8. The θ=2 conditional CDF exceeds 5/8 near x*=1+2/(−9/4−log 4). The convex test z↦(z−5/8)₊ separates them. All constants are proved from exponential/Taylor bounds.
Table 5 / Appendix A.4.2 (* cell): Mardia Schur order; Fréchet on unmixed axes Papers.AnsariRockel2024.mardia_schur_nonnegative; Papers.AnsariRockel2024.mardia_schur_nonpositive; Papers.AnsariRockel2024.frechet_schur_mono_M; Papers.AnsariRockel2024.frechet_schur_mono_W verified Mardia increases in two-direction Schur order on 0≤θ≤1 and decreases on −1≤θ≤0 (i.e. it is Schur-monotone in
Table 5 (* cells): density-TP2 exclusions for Joe-EV, Tawn and t-EV, at explicit members Papers.AnsariRockel2024.joeExtremeValue_witness_not_mtp2; Papers.AnsariRockel2024.tawn_witness_not_mtp2; Papers.AnsariRockel2024.tEV_witness_not_mtp2 verified Joe-EV with δ=1, α=β=1/2; Tawn with θ=2, α=β=1/2; and t-EV with ν=1, ρ=0 have no TP2 (MTP2) Lebesgue density. An MTP2 density forces the ordered-rectangle inequality μ(S×V)μ(T×U) ≤ μ(S×U)μ(T×V). Explicit rectangles on powers of t=99/100, with closed-form CDF values, violate it; the Tawn and t-EV witnesses use the Pythagorean double pairs (91,60), (91,312), (25,60), (25,312). The t-EV member uses T₂(z)=1/2+z/(2√(2+z²)). These rows verify the exclusion at these members only. The unit-weight Tawn members (Gumbel) do have TP2 densities (row above), and Joe-EV's unit-weight member is Galambos, whose density-TP2 status the paper leaves open (?).
Tables 1, 4, 5: t-EV family (printed Student-t form, CI, tails, orders, endpoints) Papers.AnsariRockel2024.tEV_student_cdf_eq; Papers.AnsariRockel2024.tEV_arg_def; Papers.AnsariRockel2024.tEV_pickands; Papers.AnsariRockel2024.tEV_cdf_interior; Papers.AnsariRockel2024.tEV_isCI; Papers.AnsariRockel2024.tEV_extremalCoefficient; Papers.AnsariRockel2024.tEV_tails; Papers.AnsariRockel2024.tEV_lowerTail; Papers.AnsariRockel2024.tEV_one; Papers.AnsariRockel2024.tEV_negative_one; Papers.AnsariRockel2024.tEV_lowerOrthant_mono; Papers.AnsariRockel2024.tEV_schurBoth_mono; Papers.AnsariRockel2024.tEV_lowerOrthant_iff; Papers.AnsariRockel2024.tEV_schurBoth_iff; Papers.AnsariRockel2024.tEV_closed_lowerOrthant_mono; Papers.AnsariRockel2024.tEV_closed_schurBoth_mono verified The constructed t-EV copula has the printed Pickands function A(t)=(1−t)T_{ν+1}(z((1−t)/t))+tT_{ν+1}(z(t/(1−t))), where z(w)=√((1+ν)/(1−ρ²))(w^{1/ν}−ρ) and T_{ν+1} is the Student-t CDF (proved equal to the gamma-mixture CDF). It is CI. The tails are (0, 2(1−T_{ν+1}(√((ν+1)(1−ρ)/(1+ρ))))). Lower-orthant and two-direction Schur order hold exactly when ρ≤ρ′ on (−1,1), and increase on the closed interval. ρ=1 gives M and ρ=−1 gives Π.
Table 4: t-EV parameter limits and audit of the printed ν→∞ entry Papers.AnsariRockel2024.tEV_limit_infinity; Papers.AnsariRockel2024.tEV_limit_zero; Papers.AnsariRockel2024.tEV_zero_weight; Papers.AnsariRockel2024.tEV_zero_weight_pos; Papers.AnsariRockel2024.tEV_zero_limit_ne_independence; Papers.AnsariRockel2024.huslerReiss_ne_independence; Papers.AnsariRockel2024.tEV_printed_infinity_limit_false verified For fixed ρ∈(−1,1), the limit ν→∞ gives Π pointwise. The limit ν→0 gives Marshall–Olkin(α,α) with α=1/2+arcsin(ρ)/π∈(0,1), which is not Π. The printed Hüsler–Reiss limit for ν→∞ at fixed ρ is refuted, since every Hüsler–Reiss member with δ>0 differs from Π.
Table 1: Laplace density in printed Bessel form Papers.AnsariRockel2024.laplace_radial_eq_besselK0 verified With K₀(z)=∫₀^∞e^{−z cosh s}ds, the verified radial mixture integral equals 2K₀(√(2q)) for q>0 (substitution t=√(q/2)eˢ). Combined with laplace_joint_radial_density, the joint density is K₀(√(2Q))/(π√(1−r²)) for Q>0, as printed.
Table 6: Student-t and Laplace Spearman rho in Heinen–Valdesogo form Papers.AnsariRockel2024.hv_integrand; Papers.AnsariRockel2024.student_spearmanRho_hv; Papers.AnsariRockel2024.laplace_spearmanRho_hv verified ρ=(6/π)E[arcsin(rṼ)], where Ṽ=W₃/√((W₁+W₃)(W₂+W₃)) is built from independent mixing variances. These are inverse-gamma(ν/2,ν/2) variances for Student-t and exponential(1) for Laplace, matching Heinen–Valdesogo (2020), Proposition 1. This closes the correspondence left open in the scale-expectation row.
Table 1/4: Cuadras–Augé CDF and endpoints; Marshall–Olkin endpoint; TP2 ⇒ CI Papers.AnsariRockel2024.cuadrasAuge_cdf; Papers.AnsariRockel2024.cuadrasAuge_one; Papers.AnsariRockel2024.cuadrasAuge_zero; Papers.AnsariRockel2024.marshallOlkin_one_one_eq; Papers.AnsariRockel2024.marshallOlkin_diag; Papers.AnsariRockel2024.mtp2_density_isCI verified Cuadras–Augé CDF min(u,v)·max(u,v)^{1−δ} on the closed square; δ=1 is M and δ=0 is Π; Marshall–Olkin with α=β=1 is M and equal weights give Cuadras–Augé; an MTP2 Lebesgue density implies CI in both directions (Section 2 implication chain).
Numerical-only (*) observations not formalized — excluded Hüsler–Reiss density TP2 (yes*) and the density-TP2 exclusions of Joe-EV, Tawn and t-EV at parameters other than the witnesses above are numerical observations in the source; they are not proved here. For Tawn and t-EV, a local expansion near the u=1 edge suggests the exclusion holds for all weights α<1 (resp. all non-Gumbel members), but no proof is formalized. Hüsler–Reiss TP2 reduces to a delicate asymptotic balance; it is neither proved nor refuted. Incomparable pairs for the unordered Schur cells are not asserted; the verified rows show that neither monotonicity holds.
Journal/preprint correspondence — excluded The verified scope is pinned to arXiv v3, whose numbering all rows use. The publisher PDF was compared statement by statement for the rows listed in SOURCE_COMPARISON.md (including the Fréchet/Mardia, Plackett and Raftery discrepancies, numbering of Lemmas 2.4–2.10 and Propositions 3.1–3.3, and the starred Table 3/5 cells). A cell-by-cell certification of the publisher layout is not part of the formal claims.

Proof sources: ClaytonDensityDerivative.lean, Definitions.lean, Association.lean, and Dependence.lean.

Source discrepancies and exclusions

The Fréchet simplex and Mardia W-weight above follow the valid copula mixtures. The reversed simplex inequality and negative W-weight printed in Appendix A.4.1 / equation (23) are not asserted as theorems. Table 6's coefficient formulas are checked with the valid family definitions. The corrected Frechet lower orthant order and an explicit counterexample to the printed increasing-in-W-weight direction are also mapped above.

Appendix A.5.1 of the arXiv v3 source prints a Nelsen 7 xi intermediate integral with the positive-part CDF where the squared conditional CDF step is needed. The Lean proof evaluates the printed expression as -1-theta/4 on the entire parameter interval, while actual xi is 1-theta. At the interior parameter theta=1/2, the values are -9/8 and 1/2 respectively. The final Table 6 xi=1-theta claim is verified independently; the false intermediate equality is not. This discrepancy is assigned to arXiv v3 only; we have not established whether the published journal version retains it.

The Mardia CI/CD classifications include independence at theta=0, which is omitted in the printed endpoint classifications. Density TP2 here means existence of a TP2 density with respect to square Lebesgue measure, as in the source's density definition. Both families have such a density exactly at independence: every nonzero M or W weight puts positive mass on a Lebesgue-null diagonal. Thus the printed TP2 claims at singular endpoints are corrected, not asserted. This does not classify alternative notions of total positivity for singular measures or for the CDF.

Other discrepancies documented in the pinned library's coverage audit remain outside this verified subset. Numerical plots, grid searches, and numerical-only table observations are excluded from the formal claims.

Additional proof modules: FamilyExtensions.lean, TailsAndOrders.lean, and FrechetMardiaDependence.lean. Shared measure and dependence proofs are in Verification/FrechetDependence.lean.

Nelsen7Results.lean maps the new pinned-library results. The Frechet/Mardia proof modules now delegate to the upstream package; their existing public declarations and audits are preserved.

Source-scope note: Table 5 explicitly marks BB5/Galambos density TP2, Student-t/Laplace Schur order, and both Laplace tail coefficients with question marks. These cells state no result to translate; deriving new classifications there is not a completion requirement. Starred numerical claims (including Joe-EV density TP2) are different: their claim status and formal verification still need an explicit audit. A green build does not resolve those claims or the remaining named family constructors.

Inspect the formalization

DefinitionsGenerated Lean documentation →MainGenerated Lean documentation →AxiomsGenerated Lean documentation →

Reproduce this snapshot

Run the full project build to check every source file. The pinned toolchain and dependencies live at the repository root.

git clone https://github.com/Corrram/lean-verifications.git
cd lean-verifications
git checkout --detach 0ac8668a9c4c9007ec374694abc14296edbeae75
lake exe cache get
lake build

Cite this supplement

Use the permanent folder at commit 0ac8668 to identify the exact software snapshot. Cite the original article separately. This handbook follows the latest deployed commit.

Article bibliography (BibTeX)
@article{AnsariRockel2024,
  author  = {Ansari, Jonathan and Rockel, Marcus},
  title   = {Dependence properties of bivariate copula families},
  journal = {Dependence Modeling},
  year    = {2024},
  volume  = {12},
  number  = {1},
  doi     = {10.1515/demo-2024-0002},
  url     = {https://doi.org/10.1515/demo-2024-0002}
}

@misc{AnsariRockelArxivV3,
  author        = {Ansari, Jonathan and Rockel, Marcus},
  title         = {Dependence properties of bivariate copula families},
  year          = {2024},
  eprint        = {2310.17307},
  archivePrefix = {arXiv},
  primaryClass  = {math.ST},
  note          = {Version 3, 6 April 2024},
  url           = {https://arxiv.org/abs/2310.17307v3}
}

% Cite the Lean supplement separately using its folder and full commit permalink.