← Mathematical handbook

theorem Verification.exp_neg_four_point {a b c d : ℝ} (hab : a ≤ b) (hac : a ≤ c) (hs : a + d ≤ b + c) : 0 ≤ Real.exp (-a) - Real.exp (-b) - Real.exp (-c) + Real.exp (-d)

theorem Verification.extremeValuePowerLog_mono (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (θ : ℝ) (hθ : 1 ≤ θ) {x₁ x₂ y₁ y₂ : ℝ} (hx : 0 ≤ x₁) (hy : 0 ≤ y₁) (hxx : x₁ ≤ x₂) (hyy : y₁ ≤ y₂) : extremeValuePowerLog C θ x₁ y₁ hx hy ≤ extremeValuePowerLog C θ x₂ y₂ ⋯ ⋯

theorem Verification.extremeValuePowerLog_exp_rectangle (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (θ : ℝ) (hθ : 1 ≤ θ) {x₁ x₂ y₁ y₂ : ℝ} (hx : 0 ≤ x₁) (hy : 0 ≤ y₁) (hxx : x₁ ≤ x₂) (hyy : y₁ ≤ y₂) : 0 ≤ Real.exp (-extremeValuePowerLog C θ x₁ y₁ hx hy) - Real.exp (-extremeValuePowerLog C θ x₁ y₂ hx ⋯) - Real.exp (-extremeValuePowerLog C θ x₂ y₁ ⋯ hy) + Real.exp (-extremeValuePowerLog C θ x₂ y₂ ⋯ ⋯)