stayWinningSet
plain-language theorem explainer
stayWinningSet collects the outcomes in the Monty Hall sample space where the initial pick equals the prize location. Probability researchers cite this set when establishing the stay strategy succeeds with probability 1/3 via direct cardinality computation on the nine-element space. It is defined by filtering the full outcome set with the StayWins predicate.
Claim. Let $Ω := Fin 3 × Fin 3$ be the joint sample space of (prize location, player pick). The stay-winning set is the subset $S = {ω ∈ Ω | ω₂ = ω₁}$.
background
The module models Monty Hall on the sample space Ω = Fin 3 × Fin 3 with nine equally likely outcomes. Outcome is the type of pairs (prize, pick). StayWins holds precisely when the second component equals the first, i.e., the player initially picked the prize door. The uniform measure assigns each outcome weight 1/9. Stay wins on the diagonal (three outcomes); switch wins on the off-diagonal (six outcomes). The host always reveals a goat, but this does not alter the win counts for either strategy.
proof idea
One-line definition that applies Finset.univ.filter to the StayWins predicate.
why it matters
This definition supplies the concrete stay-winning set used by MontyHallCert and monty_hall_one_statement to certify p_stay = 1/3 and p_switch = 2/3 by cardinality. It replaces the earlier placeholder probabilities with an explicit outcome-counting derivation on Fin 3 × Fin 3, completing the Decision track E6 argument that the switch strategy is strictly superior under the uniform measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.