← Mathematical handbook

theorem Verification.nelsen19_cdf_lower_bound {θ : ℝ} (hθ : 0 < θ) (u v : ↑unitInterval) : min ↑u ↑v / (1 + min ↑u ↑v * Real.log 2 / θ) ≤ (nelsen19 θ ⋯).cdf ![u, v]

theorem Verification.nelsen19_tendsto_atTop {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), 0 ≤ θ a) (ht : Filter.Tendsto θ l Filter.atTop) (u v : ↑unitInterval) : Filter.Tendsto (fun (a : α) => (nelsen19 (θ a) ⋯).cdf ![u, v]) l (nhds ((ProbabilityTheory.Copula.comonotonic 2).cdf ![u, v]))