Nelsen 8 infinite-parameter endpoint from Table 2 #
theorem
Papers.AnsariRockel2024.nelsen8_tendsto_atTop
{α : Type u_1}
{l : Filter α}
(θ : α → ℝ)
(hθ : ∀ (a : α), 1 ≤ θ a)
(hlim : Filter.Tendsto θ l Filter.atTop)
(u : Fin 2 → ↑unitInterval)
:
Filter.Tendsto (fun (a : α) => (ProbabilityTheory.Copula.nelsen8 (θ a) ⋯).cdf u) l
(nhds ((ProbabilityTheory.Copula.clayton 2 1 ⋯).cdf u))
Nelsen 8 tends pointwise to Clayton at parameter one throughout the closed square, including its zero axes.