Actual finite loss distributions and scenario ambiguity: crExpected_zero
ProvedActuarialValuation.crExpected_zeroactuarial-sciencecoherent-risk-measure-stop-lossformal-verification
Zero portfolio loss produces zero expected outgo under any weights.
Mathematical relation:
Original derived theorem target; the Lean statement gives the exact conditions and result.
Preamble
import Mathlib.Data.Real.Basic import Mathlib.Data.Fintype.Basic import Mathlib.Algebra.BigOperators.Group.Finset.Basic import Definitions.Def_actuarial_crExpected
Formal statement
namespace ActuarialValuation
theorem crExpected_zero {n : ℕ} (p : Fin n→ℝ) : crExpected p (fun _ => 0) = 0 := by sorry
end ActuarialValuationSource
Original derived actuarial mathematics inspired by Promislow (2015), chapters 22, published book reference https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/; supporting published actuarial reference https://doi.org/10.1111/1467-9965.00068. The proposed model is rooted in Promislow chapter 22. The target Lean identity is an original derivation, not a verbatim published result. Published source page 412 gives the actuarial risk assessment chapter context; the Lean statement is an original derived target.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.