← Mathematical handbook

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

Equations

• Verification.n19Psi θ t = θ / Real.log (t + Real.exp θ)

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

Equations

• Verification.n19PsiDeriv θ t = -θ / ((t + Real.exp θ) * Real.log (t + Real.exp θ) ^ 2)

theorem Verification.n19_log_pos {θ t : ℝ} (hθ : 0 < θ) (ht : 0 ≤ t) : 0 < Real.log (t + Real.exp θ)

theorem Verification.n19Psi_deriv {θ t : ℝ} (hθ : 0 < θ) (ht : 0 ≤ t) : HasDerivAt (n19Psi θ) (n19PsiDeriv θ t) t

theorem Verification.n19Psi_deriv2 {θ t : ℝ} (hθ : 0 < θ) (ht : 0 ≤ t) : HasDerivAt (n19PsiDeriv θ) (θ * (Real.log (t + Real.exp θ) + 2) / ((t + Real.exp θ) ^ 2 * Real.log (t + Real.exp θ) ^ 3)) t

theorem Verification.n19Psi_antitone {θ : ℝ} (hθ : 0 < θ) : AntitoneOn (n19Psi θ) (Set.Ici 0)

theorem Verification.n19Psi_convex {θ : ℝ} (hθ : 0 < θ) : ConvexOn ℝ (Set.Ici 0) (n19Psi θ)

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

Equations

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

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

Equations

• Verification.nelsen19 θ hθ = if hz : θ = 0 then ProbabilityTheory.Copula.clayton 2 1 Verification.nelsen19._proof_1 else (Verification.nelsen19Generator θ ⋯).copula

theorem Verification.nelsen19_zero : nelsen19 0 ⋯ = ProbabilityTheory.Copula.clayton 2 1 ⋯

theorem Verification.nelsen19_cdf {θ : ℝ} (hθ : 0 < θ) (u v : ↑unitInterval) : (nelsen19 θ ⋯).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else θ / Real.log (Real.exp (θ / ↑u) + Real.exp (θ / ↑v) - Real.exp θ)