← Mathematical handbook

theorem Verification.n17_diagonal_lower_bound {θ : ℝ} (hθ : 1 ≤ θ) (t : ↑unitInterval) : (1 + ↑t) * 4 ^ (-θ⁻¹) - 1 ≤ (nelsen17 θ ⋯).diagonal t

theorem Verification.nelsen17_cdf_lower_bound {θ : ℝ} (hθ : 1 ≤ θ) (u v : ↑unitInterval) : (1 + min ↑u ↑v) * 4 ^ (-θ⁻¹) - 1 ≤ (nelsen17 θ ⋯).cdf ![u, v]

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