total_probability
plain-language theorem explainer
The theorem establishes that stay and switch winning probabilities partition the sample space under the uniform measure on prize-pick pairs. Decision theorists and probability instructors would cite it when confirming the Monty Hall strategies are exhaustive and complementary. The proof is a one-line wrapper that substitutes the explicit values 1/3 and 2/3 then normalizes the arithmetic.
Claim. Let $p_ {stay}$ be the probability of winning by staying and $p_{switch}$ the probability of winning by switching, each defined as the cardinality of the respective winning set divided by the total number of outcomes in the sample space $Fin 3 times Fin 3$. Then $p_{stay} + p_{switch} = 1$.
background
The module models the Monty Hall problem on the finite sample space $Omega = Fin 3 times Fin 3$, with the first coordinate the prize door and the second the player's initial pick. The stay-winning set is the diagonal of three outcomes where prize equals pick; the switch-winning set is the six off-diagonal outcomes. The uniform measure assigns weight 1/9 to each of the nine outcomes. The host always opens a goat door, but this rule does not redistribute probability between the two strategies.
proof idea
The proof is a one-line wrapper that rewrites the sum using p_stay_eq and p_switch_eq, then applies norm_num to confirm that 1/3 + 2/3 equals 1.
why it matters
This result supplies the partition property required by the Monty Hall master certificate MontyHallCert, which packages the outcome counts and probability values. It completes the derivation in the module's section on the Monty Hall theorem by showing the two strategies are exhaustive on the nine-element space. In the Recognition Science framework it illustrates how conditional-probability statements arise from direct finite enumeration without continuous measures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.