← Mathematical handbook

theorem Verification.n20Comparison_inv {θ η : ℝ} (hθ : 0 < θ) (hη : 0 < η) (u : ↑unitInterval) (hu : u ≠ 0) : n20Comparison θ η ((nelsen20Generator θ hθ).invFun u) = (nelsen20Generator η hη).invFun u

theorem Verification.n20Comparison_psi {θ η t : ℝ} (hθ : 0 < θ) (hη : 0 < η) (ht : 0 ≤ t) : n20Psi η⁻¹ (n20Comparison θ η t) = n20Psi θ⁻¹ t

theorem Verification.nelsen20_lowerOrthant_monotone_pos {θ η : ℝ} (hθ : 0 < θ) (hη : 0 < η) (hθη : θ ≤ η) : (nelsen20 θ ⋯).LowerOrthantLE (nelsen20 η ⋯)

theorem Verification.nelsen20_lowerOrthant_monotone {θ η : ℝ} (hθ : 0 ≤ θ) (hη : 0 ≤ η) (hθη : θ ≤ η) : (nelsen20 θ hθ).LowerOrthantLE (nelsen20 η hη)

theorem Verification.nelsen20_schur_monotone {θ η : ℝ} (hθ : 0 ≤ θ) (hη : 0 ≤ η) (hθη : θ ≤ η) : (nelsen20 θ hθ).SchurBothLE (nelsen20 η hη)