prob_pos
plain-language theorem explainer
Probability positivity for each outcome n in the St. Petersburg ensemble is established for all natural numbers. Researchers constructing probability distributions for variational free energy and Bayesian filtering cite it to guarantee valid measures. The term proof unfolds the geometric definition of prob and applies the positivity tactic.
Claim. For every natural number $n$, $0 < (1/2)^n$.
background
The St. Petersburg module models a fair coin flipped until the first heads on trial n, with payout defined as $2^n$ and probability defined as $(1/2)^n$. The upstream payout definition sets the reward on outcome n to $2^n$, while the prob definition sets the weight to $(1/2)^n$. This positivity result supplies the strict inequality required by the ProbDist structure, which demands a positive function summing to one.
proof idea
The proof is a term-mode one-liner: it unfolds prob and invokes the positivity tactic.
why it matters
The result feeds into bayesStep, evidence_pos, boltzmannDist, boltzmann_minimizes_vfe, kl_nonneg, and ProbDist in the statistics modules. It supports the decision track by supplying a well-defined probability measure before the analysis of linear divergence versus log convergence in the St. Petersburg paradox. This aligns with the framework's use of positive probabilities in RCL-derived free-energy calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.