Retained-claim variance is nonnegative
ProvedActuarialValuation.xlRetainedVarianceNonnegativeactuarial-sciencereinsurancerisk-adjusted-retention
Nonnegative scenario weights multiply squared centred retained claims, giving nonnegative variance charge.
Mathematical statement
Preamble
import Mathlib import Definitions.Def_actuarial_xlRetainedVariance open MeasureTheory
Formal statement
namespace ActuarialValuation
theorem xlRetainedVarianceNonnegative {Ω : Type*} [Fintype Ω] (w z : Ω → ℝ) (a : ℝ) (hw : ∀ ω, 0 ≤ w ω)
:
0 ≤ xlRetainedVariance w z a := by sorry
end ActuarialValuationSource
Bäuerle and Glauner (2021), Minimizing spectral risk measures applied to Markov decision processes, Section 6 Dynamic optimal reinsurance, https://doi.org/10.1007/s00186-021-00746-w, expected premium principle pi_R(X)=(1+theta)E[X]; Glauner (2022), Dynamic reinsurance in discrete time minimizing the insurer's cost of capital, Scandinavian Actuarial Journal https://doi.org/10.1080/03461238.2021.1964590; Brachetta Ceci (2019), Optimal Excess-of-Loss Reinsurance for Stochastic Factor Risk Models, https://doi.org/10.3390/risks7020048
Read-back
What the Lean code literally says, in plain math · gpt-6
Independent mathematical reading. Each retained-claim deviation from the weighted mean is squared. Under the theorem's nonnegative weight assumption, every term in the finite variance sum is nonnegative and therefore so is the total. The theorem does not require normalisation for this numerical inequality, although unit mass is required for its familiar statistical interpretation.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.