Prove2Me

Bivariate joint distribution and boundary constraints: coInd_right_margin

Proved
ActuarialValuation.coInd_right_margin

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

actuarial-copula-dependenceactuarial-scienceformal-verification

Uniform first marginal returns second marginal. This original derived actuarial relation uses the parameter restrictions, endpoints and units stated in the separate formal theorem or definition.

Mathematical relation:

C(u,0)=0,C(1,v)=v,C(u,1)=uC(u,0)=0,\quad C(1,v)=v,\quad C(u,1)=u
Preamble
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.Order.Group.MinMax
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Definitions.Def_actuarial_coInd
Formal statement
namespace ActuarialValuation

theorem coInd_right_margin (v : ℝ) : coInd 1 v=v := 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