Repository navigation
Initial development release of copula, a Lean 4 library for finite-dimensional copulas built on mathlib.
- Measure-based copulas, classical CDFs, and Sklar's theorem.
- Copula families, dependence orders, positive dependence, rank correlations, and tail dependence.
- Binary ordinal sums with probability laws, rank formulas, and constructive converse decomposition.
- 392 public Lean examples, checked with warnings treated as errors.
Requires Lean and mathlib v4.34.0. The API is still under development; the README and coverage documentation distinguish proved results from remaining work.
Add this to lakefile.toml:
[[require]]
name = "copula"
git = "https://github.com/Corrram/copula.git"
rev = "v0.1.0"Run lake update, commit the resulting dependency manifest, and use import Copula or a focused module such as import Copula.Basic.
Reservoir metadata is included. Reservoir discovers repositories automatically, subject to its inclusion criteria; the Git dependency above works independently of indexing.
License: Apache-2.0.