theorem
Verification.survivalClayton_linear_limit
{ι : Type u_1}
{l : Filter ι}
(δ : ℝ)
(hδ : 0 < δ)
(c : ι → ℝ)
(hc : ∀ (i : ι), 0 < c i)
(hctop : Filter.Tendsto c l Filter.atTop)
(u v : ↑unitInterval)
(hu : ↑u ∈ Set.Ioo 0 1)
(hv : ↑v ∈ Set.Ioo 0 1)
:
Filter.Tendsto
(fun (i : ι) =>
c i * ((ProbabilityTheory.Copula.clayton 2 δ hδ).survivalCopula.cdf
![ProbabilityTheory.Copula.unitPower u (c i)⁻¹ ⋯, ProbabilityTheory.Copula.unitPower v (c i)⁻¹ ⋯] - 1))
l (nhds (Real.log ↑u + Real.log ↑v + galambosTailKernel δ (-Real.log ↑u) (-Real.log ↑v)))