Fractional quarterly udd example
ProvedActuarialAnnuities.fractional_quarterly_udd_exampleactuarial-scienceannuity-cashflowfractionalsingle-life-annuities
Exact quarterly UDD annuity-due worked case with £1 annual rate and zero interest. The theorem respects the exact payment-date, valuation and guarantee units in the underlying contract.
Mathematical relation:
This is an open derived mathematical target, with its complete assumptions recorded in the separate formal proposition.
Units: Present value in GBP per unit nominal pension, with individual instalments in GBP, payment time in anniversaries and survival as dimensionless probability.
Preamble
import Mathlib.Data.Real.Basic import Mathlib.Algebra.BigOperators.Group.Finset.Basic import Definitions.Def_actuarial_bFractionalExpectedPV
Formal statement
namespace ActuarialAnnuities theorem fractional_quarterly_udd_example : bFractionalExpectedPV 3 0 3 0 0 4 1 (fun _ => 1) (fun k => if k ≤ 3 then (1/4 : ℝ) else 0) = 63/32 := by sorry end ActuarialAnnuities
Source
Original derived finite annuity result. Contextual source page 152, Dickson, Hardy and Waters (2020), Actuarial Mathematics for Life Contingent Risks, third edition, Chapter 5 (and Chapter 4 for assurance). https://api.pageplace.de/preview/DT0400.9781108787406_A49239377/preview-9781108787406_A49239377.pdf. The exact definition or theorem is an original payment-event formalisation, not a numbered published result. Exact quarterly UDD annuity-due worked case with £1 annual rate and zero interest.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.