Coherent worst-case actuarial premium and portfolio: crRisk_symmetry
ProvedActuarialValuation.crRisk_symmetryactuarial-sciencecoherent-risk-measure-stop-lossformal-verification
Interchanging the two possible probability laws does not change the conservative premium.
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_crScenarioRisk
Formal statement
namespace ActuarialValuation
theorem crRisk_symmetry {n : ℕ} (p q X : Fin n→ℝ) : crScenarioRisk p q X = crScenarioRisk q p X := 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.