← Mathematical handbook

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

Equations

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

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

Equations

• Verification.n20PsiDeriv p t = -p * Real.log (t + Real.exp 1) ^ (-p - 1) / (t + Real.exp 1)

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

Equations

• Verification.n20Second p t = p * Real.log (t + Real.exp 1) ^ (-p - 2) * (Real.log (t + Real.exp 1) + p + 1) / (t + Real.exp 1) ^ 2

theorem Verification.n20Psi_deriv {p t : ℝ} (ht : 0 ≤ t) : HasDerivAt (n20Psi p) (n20PsiDeriv p t) t

theorem Verification.n20Psi_deriv2 {p t : ℝ} (ht : 0 ≤ t) : HasDerivAt (n20PsiDeriv p) (n20Second p t) t

theorem Verification.n20Psi_convex {p : ℝ} (hp : 0 < p) : ConvexOn ℝ (Set.Ici 0) (n20Psi p)

theorem Verification.n20Psi_antitone {p : ℝ} (hp : 0 < p) : AntitoneOn (n20Psi p) (Set.Ici 0)

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

Equations

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

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

Equations

• Verification.nelsen20 θ hθ = if hz : θ = 0 then ProbabilityTheory.Copula.independence 2 else (Verification.nelsen20Generator θ ⋯).copula

theorem Verification.nelsen20_zero : nelsen20 0 ⋯ = ProbabilityTheory.Copula.independence 2

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