Prove2Me

Rectangle probability, Fréchet bounds and copula construction: coRectangle_zero_width

Proved
ActuarialValuation.coRectangle_zero_width

by WillR · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

actuarial-copula-dependenceactuarial-scienceformal-verification

A rectangle of zero width has zero joint probability mass. This original derived actuarial relation uses the parameter restrictions, endpoints and units stated in the separate formal theorem or definition.

Mathematical relation:

max⁡(0,u+v−1)≤C(u,v)≤min⁡(u,v)\max(0,u+v-1)\le C(u,v)\le\min(u,v)
Preamble
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.Order.Group.MinMax
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Definitions.Def_actuarial_coRectangle
Formal statement
namespace ActuarialValuation

theorem coRectangle_zero_width (C : ℝ → ℝ → ℝ) (u v1 v2 : ℝ) : coRectangle C u u v1 v2=0 := by sorry

end ActuarialValuation
Source
Original derived actuarial mathematics, published source page 4. Sklar (1959), Fonctions de répartition à n dimensions et leurs marges, Publications de l'Institut de Statistique de l'Université de Paris; actuarial copula dependence in risk, https://www.mdpi.com/1911-8074/12/2/65; dependent insurance exposures, https://doi.org/10.1007/s13385-022-00326-0. Parent topic: Bivariate copula margins, rectangle 2-increasing criterion, Fréchet-Hoeffding bounds, FGM mixtures and insurance tail co-exceedance. The particular Lean formula is a new finite/real-algebraic formalisation and remains an unproved theorem target if labelled theorem. Relevant published actuarial derivation: https://www.mdpi.com/1911-8074/12/2/65
Human review

  • Endorsed by Shuze Chen · Oct 11, 2026

    Confirmed by the moderator at approval.

  • Endorsed by WillR · Oct 11, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph