logUtilityPartial
plain-language theorem explainer
The partial sum of log-utility contributions up to N outcomes in the St. Petersburg game equals the sum from n=1 to N of n/2^n. Decision theorists resolving the St. Petersburg paradox cite this when bounding expected log utility before taking the limit. It is a direct summation definition that instantiates the per-term logTerm over the initial segment of natural numbers.
Claim. Let $U_N = sum_{n=1}^N n / 2^n$. This is the unitless partial sum for log utility in the St. Petersburg game, where outcome n has probability (1/2)^n and payout 2^n.
background
In the St. Petersburg module a fair coin is flipped until the first heads on flip n, producing payout 2^n with probability (1/2)^n. The per-outcome log-utility term is supplied by the upstream logTerm definition: logTerm n := n / 2^n. The partial sum aggregates these terms from n=1 to N using standard Finset summation over the half-open interval Ico 1 (N+1).
proof idea
One-line definition that applies the summation operator directly to logTerm n over Finset.Ico 1 (N+1).
why it matters
This partial sum is the common building block for the downstream convergence theorems logUtility_converges, logUtility_limit_eq_two, and logUtilityPartial_closed_form. It supplies the finite approximants that remain bounded by 2 and approach the limit value 2, thereby establishing the log-utility resolution of the St. Petersburg paradox inside the module. The construction aligns with the J-cost-shaped treatment of utility in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.