Prove2Me

Independent and dependent upper-tail co-exceedance: coInd_lower_ratio

Proved
ActuarialValuation.coInd_lower_ratio

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

actuarial-copula-dependenceactuarial-scienceformal-verification

Independence makes lower-tail conditional probability equal the threshold. This original derived actuarial relation uses the parameter restrictions, endpoints and units stated in the separate formal theorem or definition.

Mathematical relation:

Pr⁡(U>u,V>v)=1−u−v+C(u,v)\Pr(U>u,V>v)=1-u-v+C(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_coInd
import Definitions.Def_actuarial_coLowerRatio
Formal statement
namespace ActuarialValuation

theorem coInd_lower_ratio (u : ℝ) (hu : u≠0) : coLowerRatio coInd u=u := 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