logUtilityPartial_zero
plain-language theorem explainer
The theorem asserts that the partial sum of log-utility terms in the St. Petersburg game equals zero for the empty case N=0. Decision theorists resolving the paradox via logarithmic utility cite this base case when inducting toward the closed-form expression. The proof is a direct term-mode reduction that unfolds the summation definition and simplifies the empty range to zero.
Claim. Let $S(N)$ denote the partial sum of logarithmic utility terms $S(N) = ∑_{n=1}^{N} logTerm(n)$. Then $S(0) = 0$.
background
The St. Petersburg module constructs the game with outcomes indexed by n=1,2,... having probability (1/2)^n and payout 2^n. Linear utility partial sums grow unbounded as N while log utility converges. The upstream definition states: 'The unitless log-utility partial sum from n = 1 to n = N' and gives logUtilityPartial N := ∑ n ∈ Finset.Ico 1 (N+1), logTerm n. This theorem supplies the N=0 base case where the summation range is empty.
proof idea
The proof is a one-line wrapper that unfolds logUtilityPartial to the summation over the empty interval Finset.Ico 1 1 and applies simp to reduce the empty sum to zero.
why it matters
This base case feeds the induction in logUtilityPartial_closed_form, which derives the closed form 2 - (N+2)/2^N and the limit 2 as N→∞. The result supports the log-utility resolution of the St. Petersburg paradox, aligning with the J-cost framework where logarithmic utility yields a convergent expectation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.