← Copula mathematical handbook

Diagonal sections of bivariate Archimedean copulas

For C(u, v) = ψ(φ(u) + φ(v)) the diagonal section is δ(t) = ψ(2 φ(t)) (Nelsen, An Introduction to Copulas, second edition, Section 4.1 and Table 4.1). Since C(t, t) < t on (0, 1), no bivariate Archimedean copula is the upper Fréchet bound M.

theorem ProbabilityTheory.Copula.BivariateGenerator.diagonal_eq_cdf (g : BivariateGenerator) (t : ↑unitInterval) : g.copula.diagonal t = g.cdf t t

The diagonal of the copula of a generator is its cdf on the diagonal.

theorem ProbabilityTheory.Copula.BivariateGenerator.diagonal_copula (g : BivariateGenerator) {t : ↑unitInterval} (ht : t ≠ 0) : g.copula.diagonal t = g.toFun (2 * g.invFun t)

The diagonal section formula δ(t) = ψ(2 φ(t)) for t > 0.

theorem ProbabilityTheory.Copula.BivariateGenerator.diagonal_lt (g : BivariateGenerator) {t : ↑unitInterval} (h0 : t ≠ 0) (h1 : t ≠ 1) : g.copula.diagonal t < ↑t

δ(t) < t on the open unit interval.

theorem ProbabilityTheory.Copula.IsArchimedean.diagonal_lt {C : Copula 2} (hC : C.IsArchimedean) {t : ↑unitInterval} (h0 : t ≠ 0) (h1 : t ≠ 1) : C.diagonal t < ↑t

The diagonal of a bivariate Archimedean copula lies strictly below the identity on (0, 1).

theorem ProbabilityTheory.Copula.IsArchimedean.ne_comonotonic {C : Copula 2} (hC : C.IsArchimedean) : C ≠ comonotonic 2

No bivariate Archimedean copula is the upper Fréchet bound.