← Mathematical handbook

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

theorem Verification.nelsen20_cdf_lower_bound {θ : ℝ} (hθ : 0 < θ) (u v : ↑unitInterval) : min ↑u ↑v * (1 + Real.log 2) ^ (-θ⁻¹) ≤ (nelsen20 θ ⋯).cdf ![u, v]

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