← Mathematical handbook

Identification of the local Frechet bounds with the actual beta extremizers.

theorem Papers.Rockel2026ExactBlest.beta_cdf_scalar (q u v : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (_hu : u ∈ Set.Icc 0 1) (_hv : v ∈ Set.Icc 0 1) : min q (min u v) + max 0 (min (1 / 2) (min u (v - 1 / 2 + q)) - q) + max 0 (min (1 - q) (min u (v + 1 / 2 - q)) - 1 / 2) + max 0 (min u v - (1 - q)) = localUpper q u v

theorem Papers.Rockel2026ExactBlest.beta_shuffle_cdf (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (u v : ↑unitInterval) : MeasureTheory.volume.real {x : ↑unitInterval | x ≤ u ∧ betaRank q hq x ≤ v} = localUpper q ↑u ↑v

theorem Papers.Rockel2026ExactBlest.beta_upper_cdf (C : ProbabilityTheory.Copula 2) (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (hb : C.blomqvistBeta = 4 * q - 1) (hn : Rockel2026XiBlest.blestNu C = betaUpper C.blomqvistBeta) (u v : ↑unitInterval) : C.cdf ![u, v] = localUpper q ↑u ↑v

theorem Papers.Rockel2026ExactBlest.local_bounds_reflection (q u v : ℝ) (_hq : q ∈ Set.Icc 0 (1 / 2)) (_hu : u ∈ Set.Icc 0 1) (_hv : v ∈ Set.Icc 0 1) : u - localUpper (1 / 2 - q) u (1 - v) = localLower q u v

theorem Papers.Rockel2026ExactBlest.beta_lower_cdf (C : ProbabilityTheory.Copula 2) (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (hb : C.blomqvistBeta = 4 * q - 1) (hn : Rockel2026XiBlest.blestNu C = betaLower C.blomqvistBeta) (u v : ↑unitInterval) : C.cdf ![u, v] = localLower q ↑u ↑v