linearUtilityPartial_mono
plain-language theorem explainer
The partial sum of expected linear utility in the St. Petersburg game is non-decreasing in the truncation level N. Decision theorists examining the classical paradox would cite this to confirm that the truncated expectation equals N and therefore grows unbounded. The proof is a one-line wrapper that rewrites both sides to the closed form N via the equality lemma and casts the order hypothesis.
Claim. The function $Nmapsto sum_{n=1}^N (1/2)^n cdot 2^n$ is monotone non-decreasing.
background
In the St. Petersburg module the ensemble consists of outcomes indexed by n greater than or equal to 1, each with probability (1/2)^n and payout 2^n. The linear partial sum is defined as the finite expectation sum from n=1 to N of prob(n) times payout(n). Upstream results establish that this sum equals N exactly, obtained by unfolding the definition and replacing each term by the identity prob(n) payout(n) equals 1.
proof idea
The proof is a one-line wrapper. It introduces the hypothesis N1 less than or equal to N2, rewrites both linearUtilityPartial applications using the closed-form equality lemma, and concludes by exact_mod_cast on the resulting numerical inequality.
why it matters
This monotonicity underpins the divergence of linear utility in the St. Petersburg setting, showing that partial sums increase without bound and therefore the infinite expectation is infinite. It belongs to the decision-theoretic track that contrasts linear divergence with logarithmic convergence, consistent with the module's replacement of earlier marginal-utility placeholders. The result feeds the sibling divergence statement that passes the partial-sum equality to the limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.