Supporting lines for extreme-value logarithmic sections #
theorem
Verification.extremeValueLogSection_support
(C : ProbabilityTheory.Copula 2)
(hC : C.IsExtremeValue)
(y : ℝ)
(hy : 0 ≤ y)
(x : ℝ)
(hx : 0 < x)
:
∃ p ∈ Set.Icc 0 1, ∀ (z : ℝ), 0 ≤ z → extremeValueLogSection C y hy x + p * (z - x) ≤ extremeValueLogSection C y hy z