logUtility_limit_eq_two
plain-language theorem explainer
Unitless logarithmic utility partial sums for the St. Petersburg game converge to 2. Decision theorists resolving the paradox via log utility would cite this limit to establish finiteness. The proof rewrites the partial sum via its closed form then subtracts the auxiliary term that vanishes at infinity.
Claim. $lim_{N to infty} sum_{n=1}^N n cdot 2^{-n} = 2$
background
The St. Petersburg module constructs the classic paradox ensemble: outcomes indexed by n in natural numbers, probability 2^{-n}, payout 2^n. Linear utility partial sums equal N and diverge to infinity. Logarithmic utility is handled in unitless form as the partial sums of n 2^{-n}, which the module shows remain bounded and converge. logUtilityPartial denotes this partial sum up to N. The upstream theorem logUtilityPartial_closed_form supplies the identity logUtilityPartial N = 2 - (N+2) 2^{-N} for every N. The auxiliary theorem aux_limit_N_plus_two_div_pow establishes that (N+2) 2^{-N} tends to 0.
proof idea
The proof first rewrites the sequence of partial sums to the closed-form expression 2 minus (N+2) 2^{-N} by applying logUtilityPartial_closed_form. It invokes tendsto_const_nhds to obtain the constant sequence tending to 2, then subtracts the vanishing term via the auxiliary limit aux_limit_N_plus_two_div_pow. Simplification of the difference yields the required limit at 2.
why it matters
This limit is invoked directly by logUtility_converges to witness existence of the limit, by stPetersburg_dichotomy to bound log utility above by 2, and by both stPetersburgCert and st_petersburg_one_statement to certify the full linear-log dichotomy. It completes the convergence half of the log-utility resolution in the module, consistent with the J-cost shaped utility in the Recognition framework where logarithmic forms produce finite expectations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.