← Mathematical handbook

TP2 of Archimedean CDFs with log-convex inverse generators

theorem ProbabilityTheory.Copula.BivariateGenerator.isTP2CDF_of_logConvex (g : BivariateGenerator) (hpos : ∀ (t : ℝ), 0 ≤ t → 0 < g.toFun t) (hconv : ConvexOn ℝ (Set.Ici 0) fun (t : ℝ) => Real.log (g.toFun t)) : g.copula.IsTP2CDF

A positive log-convex inverse generator yields a TP2 bivariate CDF.

theorem ProbabilityTheory.Copula.isTP2CDF_bb1 (θ : ℝ) (hθ : 0 < θ) (δ : ℝ) (hδ : 1 ≤ δ) : (bb1 θ hθ δ hδ).IsTP2CDF

Every bivariate BB1 copula has a TP2 CDF at positive Clayton parameter and outer-power parameter at least one. This is a CDF property, not an MTP2 density claim.