← Mathematical handbook

theorem Verification.convex_neg_log_one_add_power {α : ℝ} (hα0 : 0 ≤ α) (hα1 : α ≤ 1) : ConvexOn ℝ (Set.Ici 0) fun (t : ℝ) => -Real.log (1 + t ^ α)

noncomputable def Verification.bbPsiDeriv (p q t : ℝ) : ℝ

Equations

• Verification.bbPsiDeriv p q t = -p * q * t ^ (p - 1) * (1 + t ^ p) ^ (-q - 1)

theorem Verification.bbPsi_deriv {p q t : ℝ} (ht : 0 < t) : HasDerivAt (fun (x : ℝ) => (1 + x ^ p) ^ (-q)) (bbPsiDeriv p q t) t

theorem Verification.bbPsiDeriv_neg {p q t : ℝ} (hp : 0 < p) (hq : 0 < q) (ht : 0 < t) : bbPsiDeriv p q t < 0

theorem Verification.bbPsiDeriv_logconvex {p q : ℝ} (hp : 0 < p) (hp1 : p ≤ 1) (hq : 0 < q) : ConvexOn ℝ (Set.Ioi 0) fun (t : ℝ) => Real.log (-bbPsiDeriv p q t)

theorem Verification.bb1_isCI (θ : ℝ) (hθ : 0 < θ) (δ : ℝ) (hδ : 1 ≤ δ) : (ProbabilityTheory.Copula.bb1 θ hθ δ hδ).IsCI

theorem Verification.nelsen12_isCI (θ : ℝ) (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.nelsen12 θ hθ).IsCI

theorem Verification.nelsen14_isCI (θ : ℝ) (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.nelsen14 θ hθ).IsCI