← Mathematical handbook

theorem Verification.n21Core_upper_bound {θ t : ℝ} (hθ : 1 ≤ θ) (ht : t ∈ Set.Icc 0 1) : n21Core θ t ≤ (1 - t) ^ θ

theorem Verification.n21Psi_lower_bound {θ s : ℝ} (hθ : 1 ≤ θ) (hs : 0 ≤ s) : 1 - (θ * s) ^ θ⁻¹ ≤ n21Psi θ s

theorem Verification.n21_diagonal_formula (θ : ℝ) (hθ : 1 ≤ θ) (t : ↑unitInterval) : (nelsen21 θ hθ).diagonal t = n21Psi θ (2 * n21Core θ ↑t)

theorem Verification.n21_diagonal_lower_bound (θ : ℝ) (hθ : 1 ≤ θ) (t : ↑unitInterval) : 1 - (2 * θ) ^ θ⁻¹ * (1 - ↑t) ≤ (nelsen21 θ hθ).diagonal t

theorem Verification.nelsen21_cdf_lower_bound (θ : ℝ) (hθ : 1 ≤ θ) (u v : ↑unitInterval) : 1 - (2 * θ) ^ θ⁻¹ * (1 - min ↑u ↑v) ≤ (nelsen21 θ hθ).cdf ![u, v]

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

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

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