← Mathematical handbook

noncomputable def Verification.n14Inv (θ u : ℝ) : ℝ

Equations

• Verification.n14Inv θ u = (u ^ (-θ⁻¹) - 1) ^ θ

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

Equations

• Verification.n14Psi θ t = (1 + t ^ θ⁻¹) ^ (-θ)

theorem Verification.n14Inv_base {θ : ℝ} (hθ : 0 < θ) {u : ↑unitInterval} (hu : 0 < ↑u) : 0 ≤ ↑u ^ (-θ⁻¹) - 1

theorem Verification.n14Comparison_inv {θ η : ℝ} (hθ : 0 < θ) (hη : 0 < η) {u : ↑unitInterval} (hu : 0 < ↑u) : n14Comparison θ η (n14Inv θ ↑u) = n14Inv η ↑u

theorem Verification.n14Comparison_psi {θ η t : ℝ} (hθ : 0 < θ) (hη : 0 < η) (ht : 0 ≤ t) : n14Psi η (n14Comparison θ η t) = n14Psi θ t

theorem Verification.nelsen14_lowerOrthant_monotone {θ η : ℝ} (hθ : 1 ≤ θ) (hη : 1 ≤ η) (hθη : θ ≤ η) : (ProbabilityTheory.Copula.nelsen14 θ hθ).LowerOrthantLE (ProbabilityTheory.Copula.nelsen14 η hη)

theorem Verification.nelsen14_schur_monotone {θ η : ℝ} (hθ : 1 ≤ θ) (hη : 1 ≤ η) (hθη : θ ≤ η) : (ProbabilityTheory.Copula.nelsen14 θ hθ).SchurBothLE (ProbabilityTheory.Copula.nelsen14 η hη)