← Mathematical handbook

Convex logarithmic sections of arbitrary extreme-value copulas

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

Extension to real first coordinates, clamped at the logarithmic boundary.

Equations

• Verification.extremeValueLogSection C y hy x = Verification.extremeValueLog C (max x 0) y ⋯ hy

theorem Verification.extremeValueLogSection_of_nonneg (C : ProbabilityTheory.Copula 2) (y : ℝ) (hy : 0 ≤ y) (x : ℝ) (hx : 0 ≤ x) : extremeValueLogSection C y hy x = extremeValueLog C x y hx hy

theorem Verification.extremeValueLogSection_continuous (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (y : ℝ) (hy : 0 ≤ y) : Continuous (extremeValueLogSection C y hy)

theorem Verification.extremeValueLogSection_geometric (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (y : ℝ) (hy : 0 ≤ y) (x r : ℝ) (hx : 0 < x) (hr : 1 < r) : (r + 1) * extremeValueLogSection C y hy x ≤ r * extremeValueLogSection C y hy (x / r) + extremeValueLogSection C y hy (r * x)

theorem Verification.extremeValueLogSection_convex (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (y : ℝ) (hy : 0 ≤ y) : ConvexOn ℝ (Set.Ioi 0) (extremeValueLogSection C y hy)