logUtilityPartial_mono
plain-language theorem explainer
The partial sums of the per-outcome log-utility terms n/2^n in the St. Petersburg game increase with the cutoff N. Decision theorists using logarithmic utility to resolve the paradox cite this to guarantee the expected utility is well-defined and bounded. The proof applies a general sum-monotonicity lemma for non-negative terms over an expanding index set, using the successor inequality on natural numbers.
Claim. Let $s(N) := ∑_{n=1}^N n/2^n$. If $N_1 ≤ N_2$, then $s(N_1) ≤ s(N_2)$.
background
In the St. Petersburg setup a fair coin is flipped until the first heads on flip n, yielding payout 2^n with probability 2^{-n}. The per-outcome log-utility term is n/2^n and the partial sum aggregates these contributions from n=1 to N. The module establishes the classical divergence of linear expected value against convergence under log utility. The result rests on the explicit definition of the partial sum and the arithmetic fact that successor preserves order.
proof idea
Introduce N1 and N2 with N1 ≤ N2. Unfold both partial sums and apply the Finset lemma that sums over a subset are bounded above by the full sum when every term is nonnegative. The subset relation on Ico intervals follows by rewriting membership and invoking the successor inequality. Nonnegativity of each term n/2^n is immediate from the cast of n and positivity of powers of 2.
why it matters
This monotonicity feeds the master certificate that assembles linear divergence and log convergence. It supplies the monotonicity half needed to invoke the bounded-monotone-sequence theorem for existence of the log-utility limit. In the Recognition framework the result supports the log-shaped resolution of the paradox, consistent with J-cost and the phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.