Joe infinite-parameter endpoint from Table 2 #
theorem
Papers.AnsariRockel2024.joe_tendsto_atTop
{α : Type u_1}
{l : Filter α}
(θ : α → ℝ)
(hθ : ∀ (z : α), 1 ≤ θ z)
(hlim : Filter.Tendsto θ l Filter.atTop)
(u : Fin 2 → ↑unitInterval)
:
Filter.Tendsto (fun (z : α) => (ProbabilityTheory.Copula.joe (θ z) ⋯).cdf u) l
(nhds ((ProbabilityTheory.Copula.comonotonic 2).cdf u))
The Joe CDF converges pointwise to the upper Fréchet bound throughout the closed square as its parameter tends to infinity.