Prove2Me

Within-year survival and discount timing: frUdd_nonneg

Proved
ActuarialValuation.frUdd_nonneg

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

actuarial-scienceformal-verificationfractional-life-valuation

Within-year survival remains nonnegative when annual mortality and elapsed duration belong to the unit interval.

Mathematical relation:

frUdd_nonnegfrUdd\_nonneg

Original derived theorem target; the Lean statement gives the exact conditions and result.

Preamble
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Analysis.SpecialFunctions.Exp
import Definitions.Def_actuarial_frUddSurvival
Formal statement
namespace ActuarialValuation

theorem frUdd_nonneg (q s : ℝ) (hq0 : 0 ≤ q) (hq1 : q ≤ 1) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) : 0 ≤ frUddSurvival q s := by sorry

end ActuarialValuation
Source
Original derived actuarial mathematics inspired by Promislow (2015), chapters 7, 4 and 8, published book reference https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/; supporting published actuarial reference https://www.soa.org/498941/globalassets/assets/files/e-business/pd/events/2018/las/pd-2018-05-las-session-033.pdf. Published source page 98 of Promislow's 2015 edition provides the thematic mathematical context. The target Lean identity is an original derivation, not a verbatim published result.
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