linearUtilityPartial_eq
plain-language theorem explainer
The partial sum of linear expected payouts over the first N outcomes in the St. Petersburg game equals N exactly. Decision theorists resolving the St. Petersburg paradox cite this closed form to establish that linear utility is unbounded. The proof unfolds the partial-sum definition, replaces every summand by 1 using the per-term identity, and reduces the result to the cardinality of the index interval.
Claim. For each natural number $N$, let $p(n) = 2^{-n}$ and $x(n) = 2^n$. Then the partial sum satisfies $S_N = N$, where $S_N = sum_{n=1}^N p(n) x(n)$.
background
The St. Petersburg module constructs the ensemble with outcomes indexed by $n geq 1$, probability $(1/2)^n$, and payout $2^n$. linearUtilityPartial is the finite sum over the interval Ico 1 (N+1) of prob n times payout n. The upstream linear_term lemma states that each such product equals 1. This sits inside the module's treatment of the classical paradox, where linear utility is shown to diverge while log utility converges to a bound of 2.
proof idea
The term-mode proof unfolds linearUtilityPartial, invokes sum_congr with the linear_term identity to turn every summand into 1, applies sum_const, replaces the sum by the cardinality of Ico 1 (N+1) via Nat.card_Ico, and finishes with simp.
why it matters
linearUtilityPartial_eq supplies the closed form required by linearUtility_diverges (which shows the partial sums are unbounded) and by stPetersburgCert (the master certificate for the full resolution). It completes the linear half of st_petersburg_one_statement, which contrasts divergence under linear utility with the bounded log-utility sums that align with J-cost. The result therefore anchors the Recognition Science claim that linear utility fails to resolve the paradox.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.