← Mathematical handbook

noncomputable def Verification.n13Psi (p t : ℝ) : ℝ

Equations

• Verification.n13Psi p t = Real.exp (1 - (1 + t) ^ p)

noncomputable def Verification.n13PsiDeriv (p t : ℝ) : ℝ

Equations

• Verification.n13PsiDeriv p t = -p * (1 + t) ^ p / (1 + t) * Verification.n13Psi p t

theorem Verification.n13Psi_deriv (p t : ℝ) (ht : 0 < 1 + t) : HasDerivAt (n13Psi p) (n13PsiDeriv p t) t

theorem Verification.n13Psi_deriv2 (p t : ℝ) (ht : 0 < 1 + t) : HasDerivAt (n13PsiDeriv p) (p * (1 + t) ^ p / (1 + t) ^ 2 * (p * (1 + t) ^ p - p + 1) * n13Psi p t) t

theorem Verification.n13Psi_convex (p : ℝ) (hp : 0 < p) : ConvexOn ℝ (Set.Ici 0) (n13Psi p)

theorem Verification.n13_inv_base (u : ↑unitInterval) : 1 ≤ 1 - Real.log ↑u

noncomputable def Verification.nelsen13Generator (θ : ℝ) (hθ : 0 < θ) : ProbabilityTheory.Copula.BivariateGenerator

Equations

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

noncomputable def Verification.nelsen13 (θ : ℝ) (hθ : 0 ≤ θ) : ProbabilityTheory.Copula 2

Equations

• Verification.nelsen13 θ hθ = if hz : θ = 0 then Verification.gumbelBarnett 1 else (Verification.nelsen13Generator θ ⋯).copula

theorem Verification.nelsen13_zero : nelsen13 0 ⋯ = gumbelBarnett 1

theorem Verification.nelsen13_cdf (θ : ℝ) (hθ : 0 < θ) (u v : ↑unitInterval) : (nelsen13 θ ⋯).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else Real.exp (1 - ((1 - Real.log ↑u) ^ θ + (1 - Real.log ↑v) ^ θ - 1) ^ θ⁻¹)

theorem Verification.nelsen13_one : nelsen13 1 ⋯ = ProbabilityTheory.Copula.independence 2