← Mathematical handbook

Pointwise local Frechet bounds used in exact-blest-regions.tex.

theorem Papers.Rockel2026ExactBlest.cdf_increment_positive (C : ProbabilityTheory.Copula 2) (u v : Fin 2 → ↑unitInterval) : C.cdf u - C.cdf v ≤ ∑ i : Fin 2, max (↑(u i) - ↑(v i)) 0

noncomputable def Papers.Rockel2026ExactBlest.localUpper (q u v : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.localUpper q u v = min (min u v) (q + max (u - 1 / 2) 0 + max (v - 1 / 2) 0)

noncomputable def Papers.Rockel2026ExactBlest.localLower (q u v : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.localLower q u v = max (max 0 (u + v - 1)) (q - max (1 / 2 - u) 0 - max (1 / 2 - v) 0)

theorem Papers.Rockel2026ExactBlest.cdf_le_localUpper (C : ProbabilityTheory.Copula 2) (u v : ↑unitInterval) : C.cdf ![u, v] ≤ localUpper (C.cdf ![ProbabilityTheory.Copula.unitHalf, ProbabilityTheory.Copula.unitHalf]) ↑u ↑v

theorem Papers.Rockel2026ExactBlest.localLower_le_cdf (C : ProbabilityTheory.Copula 2) (u v : ↑unitInterval) : localLower (C.cdf ![ProbabilityTheory.Copula.unitHalf, ProbabilityTheory.Copula.unitHalf]) ↑u ↑v ≤ C.cdf ![u, v]

theorem Papers.Rockel2026ExactBlest.local_frechet_bounds (C : ProbabilityTheory.Copula 2) (q : ℝ) (hq : C.cdf ![ProbabilityTheory.Copula.unitHalf, ProbabilityTheory.Copula.unitHalf] = q) (u v : ↑unitInterval) : localLower q ↑u ↑v ≤ C.cdf ![u, v] ∧ C.cdf ![u, v] ≤ localUpper q ↑u ↑v