Zero loss has zero exponential premium
ProvedActuarialValuation.finiteEntropicPremium_zero_lossactuarial-scienceentropic-riskexponential-premium
With unit scenario mass, the zero-loss exponential moment is one and its logarithm is zero; dividing by gamma yields zero even with Lean's totalised zero division.
Mathematical statement
Preamble
import Mathlib import Definitions.Def_actuarial_finiteEntropicPremium open MeasureTheory
Formal statement
namespace ActuarialValuation
theorem finiteEntropicPremium_zero_loss {Ω : Type*} [Fintype Ω] (w : Ω → ℝ) (gamma : ℝ)
(hsum : (∑ ω : Ω, w ω) = 1)
:
finiteEntropicPremium w (fun _ => 0) gamma = 0 := by sorry
end ActuarialValuationSource
Tsanakas and Desli (2003), Risk measures and theories of choice, British Actuarial Journal 9(4), 959-991, exponential premium principle, https://doi.org/10.1017/S1357321700004414; Baeuerle and Glauner (2022), Markov decision processes with recursive risk measures, European Journal of Operational Research 296(3), 953-966, https://doi.org/10.1016/j.ejor.2021.04.030; Baeuerle and Glauner (2021), Minimizing spectral risk measures applied to Markov decision processes, https://doi.org/10.1007/s00186-021-00746-w, section 2 entropic risk definition
Read-back
What the Lean code literally says, in plain math · gpt-6
Independent mathematical reading. When all losses are zero and scenario weights sum to one, the exponential moment is one. Its logarithm is zero, so the entropic premium definition gives zero for every real gamma, including the totalised algebraic zero-sensitivity case. The statement does not identify the latter with any analytically defined expectation limit.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.