switchWinningSet

formal source

 101  unfold SwitchWins; infer_instance
 102
 103/-- The set of switch-winning outcomes. -/
 104def switchWinningSet : Finset Outcome :=
 105  Finset.univ.filter (fun ω => SwitchWins ω)
 106
 107/-! ## §2. The two outcome sets are complementary -/
 108
 109/-- Every outcome either wins by staying or wins by switching. -/
 110theorem stay_or_switch (ω : Outcome) : StayWins ω ∨ SwitchWins ω := by
 111  unfold StayWins SwitchWins
 112  by_cases h : ω.2 = ω.1
 113  · exact Or.inl h
 114  · exact Or.inr h
 115
 116/-- No outcome wins by both. -/
 117theorem not_both (ω : Outcome) : ¬ (StayWins ω ∧ SwitchWins ω) := by
 118  unfold StayWins SwitchWins
 119  rintro ⟨h₁, h₂⟩
 120  exact h₂ h₁
 121
 122/-! ## §3. Counting the outcome sets -/
 123
 124/-- The diagonal of `Fin 3 × Fin 3` has cardinality 3. -/
 125theorem stayWinningSet_card : stayWinningSet.card = 3 := by
 126  -- Compute by `decide`: the filter is a concrete subset of a concrete finite type.
 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