← Mathematical handbook

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

theorem Verification.n18_diagonal_normalized (θ : ℝ) (hθ : 2 ≤ θ) (t : ↑unitInterval) (ht : t < 1) : (nelsen18 θ hθ).diagonal t = max 0 (1 + 1 / (Real.log 2 / θ + 1 / (↑t - 1)))

theorem Verification.nelsen18_diagonal_tendsto_atTop {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), 2 ≤ θ a) (ht : Filter.Tendsto θ l Filter.atTop) (t : ↑unitInterval) : Filter.Tendsto (fun (a : α) => (nelsen18 (θ a) ⋯).diagonal t) l (nhds ↑t)

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