← Mathematical handbook

theorem Verification.n22Inv_mem {θ : ℝ} (hθ : 0 < θ) (hθ1 : θ ≤ 1) (u : ↑unitInterval) : (n22Generator θ hθ hθ1).invFun u ∈ Set.Icc 0 (Real.pi / 2)

theorem Verification.n22Comparison_inv {θ η : ℝ} (hθ : 0 < θ) (hθη : θ ≤ η) (hη1 : η ≤ 1) (u : ↑unitInterval) : n22Comparison (η / θ) ((n22Generator θ hθ ⋯).invFun u) = (n22Generator η ⋯ hη1).invFun u

theorem Verification.n22Comparison_psi {θ η t : ℝ} (hθ : 0 < θ) (hθη : θ ≤ η) (hη1 : η ≤ 1) (ht : t ∈ Set.Icc 0 (Real.pi / 2)) : (n22Generator η ⋯ hη1).toFun (n22Comparison (η / θ) t) = (n22Generator θ hθ ⋯).toFun t

theorem Verification.n22Psi_zero {θ t : ℝ} (hθ : 0 < θ) (hθ1 : θ ≤ 1) (ht : Real.pi / 2 ≤ t) : (n22Generator θ hθ hθ1).toFun t = 0

theorem Verification.nelsen22_lowerOrthant_positive {θ η : ℝ} (hθ : 0 < θ) (hθη : θ ≤ η) (hη1 : η ≤ 1) : (nelsen22 η ⋯).LowerOrthantLE (nelsen22 θ ⋯)

theorem Verification.nelsen22_lowerOrthant_antitone {θ η : ℝ} (hθ : θ ∈ Set.Icc 0 1) (hη : η ∈ Set.Icc 0 1) (hθη : θ ≤ η) : (nelsen22 η hη).LowerOrthantLE (nelsen22 θ hθ)

theorem Verification.nelsen22_schur_monotone {θ η : ℝ} (hθ : θ ∈ Set.Icc 0 1) (hη : η ∈ Set.Icc 0 1) (hθη : θ ≤ η) : (nelsen22 θ hθ).SchurBothLE (nelsen22 η hη)