← Mathematical handbook

Lower-orthant comparison of bivariate Archimedean copulas

For strict bivariate generators ψ₁, ψ₂ (inverse generators, ψ(0)=1, positive on [0,∞)), C_{ψ₁} ≤_lo C_{ψ₂} holds iff φ₁ ∘ ψ₂ is subadditive on [0,∞), where φ₁=ψ₁⁻¹. This is Proposition 3.3(i) of Ansari–Rockel (Nelsen, Theorem 4.4.2).

theorem ProbabilityTheory.Copula.BivariateGenerator.toFun_zero (g : BivariateGenerator) : g.toFun 0 = 1

theorem ProbabilityTheory.Copula.BivariateGenerator.toFun_le_one (g : BivariateGenerator) {x : ℝ} (hx : 0 ≤ x) : g.toFun x ≤ 1

theorem ProbabilityTheory.Copula.BivariateGenerator.strictAntiOn_of_pos (g : BivariateGenerator) (hpos : ∀ (x : ℝ), 0 ≤ x → 0 < g.toFun x) : StrictAntiOn g.toFun (Set.Ici 0)

A strict generator is strictly decreasing on [0,∞): a flat piece would force a positive lower bound, contradicting surjectivity onto (0,1].

theorem ProbabilityTheory.Copula.BivariateGenerator.invFun_toFun (g : BivariateGenerator) (hpos : ∀ (x : ℝ), 0 ≤ x → 0 < g.toFun x) {x : ℝ} (hx : 0 ≤ x) : g.invFun (Set.projIcc 0 1 ⋯ (g.toFun x)) = x

noncomputable def ProbabilityTheory.Copula.BivariateGenerator.compose (g₁ g₂ : BivariateGenerator) (x : ℝ) : ℝ

The composition φ₁ ∘ ψ₂ of Proposition 3.3.

Equations

• g₁.compose g₂ x = g₁.invFun (Set.projIcc 0 1 ProbabilityTheory.Copula.BivariateGenerator.compose._proof_1 (g₂.toFun x))

theorem ProbabilityTheory.Copula.BivariateGenerator.lowerOrthantLE_iff_cdf (g₁ g₂ : BivariateGenerator) : g₁.copula.LowerOrthantLE g₂.copula ↔ ∀ (u v : ↑unitInterval), g₁.cdf u v ≤ g₂.cdf u v

theorem ProbabilityTheory.Copula.BivariateGenerator.lowerOrthantLE_iff_subadditive (g₁ g₂ : 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), strict generators: lower-orthant order iff subadditivity of φ₁ ∘ ψ₂ on [0,∞).

theorem ProbabilityTheory.Copula.BivariateGenerator.lowerOrthantLE_iff_generator (g₁ g₂ : 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), general form: lower-orthant order in generator coordinates.