Exponential moment nonnegative for nonnegative scenario weights
ProvedActuarialValuation.finiteExponentialMoment_nonnegativeactuarial-scienceentropic-riskexponential-premium
Every scenario exponential is strictly positive; multiplied by a nonnegative weight it is nonnegative, so its finite sum is nonnegative.
Mathematical statement
Preamble
import Mathlib import Definitions.Def_actuarial_finiteExponentialMoment open MeasureTheory
Formal statement
namespace ActuarialValuation
theorem finiteExponentialMoment_nonnegative {Ω : Type*} [Fintype Ω] (w X : Ω → ℝ) (gamma : ℝ)
(hw : ∀ ω, 0 ≤ w ω)
:
0 ≤ finiteExponentialMoment w X gamma := 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. Assume each scenario weight is nonnegative. For every real loss and real sensitivity the exponential factor is strictly positive, so each weighted contribution is nonnegative and their finite sum is nonnegative. Total probability mass one is not needed for this inequality; some weights may all be zero.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.