`switchWinningSet_card`

proved

show as: view math explainer →

module: IndisputableMonolith.Decision.MontyHall
domain: Decision
line: 130 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Decision.MontyHall on GitHub at line 130.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 127  decide
 128
 129/-- The off-diagonal has cardinality 6 (= 9 − 3). -/
 130theorem switchWinningSet_card : switchWinningSet.card = 6 := by
 131  decide
 132
 133/-! ## §4. Probabilities under the uniform measure -/
 134
 135/-- The probability of a stay-win under the uniform measure on
 136`Fin 3 × Fin 3`. -/
 137def p_stay : ℚ := stayWinningSet.card / (Finset.univ : Finset Outcome).card
 138
 139/-- The probability of a switch-win under the uniform measure. -/
 140def p_switch : ℚ := switchWinningSet.card / (Finset.univ : Finset Outcome).card
 141
 142/-- **STAY-WINS-WITH-PROBABILITY-1/3.** -/
 143theorem p_stay_eq : p_stay = 1 / 3 := by
 144  unfold p_stay
 145  rw [stayWinningSet_card, outcome_count]
 146  norm_num
 147
 148/-- **SWITCH-WINS-WITH-PROBABILITY-2/3.** -/
 149theorem p_switch_eq : p_switch = 2 / 3 := by
 150  unfold p_switch
 151  rw [switchWinningSet_card, outcome_count]
 152  norm_num
 153
 154/-! ## §5. The Monty Hall theorem -/
 155
 156/-- **MONTY HALL THEOREM (counting form).** Switching strictly beats
 157staying: the switch strategy wins on twice as many outcomes as the
 158stay strategy. -/
 159theorem switch_strictly_better : p_stay < p_switch := by
 160  rw [p_stay_eq, p_switch_eq]

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.