← Copula mathematical handbook

Nelsen 8 infinite-parameter endpoint

The family converges pointwise on the closed square to the Clayton copula with parameter one, as stated in Ansari–Rockel Table 2.

theorem ProbabilityTheory.Copula.tendsto_nelsen8_atTop {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), 1 ≤ θ a) (hlim : Filter.Tendsto θ l Filter.atTop) (u : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (a : α) => (nelsen8 (θ a) ⋯).cdf u) l (nhds ((clayton 2 1 ⋯).cdf u))

The upper endpoint of Nelsen 8 is Clayton with parameter one.