← Mathematical handbook

Logarithmic rectangle inequalities from max-stability

These results require only max-stability of an actual copula, without a density or smoothness assumption. They support the general extreme-value CI proof.

theorem Verification.extremeValue_exp_cdf_pos (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) : 0 < C.cdf ![unitNegExp x hx, unitNegExp y hy]

theorem Verification.extremeValue_log_rectangle (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (u₁ u₂ v₁ v₂ : ↑unitInterval) (hu : u₁ ≤ u₂) (hv : v₁ ≤ v₂) (hp : 0 < C.cdf ![u₁, v₁]) : Real.log (C.cdf ![u₁, v₂]) + Real.log (C.cdf ![u₂, v₁]) ≤ Real.log (C.cdf ![u₁, v₁]) + Real.log (C.cdf ![u₂, v₂])

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

The stable tail function in nonnegative logarithmic coordinates.

Equations

• Verification.extremeValueLog C x y hx hy = -Real.log (C.cdf ![Verification.unitNegExp x hx, Verification.unitNegExp y hy])

theorem Verification.extremeValueLog_submodular (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) {x₁ x₂ y₁ y₂ : ℝ} (hx : 0 ≤ x₁) (hy : 0 ≤ y₁) (hxx : x₁ ≤ x₂) (hyy : y₁ ≤ y₂) : extremeValueLog C x₁ y₁ hx hy + extremeValueLog C x₂ y₂ ⋯ ⋯ ≤ extremeValueLog C x₁ y₂ hx ⋯ + extremeValueLog C x₂ y₁ ⋯ hy

theorem Verification.extremeValueLog_zero_right (C : ProbabilityTheory.Copula 2) (x : ℝ) (hx : 0 ≤ x) : extremeValueLog C x 0 hx ⋯ = x

theorem Verification.extremeValueLog_zero_left (C : ProbabilityTheory.Copula 2) (y : ℝ) (hy : 0 ≤ y) : extremeValueLog C 0 y ⋯ hy = y

theorem Verification.extremeValueLog_homogeneous (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (x y t : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) (ht : 0 ≤ t) : extremeValueLog C (t * x) (t * y) ⋯ ⋯ = t * extremeValueLog C x y hx hy

theorem Verification.extremeValueLog_increment_first (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) {x₁ x₂ y : ℝ} (hx : 0 ≤ x₁) (hy : 0 ≤ y) (hxx : x₁ ≤ x₂) : 0 ≤ extremeValueLog C x₂ y ⋯ hy - extremeValueLog C x₁ y hx hy ∧ extremeValueLog C x₂ y ⋯ hy - extremeValueLog C x₁ y hx hy ≤ x₂ - x₁

theorem Verification.extremeValueLog_increment_second (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) {x y₁ y₂ : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y₁) (hyy : y₁ ≤ y₂) : 0 ≤ extremeValueLog C x y₂ hx ⋯ - extremeValueLog C x y₁ hx hy ∧ extremeValueLog C x y₂ hx ⋯ - extremeValueLog C x y₁ hx hy ≤ y₂ - y₁

theorem Verification.extremeValueLog_bounds (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) : max x y ≤ extremeValueLog C x y hx hy ∧ extremeValueLog C x y hx hy ≤ x + y

theorem Verification.extremeValue_pickands_bounds (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (t : ↑unitInterval) : max (1 - ↑t) ↑t ≤ copulaPickands C t ∧ copulaPickands C t ≤ 1