← Mathematical handbook

theorem Verification.n21CorePrime_neg {θ t : ℝ} (hθ : 0 < θ) (ht : t ∈ Set.Ioo 0 1) : n21CorePrime θ t < 0

theorem Verification.n21CorePrime_strictMono {θ : ℝ} (hθ : 1 < θ) : StrictMonoOn (n21CorePrime θ) (Set.Ioo 0 1)

theorem Verification.n21Core_interior {θ t : ℝ} (hθ : 0 < θ) (ht : t ∈ Set.Ioo 0 1) : n21Core θ t ∈ Set.Ioo 0 1

theorem Verification.n21CorePrime_inverse {θ t : ℝ} (hθ : 0 < θ) (ht : t ∈ Set.Ioo 0 1) : n21CorePrime θ (n21Core θ t) * n21CorePrime θ t = 1

theorem Verification.nelsen21_section_deriv {θ : ℝ} (hθ : 1 ≤ θ) (v : ↑unitInterval) {u : ℝ} (hu : u ∈ Set.Ioo 0 1) (hv : 0 < ↑v) (hs : n21Core θ u + n21Core θ ↑v ∈ Set.Ioo 0 1) : HasDerivAt ((nelsen21 θ hθ).cdfSection v) (n21CorePrime θ (n21Core θ u + n21Core θ ↑v) * n21CorePrime θ u) u

theorem Verification.nelsen21_two_median_energy_lt : ∫ (u : ↑unitInterval), (nelsen21 2 ⋯).conditionalCDF u ProbabilityTheory.Copula.unitHalf ^ 2 < 1 / 2

theorem Verification.nelsen21_not_schur_monotone : ¬∀ (θ η : ℝ) (hθ : 1 ≤ θ) (hθη : θ ≤ η), (nelsen21 θ hθ).SchurLE (nelsen21 η ⋯)

theorem Verification.nelsen21_not_schur_antitone : ¬∀ (θ η : ℝ) (hθ : 1 ≤ θ) (hθη : θ ≤ η), (nelsen21 η ⋯).SchurLE (nelsen21 θ hθ)