← Mathematical handbook

noncomputable def Verification.n21Psi (θ t : ℝ) : ℝ

Equations

• Verification.n21Psi θ t = Verification.n21Core θ (min t 1)

theorem Verification.n21Psi_convex {θ : ℝ} (hθ : 1 ≤ θ) : ConvexOn ℝ (Set.Ici 0) (n21Psi θ)

noncomputable def Verification.n21Generator (θ : ℝ) (hθ : 1 ≤ θ) : ProbabilityTheory.Copula.BivariateGenerator

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Verification.nelsen21 (θ : ℝ) (hθ : 1 ≤ θ) : ProbabilityTheory.Copula 2

Equations

• Verification.nelsen21 θ hθ = (Verification.n21Generator θ hθ).copula

theorem Verification.n21Psi_formula (θ t : ℝ) : n21Psi θ t = 1 - (1 - max 0 (1 - t) ^ θ) ^ θ⁻¹

theorem Verification.nelsen21_cdf (θ : ℝ) (hθ : 1 ≤ θ) (u v : ↑unitInterval) : (nelsen21 θ hθ).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else 1 - (1 - max 0 ((1 - (1 - ↑u) ^ θ) ^ θ⁻¹ + (1 - (1 - ↑v) ^ θ) ^ θ⁻¹ - 1) ^ θ) ^ θ⁻¹

theorem Verification.nelsen21_cdf_full (θ : ℝ) (hθ : 1 ≤ θ) (u v : ↑unitInterval) : (nelsen21 θ hθ).cdf ![u, v] = 1 - (1 - max 0 ((1 - (1 - ↑u) ^ θ) ^ θ⁻¹ + (1 - (1 - ↑v) ^ θ) ^ θ⁻¹ - 1) ^ θ) ^ θ⁻¹

theorem Verification.nelsen21_one : nelsen21 1 ⋯ = ProbabilityTheory.Copula.countermonotonic