← Mathematical handbook

Convexity of the canonical Pickands function on the closed interval

theorem Verification.copulaPickands_eq_log (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (t : ↑unitInterval) : copulaPickands C t = extremeValueLog C (1 - ↑t) ↑t ⋯ ⋯

theorem Verification.copulaPickands_perspective (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (t : ↑unitInterval) (ht : 0 < ↑t) : copulaPickands C t = ↑t * extremeValueLogSection C 1 ⋯ ((1 - ↑t) / ↑t)

theorem Verification.copulaPickands_support (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (t : ↑unitInterval) (ht0 : 0 < ↑t) (ht1 : ↑t < 1) : ∃ (p : ℝ) (q : ℝ), copulaPickands C t = p * (1 - ↑t) + q * ↑t ∧ ∀ (s : ↑unitInterval), p * (1 - ↑s) + q * ↑s ≤ copulaPickands C s

Every interior Pickands point admits a linear support valid also at both endpoints.

noncomputable def Verification.copulaPickandsReal (C : ProbabilityTheory.Copula 2) (t : ℝ) : ℝ

Real-coordinate extension used only to state ordinary ConvexOn on [0,1].

Equations

• Verification.copulaPickandsReal C t = Verification.extremeValueLog C (max (1 - t) 0) (max t 0) ⋯ ⋯

theorem Verification.copulaPickandsReal_coe (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (t : ↑unitInterval) : copulaPickandsReal C ↑t = copulaPickands C t

theorem Verification.copulaPickandsReal_convex (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) : ConvexOn ℝ (Set.Icc 0 1) (copulaPickandsReal C)