← Copula mathematical handbook

The independence and comonotonic limits of Clayton copulas

The statements apply to any filter of positive parameters. At zero, differentiating the logarithm of the CDF base gives the product limit. At infinity, a power-mean bound squeezes the CDF to its smallest coordinate.

theorem ProbabilityTheory.Copula.tendsto_clayton_zero {d : ℕ} {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), 0 < θ a) (hlim : Filter.Tendsto θ l (nhds 0)) (u : Fin d → ↑unitInterval) : Filter.Tendsto (fun (a : α) => (clayton d (θ a) ⋯).cdf u) l (nhds ((independence d).cdf u))

Positive Clayton parameters approaching zero give the independence CDF.

theorem ProbabilityTheory.Copula.clayton_min_lower_bound {d : ℕ} [NeZero d] (θ : ℝ) (hθ : 0 < θ) (u : Fin d → ↑unitInterval) (hu : ∀ (i : Fin d), 0 < ↑(u i)) : ↑d ^ (-θ⁻¹) * ↑(⨅ (i : Fin d), u i) ≤ (clayton d θ hθ).cdf u

A quantitative lower bound that becomes the minimum-coordinate CDF at infinity.

theorem ProbabilityTheory.Copula.tendsto_clayton_atTop {d : ℕ} {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), 0 < θ a) (hlim : Filter.Tendsto θ l Filter.atTop) (u : Fin d → ↑unitInterval) : Filter.Tendsto (fun (a : α) => (clayton d (θ a) ⋯).cdf u) l (nhds ((comonotonic d).cdf u))

Positive Clayton parameters tending to infinity give the comonotonic CDF.