Joe infinite-parameter endpoint #
The power-sum-minus-product CDF base is squeezed between the maximum term and the two-term power sum. Its pointwise limit is comonotonicity.
theorem
ProbabilityTheory.Copula.tendsto_joe_atTop
{α : Type u_1}
{l : Filter α}
(θ : α → ℝ)
(hθ : ∀ (z : α), 1 ≤ θ z)
(hlim : Filter.Tendsto θ l Filter.atTop)
(u : Fin 2 → ↑unitInterval)
:
Filter.Tendsto (fun (z : α) => (joe (θ z) ⋯).cdf u) l (nhds ((comonotonic 2).cdf u))
Joe converges pointwise to the upper Fréchet bound.