← Copula mathematical handbook

Quadrant dependence from strict log-convexity of the inverse generator

If log ψ is strictly convex on [0, ∞) for the inverse generator ψ of an Archimedean copula (with ψ > 0), then ψ(0) = 1 gives the strict superadditivity ψ(x) ψ(y) < ψ(x + y) for x, y > 0. By the criteria of Copula.Archimedean.QuadrantCriteria the copula is then PQD but not NQD. Strict log-concavity gives the opposite (NQD but not PQD). Strict (log-)convexity is checked from the second derivative: ψ ψ'' > (ψ')² (resp. <) on (0, ∞).

theorem ProbabilityTheory.Copula.strictConvexOn_log_of_derivs {ψ ψ1 ψ2 : ℝ → ℝ} (hpos : ∀ (t : ℝ), 0 ≤ t → 0 < ψ t) (hcont : ContinuousOn ψ (Set.Ici 0)) (h1 : ∀ (t : ℝ), 0 < t → HasDerivAt ψ (ψ1 t) t) (h2 : ∀ (t : ℝ), 0 < t → HasDerivAt ψ1 (ψ2 t) t) (h : ∀ (t : ℝ), 0 < t → ψ1 t ^ 2 < ψ2 t * ψ t) : StrictConvexOn ℝ (Set.Ici 0) fun (t : ℝ) => Real.log (ψ t)

If ψ > 0 is twice differentiable on (0, ∞), continuous on [0, ∞) and ψ'^2 < ψ ψ'' there, then log ψ is strictly convex on [0, ∞).

theorem ProbabilityTheory.Copula.strictConcaveOn_log_of_derivs {ψ ψ1 ψ2 : ℝ → ℝ} (hpos : ∀ (t : ℝ), 0 ≤ t → 0 < ψ t) (hcont : ContinuousOn ψ (Set.Ici 0)) (h1 : ∀ (t : ℝ), 0 < t → HasDerivAt ψ (ψ1 t) t) (h2 : ∀ (t : ℝ), 0 < t → HasDerivAt ψ1 (ψ2 t) t) (h : ∀ (t : ℝ), 0 < t → ψ2 t * ψ t < ψ1 t ^ 2) : StrictConcaveOn ℝ (Set.Ici 0) fun (t : ℝ) => Real.log (ψ t)

If ψ > 0 is twice differentiable on (0, ∞), continuous on [0, ∞) and ψ ψ'' < (ψ')² there, then log ψ is strictly concave on [0, ∞).

theorem ProbabilityTheory.Copula.lt_add_of_strictConvexOn {f : ℝ → ℝ} (hf : StrictConvexOn ℝ (Set.Ici 0) f) (h0 : f 0 = 0) {x y : ℝ} (hx : 0 < x) (hy : 0 < y) : f x + f y < f (x + y)

A strictly convex f on [0, ∞) with f 0 = 0 is strictly superadditive on (0, ∞).

theorem ProbabilityTheory.Copula.BivariateGenerator.mul_lt_toFun_add_of_strictConvexOn (g : BivariateGenerator) (hpos : ∀ (t : ℝ), 0 ≤ t → 0 < g.toFun t) (hf : StrictConvexOn ℝ (Set.Ici 0) fun (t : ℝ) => Real.log (g.toFun t)) {x y : ℝ} (hx : 0 < x) (hy : 0 < y) : g.toFun x * g.toFun y < g.toFun (x + y)

If log ψ is strictly convex on [0, ∞), then ψ(x) ψ(y) < ψ(x + y) for x, y > 0.

theorem ProbabilityTheory.Copula.BivariateGenerator.toFun_add_lt_mul_of_strictConcaveOn (g : BivariateGenerator) (hpos : ∀ (t : ℝ), 0 ≤ t → 0 < g.toFun t) (hf : StrictConcaveOn ℝ (Set.Ici 0) fun (t : ℝ) => Real.log (g.toFun t)) {x y : ℝ} (hx : 0 < x) (hy : 0 < y) : g.toFun (x + y) < g.toFun x * g.toFun y

If log ψ is strictly concave on [0, ∞), then ψ(x + y) < ψ(x) ψ(y) for x, y > 0.

theorem ProbabilityTheory.Copula.BivariateGenerator.isPQD_and_not_isNQD_of_strictConvexOn (g : BivariateGenerator) (hpos : ∀ (t : ℝ), 0 ≤ t → 0 < g.toFun t) (hf : StrictConvexOn ℝ (Set.Ici 0) fun (t : ℝ) => Real.log (g.toFun t)) : g.copula.IsPQD ∧ ¬g.copula.IsNQD

A generator with strictly log-convex inverse generator yields a PQD copula which is not NQD.

theorem ProbabilityTheory.Copula.BivariateGenerator.isNQD_and_not_isPQD_of_strictConcaveOn (g : BivariateGenerator) (hpos : ∀ (t : ℝ), 0 ≤ t → 0 < g.toFun t) (hf : StrictConcaveOn ℝ (Set.Ici 0) fun (t : ℝ) => Real.log (g.toFun t)) : g.copula.IsNQD ∧ ¬g.copula.IsPQD

A generator with strictly log-concave inverse generator yields an NQD copula which is not PQD.