← Mathematical handbook

Proposition 3.3: ordering Archimedean copulas

Generators are inverse generators ψ in the library convention (C=ψ(ψ⁻¹u+ψ⁻¹v)). Part (i) is proved for strict generators, where ψ₁⁻¹ ∘ ψ₂ is defined on all of [0,∞), and in generator coordinates for arbitrary bivariate generators. Parts (ii) and (iii) use the smooth log-convexity/log-concavity hypotheses of the paper to obtain CI/CD, and then Lemmas 2.6 and 2.8.

def Papers.AnsariRockel2024.LogConvexNegDeriv (g : ProbabilityTheory.Copula.BivariateGenerator) : Prop

Smooth strict inverse generator with log-convex -ψ' (hypothesis of Prop. 3.3(ii)).

Equations

• One or more equations did not get rendered due to their size.

def Papers.AnsariRockel2024.LogConcaveNegDeriv (g : ProbabilityTheory.Copula.BivariateGenerator) : Prop

Smooth strict inverse generator with log-concave -ψ' (hypothesis of Prop. 3.3(iii)).

Equations

• One or more equations did not get rendered due to their size.

theorem Papers.AnsariRockel2024.LogConvexNegDeriv.isCI {g : ProbabilityTheory.Copula.BivariateGenerator} (h : LogConvexNegDeriv g) : g.copula.IsCI

theorem Papers.AnsariRockel2024.LogConcaveNegDeriv.isCD {g : ProbabilityTheory.Copula.BivariateGenerator} (h : LogConcaveNegDeriv g) : g.copula.IsCD

theorem Papers.AnsariRockel2024.archimedean_lowerOrthant_iff_generator (g₁ g₂ : ProbabilityTheory.Copula.BivariateGenerator) : g₁.copula.LowerOrthantLE g₂.copula ↔ ∀ (u v : ↑unitInterval), u ≠ 0 → v ≠ 0 → g₁.toFun (g₁.invFun u + g₁.invFun v) ≤ g₂.toFun (g₂.invFun u + g₂.invFun v)

Proposition 3.3(i), generator coordinates, for arbitrary bivariate generators.

theorem Papers.AnsariRockel2024.archimedean_lowerOrthant_iff_subadditive (g₁ g₂ : ProbabilityTheory.Copula.BivariateGenerator) (h₁ : ∀ (x : ℝ), 0 ≤ x → 0 < g₁.toFun x) (h₂ : ∀ (x : ℝ), 0 ≤ x → 0 < g₂.toFun x) : g₁.copula.LowerOrthantLE g₂.copula ↔ ∀ (x y : ℝ), 0 ≤ x → 0 ≤ y → g₁.compose g₂ (x + y) ≤ g₁.compose g₂ x + g₁.compose g₂ y

Proposition 3.3(i): for strict generators, C₁ ≤_lo C₂ iff ψ₁⁻¹∘ψ₂ is subadditive.

theorem Papers.AnsariRockel2024.archimedean_schur_iff_subadditive_of_logconvex (g₁ g₂ : ProbabilityTheory.Copula.BivariateGenerator) (h₁ : ∀ (x : ℝ), 0 ≤ x → 0 < g₁.toFun x) (h₂ : ∀ (x : ℝ), 0 ≤ x → 0 < g₂.toFun x) (hc₁ : LogConvexNegDeriv g₁) (hc₂ : LogConvexNegDeriv g₂) : g₁.copula.SchurBothLE g₂.copula ↔ ∀ (x y : ℝ), 0 ≤ x → 0 ≤ y → g₁.compose g₂ (x + y) ≤ g₁.compose g₂ x + g₁.compose g₂ y

Proposition 3.3(ii): with log-convex -ψᵢ', subadditivity characterizes the two-direction Schur order C₁ ≤_∂S C₂.

theorem Papers.AnsariRockel2024.archimedean_schur_iff_subadditive_of_logconcave (g₁ g₂ : ProbabilityTheory.Copula.BivariateGenerator) (h₁ : ∀ (x : ℝ), 0 ≤ x → 0 < g₁.toFun x) (h₂ : ∀ (x : ℝ), 0 ≤ x → 0 < g₂.toFun x) (hc₁ : LogConcaveNegDeriv g₁) (hc₂ : LogConcaveNegDeriv g₂) : g₂.copula.SchurBothLE g₁.copula ↔ ∀ (x y : ℝ), 0 ≤ x → 0 ≤ y → g₁.compose g₂ (x + y) ≤ g₁.compose g₂ x + g₁.compose g₂ y

Proposition 3.3(iii): with log-concave -ψᵢ', subadditivity characterizes the reversed two-direction Schur order C₂ ≤_∂S C₁.