Normalised stochastic transitions give a positive exponential moment
ProvedActuarialValuation.finiteEntropicTransitionMoment_posA stochastic transition row has nonnegative entries adding to one; at least one entry is positive. Every real exponential of a finite real-valued loss is strictly positive, so the sum of these weighted exponentials is strictly positive. This remains valid for arbitrary real beta and gamma and for some zero-probability destination states.
Mathematical statement
import Mathlib import Definitions.Def_actuarial_finiteEntropicTransitionMoment
namespace ActuarialValuation
theorem finiteEntropicTransitionMoment_pos {S A : Type*} [Fintype S]
(P : S → A → S → ℝ) (cost : S → A → S → ℝ)
(beta gamma : ℝ) (next : S → ℝ) (s : S) (a : A)
(hP : ∀ t, 0 ≤ P s a t)
(hsum : (∑ t : S, P s a t) = 1) :
0 < finiteEntropicTransitionMoment P cost beta gamma next s a := by sorry
end ActuarialValuationRead-back
What the Lean code literally says, in plain math · gpt-6
Independent mathematical reading. At one fixed state and action, nonnegative real transition weights with sum exactly one give a nonempty positive-weight contribution. Since the exponential of every finite real number is positive, the resulting weighted exponential moment is strictly positive. Neither the annual cost nor the continuation needs a lower bound in the finite real-valued setting; the theorem also permits any real gamma and beta.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.