Featured theorem index¶
These are the definitions and theorems linked from the mathematical handbook. Each formal-statement link opens the generated API; each source link opens the declaration and its proof at this site's library revision.
For the full declaration catalogue, including supporting lemmas, use the Lean API browser.
A copula as a probability measure¶
The copula distribution function¶
Fréchet–Hoeffding lower bound¶
Fréchet–Hoeffding upper bound¶
Lipschitz regularity¶
Recovering a classical copula CDF¶
Sklar existence with arbitrary marginals¶
Uniqueness on marginal CDF ranges¶
Sklar uniqueness with continuous marginals¶
The independence copula¶
The comonotonic copula¶
The countermonotonic copula¶
The Farlie–Gumbel–Morgenstern family¶
Spearman's rho of FGM¶
Kendall's tau of FGM¶
Stochastic increasingness of FGM¶
The positive-parameter Clayton CDF¶
Joe lower-tail coefficient for every parameter¶
Joe upper-tail coefficient for every parameter¶
The Nelsen 8 CDF on the closed square¶
Nelsen 8 is never positive quadrant dependent¶
Nelsen 8 is never conditionally increasing¶
Nelsen 8 never has a TP2 CDF¶
Nelsen 8 never has an MTP2 density¶
Nelsen 8 is conditionally decreasing exactly at one¶
Nelsen 8 at one is conditionally decreasing¶
Nelsen 8 increases in lower-orthant order¶
Nelsen 8 lower-tail coefficient for every parameter¶
Nelsen 8 upper-tail coefficient for every parameter¶
Nelsen 8 tends pointwise to Clayton at one¶
Nelsen 8 lower-Fréchet endpoint¶
Nelsen 2 tends pointwise to comonotonicity¶
Nelsen 2 increases in lower-orthant order¶
Nelsen 2 is conditionally decreasing exactly at one¶
Nelsen 2 is never positive quadrant dependent¶
Nelsen 2 is never conditionally increasing¶
Nelsen 2 never has a TP2 CDF¶
Nelsen 2 never has an MTP2 density¶
The Nelsen 2 CDF on the closed square¶
Nelsen 2 lower-tail coefficient for every parameter¶
Nelsen 2 upper-tail coefficient for every parameter¶
Nelsen 12 lower-tail dependence coefficient¶
Nelsen 12 upper-tail dependence coefficient¶
Nelsen 12 increases in lower-orthant order¶
Nelsen 12 tends pointwise to comonotonicity¶
The Nelsen 12 CDF on the closed square¶
Nelsen 14 lower-tail dependence coefficient¶
Nelsen 14 upper-tail dependence coefficient¶
Nelsen 14 tends pointwise to comonotonicity¶
Genest–Ghoudi tends pointwise to comonotonicity¶
The Nelsen 14 CDF on the closed square¶
Genest–Ghoudi is never positively quadrant dependent¶
Genest–Ghoudi is never conditionally increasing¶
Genest–Ghoudi CDF is never TP2¶
Genest–Ghoudi never has an MTP2 Lebesgue density¶
Genest–Ghoudi is CD exactly at parameter one¶
Genest–Ghoudi lower-tail dependence coefficient¶
Genest–Ghoudi upper-tail dependence coefficient¶
The Genest–Ghoudi CDF on the closed square¶
The positive-parameter Frank CDF on the closed square¶
The negative-parameter Frank CDF on the closed square¶
The printed negative-parameter Frank CDF on the closed square¶
The BB1 CDF on the closed square¶
The BB6 CDF on the closed square¶
Joe tends pointwise to comonotonicity¶
The Joe CDF on the closed square¶
The Gumbel–Hougaard CDF¶
Gumbel–Hougaard increases in lower-orthant order¶
Gumbel–Hougaard tends pointwise to comonotonicity¶
The Gumbel–Hougaard CDF on the closed square¶
The Tawn CDF on the closed square¶
Gumbel is an extreme-value copula¶
Spearman's rho¶
Kendall's tau¶
Spearman's footrule¶
Gini's gamma¶
Blomqvist's beta¶
Chatterjee's xi detects independence¶
Maximal rho characterizes comonotonicity¶
Minimal rho characterizes countermonotonicity¶
Maximal tau characterizes comonotonicity¶
Strict rho monotonicity among comparable copulas¶
Zero rho within the PQD class¶
Bivariate concordance and lower orthant order¶
Independence is least in Schur order¶
Schur order preserves Chatterjee's xi¶
SI implies LTD¶
SI implies RTI¶
LTD implies PQD¶
RTI implies PQD¶
Unique components at a fixed ordinal-sum split¶
Reconstruction from the two components¶
Threshold disagreement and the diagonal deficit¶
Kendall's tau of an ordinal sum¶
Spearman's rho of an ordinal sum¶
Footrule of an ordinal sum¶
Maximal beta as an equal-split ordinal sum¶
Formal statementSource and proof
ProbabilityTheory.Copula.blomqvistBeta_eq_one_iff_existsUnique_ordinalSumMaximal beta forces rho at least one half¶
Formal statementSource and proof
ProbabilityTheory.Copula.half_le_spearmanRho_of_blomqvistBeta_eq_oneMaximal beta forces nonnegative tau¶
NQD excludes a nontrivial ordinal sum¶
C-vine root-pair marginals¶
Recursive C-vine distribution function¶
Independent pair copulas give an independent vine¶
Regular-vine path attachment satisfies proximity¶
Conditional gluing preserves the left marginal¶
Unconditional gluing recovers its pair copula¶
Conditional gluing preserves the right marginal¶
Conditioning-dependent vine event probabilities¶
Vine extension preserves the previous joint law¶
Nelsen 7 xi on the full parameter interval¶
Nelsen 7 Spearman rho, including endpoints¶
Nelsen 7 Kendall tau, including endpoints¶
Exact Nelsen 7 Schur order in both directions¶
Exact Frechet CI classification¶
Exact Frechet density TP2 classification¶
Exact Mardia CI classification¶
Exact Mardia density TP2 classification¶
Minimum of xi plus footrule over Frechet copulas¶
Unique Frechet minimizer of xi plus footrule¶
Any local filling interpolates the source copula at grid vertices¶
Uniform error bound for sampled grid copulas¶
Positive-degree Bernstein polynomials satisfy the copula axioms¶
Bernstein copulas converge uniformly¶
Countable ordinal sums have summable weighted CDF series¶
Straight shuffles of M are dense for the uniform metric¶
Grid shuffles agree with the copula at every grid vertex¶
General ordinal sums on the component squares¶
Ordinal sums are characterized by diagonal fixed points¶
Library revision: fe53ea2f · Lean 4.34.0