← Copula mathematical handbook

Uniqueness of Archimedean generators up to a positive factor

Nelsen, An Introduction to Copulas, second edition, Theorem 4.1.5 (3) shows that the generators φ and c φ (c > 0) produce the same Archimedean copula. Conversely, the generator of a bivariate Archimedean copula is unique up to such a factor (Genest and MacKay, 1986; Nelsen, Section 4.1, the remark after Theorem 4.1.5):

• BivariateGenerator.copula_eq_iff: C_{φ₁} = C_{φ₂} iff φ₂ = c φ₁ on (0, 1] for some c > 0;
• BivariateGenerator.toFun_mul_eq_of_invFun_eq_mul: in that case the inverse generators satisfy ψ₂(c s) = ψ₁(s) for all s ≥ 0, including the zero set of a non-strict generator;
• HasArchimedeanGenerator.invFun_eq_mul: two generators identified for the same bivariate copula differ by a positive factor.

The proof of the converse follows Genest–MacKay: h = φ₂ ∘ ψ₁ satisfies Cauchy's equation h(x + y) = h(x) + h(y) wherever ψ₁(x + y) > 0 (because φ₂(C(u, v)) = φ₂(u) + φ₂(v) when C(u, v) > 0), and it is monotone, so it is linear (additive_monotone_ratio_le, a self-contained version of the monotone Cauchy equation on a down-closed subset of [0, ∞)).

theorem ProbabilityTheory.Copula.BivariateGenerator.additive_monotone_ratio_le {P : ℝ → Prop} {h : ℝ → ℝ} (hdown : ∀ (s t : ℝ), P t → 0 ≤ s → s ≤ t → P s) (hadd : ∀ (x y : ℝ), 0 ≤ x → 0 ≤ y → P (x + y) → h (x + y) = h x + h y) (hmono : ∀ (s t : ℝ), P t → 0 ≤ s → s ≤ t → h s ≤ h t) {s t : ℝ} (hs : P s) (ht : P t) (hs0 : 0 < s) (ht0 : 0 < t) : h t * s ≤ h s * t

Monotone solutions of Cauchy's equation on a down-closed subset P of [0, ∞) are linear: for s, t ∈ P with s, t > 0 one has h(t) s ≤ h(s) t (hence h(s)/s = h(t)/t by symmetry).

theorem ProbabilityTheory.Copula.BivariateGenerator.toFun_mul_eq_of_invFun_eq_mul (g₁ g₂ : BivariateGenerator) {c : ℝ} (hc : 0 < c) (h : ∀ (u : ↑unitInterval), u ≠ 0 → g₂.invFun u = c * g₁.invFun u) {s : ℝ} (hs : 0 ≤ s) : g₂.toFun (c * s) = g₁.toFun s

If φ₂ = c φ₁ on (0, 1], then ψ₂(c s) = ψ₁(s) for every s ≥ 0.

theorem ProbabilityTheory.Copula.BivariateGenerator.copula_eq_of_invFun_eq_mul (g₁ g₂ : BivariateGenerator) {c : ℝ} (hc : 0 < c) (h : ∀ (u : ↑unitInterval), u ≠ 0 → g₂.invFun u = c * g₁.invFun u) : g₁.copula = g₂.copula

Nelsen, Theorem 4.1.5 (3) in pointwise form: generators proportional on (0, 1] give the same Archimedean copula.

theorem ProbabilityTheory.Copula.BivariateGenerator.exists_invFun_eq_mul_of_copula_eq (g₁ g₂ : BivariateGenerator) (hC : g₁.copula = g₂.copula) : ∃ (c : ℝ), 0 < c ∧ ∀ (u : ↑unitInterval), u ≠ 0 → g₂.invFun u = c * g₁.invFun u

Genest–MacKay: the generator of a bivariate Archimedean copula is unique up to a positive factor. If C_{φ₁} = C_{φ₂} then φ₂ = c φ₁ on (0, 1] for some c > 0.

theorem ProbabilityTheory.Copula.BivariateGenerator.copula_eq_iff (g₁ g₂ : BivariateGenerator) : g₁.copula = g₂.copula ↔ ∃ (c : ℝ), 0 < c ∧ ∀ (u : ↑unitInterval), u ≠ 0 → g₂.invFun u = c * g₁.invFun u

Genest–MacKay uniqueness theorem (Nelsen, Section 4.1): two bivariate generators give the same Archimedean copula iff φ₂ = c φ₁ on (0, 1] for some constant c > 0.

theorem ProbabilityTheory.Copula.BivariateGenerator.copula_eq_iff_toFun (g₁ g₂ : BivariateGenerator) : g₁.copula = g₂.copula ↔ ∃ (c : ℝ), 0 < c ∧ ∀ (s : ℝ), 0 ≤ s → g₂.toFun (c * s) = g₁.toFun s

Uniqueness in terms of inverse generators: C_{ψ₁} = C_{ψ₂} iff ψ₂(s) = ψ₁(s / c) for all s ≥ 0 and some c > 0.

theorem ProbabilityTheory.Copula.BivariateGenerator.copula_eq_iff_scale (g₁ g₂ : BivariateGenerator) : g₁.copula = g₂.copula ↔ ∃ (c : ℝ) (hc : 0 < c), ∀ (u : ↑unitInterval), u ≠ 0 → g₂.invFun u = (g₁.scale c hc).invFun u

Two generators give the same copula iff one is a positive rescaling of the other (BivariateGenerator.scale) on (0, 1].

theorem ProbabilityTheory.Copula.HasArchimedeanGenerator.invFun_eq_mul {C : Copula 2} {g₁ g₂ : BivariateGenerator} (h₁ : C.HasArchimedeanGenerator g₁) (h₂ : C.HasArchimedeanGenerator g₂) : ∃ (c : ℝ), 0 < c ∧ ∀ (u : ↑unitInterval), u ≠ 0 → g₂.invFun u = c * g₁.invFun u

Two generators identified for the same bivariate copula differ by a positive factor.