← Mathematical handbook

noncomputable def Verification.extremeValuePowerLog (C : ProbabilityTheory.Copula 2) (θ x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) : ℝ

Equations

• Verification.extremeValuePowerLog C θ x y hx hy = Verification.extremeValueLog C (x ^ θ) (y ^ θ) ⋯ ⋯ ^ (1 / θ)

theorem Verification.extremeValuePowerLog_submodular (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₂ ⋯ ⋯ ≤ extremeValuePowerLog C θ x₁ y₂ hx ⋯ + extremeValuePowerLog C θ x₂ y₁ ⋯ hy