module
public import Mathlib.Data.Real.Basic
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.Ring
public section
/-!
# USA Mathematical Olympiad 1974, Problem 4
A, B, C play a series of games. Each game is between two players.
The next game is between the winner and the person who was not playing.
The series continues until one player has won two games. He wins the series.
A is the weakest player, C the strongest. Each player has a fixed probability
of winning against a given opponent. A chooses who plays the first game.
Show that he should choose to play himself against B.
-/
namespace Usa1974P4
/-- The three players of the series. -/
inductive Player | A | B | C
deriving DecidableEq
/-- The player who sits out a game between `x` and `y`.
Only meaningful for `x ≠ y`; returns `A` on the diagonal. -/
def third : Player → Player → Player
| .A, .B => .C
| .B, .A => .C
| .A, .C => .B
| .C, .A => .B
| .B, .C => .A
| .C, .B => .A
| _, _ => .A
/-- The probability that player `A` wins the series, where
* `win x y` is the probability that `x` beats `y` in a single game,
* the next game is played between `w` (the winner of the previous game)
and `i` (the player who sat out the previous game); the loser of a game
sits out the next one,
* `hist` is the list of winners of the games played so far, and
* `n` is a fuel bounding the number of games still to be played.
The series ends as soon as some player has won two games in total, so it
lasts at most four games: if no one has won twice after three games then the
three winners so far are three distinct players, and the fourth game is played
between two of them, so its winner reaches two wins. -/
def probWinA (win : Player → Player → ℝ) :
ℕ → Player → Player → List Player → ℝ
| 0, _, _, _ => 0
| n + 1, w, i, hist =>
win w i * (if w ∈ hist then (if w = .A then 1 else 0)
else probWinA win n w (third w i) (w :: hist)) +
win i w * (if i ∈ hist then (if i = .A then 1 else 0)
else probWinA win n i (third w i) (i :: hist))
/-- The probability that A wins the series when the first game is A against B. -/
def probFirstAB (win : Player → Player → ℝ) : ℝ := probWinA win 4 .A .B []
/-- The probability that A wins the series when the first game is A against C. -/
def probFirstAC (win : Player → Player → ℝ) : ℝ := probWinA win 4 .A .C []
/-- The probability that A wins the series when the first game is B against C. -/
def probFirstBC (win : Player → Player → ℝ) : ℝ := probWinA win 4 .B .C []
theorem usa1974_p4
(win : Player → Player → ℝ)
(hwin : ∀ x y : Player, x ≠ y → 0 < win x y ∧ win x y + win y x = 1)
-- "A is the weakest player, C the strongest"; the proof only uses that A is
-- more likely to beat B than to beat C.
(hweak : win Player.A Player.C < win Player.A Player.B) :
probFirstBC win < probFirstAB win ∧ probFirstAC win < probFirstAB win := sorry
end Usa1974P4
This problem has a complete formalized solution.