Nelsen 2 infinite-parameter endpoint from Table 2 #
theorem
Papers.AnsariRockel2024.nelsen2_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.nelsen2 (θ a) ⋯).cdf u) l
(nhds ((ProbabilityTheory.Copula.comonotonic 2).cdf u))
The Nelsen 2 copula tends pointwise to the upper Fréchet bound on the entire closed square as its parameter tends to infinity.