prob_zero
plain-language theorem explainer
The probability of the zeroth outcome equals one under the geometric distribution for the St. Petersburg ensemble. Decision theorists analyzing partial sums for the paradox would cite this identity as the base case when building expectations. The proof is a one-line wrapper that unfolds the definition of prob and simplifies the power.
Claim. Let $p : ℕ → ℝ$ be given by $p(n) = (1/2)^n$. Then $p(0) = 1$.
background
The St. Petersburg module constructs an ensemble in which a fair coin is flipped until the first heads on flip $n ≥ 1$, yielding payout $2^n$ with probability $(1/2)^n$. The function prob is defined directly as prob(n) := (1/2)^n. The accompanying convention uses the 1-indexed range Finset.Ico 1 (N+1) for partial sums over the first N outcomes, so the n=0 case supplies the empty-product identity 1.
proof idea
The proof is a one-line wrapper that unfolds the definition of prob and simplifies the resulting expression.
why it matters
This identity supplies the base case for the partial-sum arguments that establish divergence of linear utility and convergence of log utility. It anchors the module's proofs of linearUtility_diverges and logUtilityPartial_zero. Within the Recognition framework it provides the probabilistic starting point for the decision-theoretic track that contrasts linear and J-cost-shaped utilities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.