Skip to content

Instantly share code, notes, and snippets.

@llllvvuu
Last active March 23, 2024 02:59
Show Gist options
  • Save llllvvuu/02e08ee87b2191c0f3f504072be73a0f to your computer and use it in GitHub Desktop.
Save llllvvuu/02e08ee87b2191c0f3f504072be73a0f to your computer and use it in GitHub Desktop.

Problem: https://twitter.com/littmath/status/1769044719034647001

Flip a fair coin 100 times—it gives a sequence of heads (H) and tails (T). For each HH in the sequence of flips, Alice gets a point; for each HT, Bob does, so e.g. for the sequence THHHT Alice gets 2 points and Bob gets 1 point. Who is most likely to win?

Proofs:

  1. https://twitter.com/llllvvuu/status/1769629337953923403
  2. https://x.com/alexselby1770/status/1769795987344638033
  3. https://twitter.com/RadishHarmers/status/1770217473716932647
  4. https://x.com/RadishHarmers/status/1771368007174168604?s=20

Generating Functions

Extension of: https://x.com/alexselby1770/status/1770269732588888466

Number of games Bob wins

$$f(x) = \dfrac{x\left(1 + x + 2x^2 + (x - 1)\sqrt{1 + \frac{4x^3}{x - 1}}\right)}{2 (x - 1)^2\left(1 + \frac{4x^3}{x - 1}\right)}$$

  • TODO: Rewrite as quadratic equation
  • TODO: Substitute $f(x) = \sum a_n x^n$ into quadratic equation and derive linear recurrence relation for $a_n$ by aligning coefficients of $x^n$

Number of games Alice wins

$$f(x) = \dfrac{(x + 1) \sqrt{1 + \frac{4x^3}{x - 1}} - 2 x^2 - x - 1}{2 (x - 1)\left(1 + \frac{4x^3}{x - 1}\right)}$$

  • TODO: Rewrite as quadratic equation
  • TODO: Substitute $f(x) = \sum a_n x^n$ into quadratic equation and derive linear recurrence relation for $a_n$ by aligning coefficients of $x^n$

Number of more games Bob wins

$$f(x) = \dfrac{\left(1+\frac{4x^3}{x-1}\right)^{-\frac{1}{2}} - 1}{2(1 - x)}$$

$$(4x^3 + x - 1)(1 - x)^2 f(x)^2 + (4x^3 + x - 1)(1 - x)f(x) + x^3 = 0$$

  • TODO: Substitute $f(x) = \sum a_n x^n$ and derive linear recurrence relation for $a_n$ by aligning coefficients of $x^n$

Number of games tied

$$f(x) = \dfrac{(1 + 2 x)\left(1 + \frac{4 x^3}{x - 1}\right)^{-\frac{1}{2}} + 1}{2 (1 - x)}$$

$$(-1 + x)^2 (-1 + x + 4 x^3) f(x)^2 + (-1 + x) (-1 + 2 x) (1 + x + 2 x^2) f(x) + x = 0$$

  • TODO: Substitute $f(x) = \sum a_n x^n$ and derive linear recurrence relation for $a_n$ by aligning coefficients of $x^n$

What's incomplete about the "autocorrelation" intuition?

This intuition basically says "Alice has larger average win margins, but total win margin is the same for Alice and Bob, so Alice wins fewer times".

"Alice has larger average win margins" is an unproven conjecture, extrapolated from a few data points (e.g. there are win margins between n/2 and n for Alice, but not for Bob).

It turns out this skew is not really noticeable outside of the tails:

Figure_1

How do we know the center is not skewed the other way? We need an actual proof here.

#include <assert.h>
#include <stdint.h>
#include <stdio.h>
#include <string.h>
#define SWAP(x, y, T) \
do { \
T SWAP = x; \
x = y; \
y = SWAP; \
} while (0)
#define MAX_FLIPS 65
/**
* @param flips - At most 65 due to overflow
* @param[out] alice - Must be allocated at least `flips` `uint64_t`s
* @param[out] bob - Must be allocated at least `flips` `uint64_t`s
* @param[in, out] buf - Must be allocated at least `8 * (flips + 1)` `uint64_t`s.
*/
void count(uint8_t flips, uint64_t *alice, uint64_t *bob, uint64_t *buf) {
assert(flips <= MAX_FLIPS);
flips++; // HACK: bump memory offset
uint64_t *T_prev = &buf[flips], *T = &buf[5 * flips];
uint64_t *H_prev = &buf[3 * flips], *H = &buf[7 * flips];
memset(buf, 0, 8 * flips * sizeof(uint64_t));
*T = 1;
for (uint8_t n = 1; n < flips; n++) {
alice[n - 1] = bob[n - 1] = 0;
SWAP(H_prev, H, uint64_t *);
SWAP(T_prev, T, uint64_t *);
for (int8_t d = -n; d < 0; d++) {
assert(1 - d <= flips); // bounds check
T[d] = T_prev[d] + H_prev[d - 1];
H[d] = T_prev[d] + H_prev[d + 1];
alice[n - 1] += T[d] + H[d];
}
assert(flips > 1); // bounds check
T[0] = T_prev[0] + H_prev[-1];
H[0] = T_prev[0] + H_prev[1];
for (int8_t d = 1; d <= n / 2; d++) {
assert(d + 1 < flips); // bounds check
T[d] = T_prev[d] + H_prev[d - 1];
H[d] = T_prev[d] + H_prev[d + 1];
bob[n - 1] += T[d] + H[d];
}
}
}
int main() {
static uint64_t alice[MAX_FLIPS], bob[MAX_FLIPS], buf[8 * (MAX_FLIPS + 1)];
count(MAX_FLIPS, alice, bob, buf);
for (uint8_t i = 0; i < MAX_FLIPS; i++) {
printf("%2d flips: Bob %24llu - Alice %24llu\n", i + 1, bob[i], alice[i]);
}
return 0;
}
import Mathlib
def alice {n : ℕ} (x : Std.BitVec n.succ) : ℕ :=
Finset.card <| (Finset.range n).filter (fun i ↦ x.getLsb i ∧ x.getLsb i.succ)
def bob {n : ℕ} (x : Std.BitVec n.succ) : ℕ :=
Finset.card <| (Finset.range n).filter (fun i ↦ x.getLsb i ∧ ¬x.getLsb i.succ)
def alice_win {n : ℕ} (x : Std.BitVec n.succ) : Prop :=
bob x < alice x
def alice_win' {n : ℕ} (x : Std.BitVec n.succ) : Prop :=
bob x < alice x ∨ (bob x == alice x ∧ ¬x.getLsb n)
def bob_win {n : ℕ} (x : Std.BitVec n.succ) : Prop :=
alice x < bob x
instance {n : ℕ} (x : Std.BitVec n.succ) : Decidable (alice_win x) := by
unfold alice_win; infer_instance
instance {n : ℕ} (x : Std.BitVec n.succ) : Decidable (alice_win' x) := by
unfold alice_win'; infer_instance
instance {n : ℕ} (x : Std.BitVec n.succ) : Decidable (bob_win x) := by
unfold bob_win; infer_instance
def alice_wins (n : ℕ) : ℕ :=
Finset.card
<| (Finset.range (2 ^ n.succ)).filter
<| (fun i ↦ alice_win (Std.BitVec.ofNat n.succ i))
def alice_wins' (n : ℕ) : ℕ :=
Finset.card
<| (Finset.range (2 ^ n.succ)).filter
<| (fun i ↦ alice_win' (Std.BitVec.ofNat n.succ i))
def bob_wins (n : ℕ) : ℕ :=
Finset.card
<| (Finset.range (2 ^ n.succ)).filter
<| (fun i ↦ bob_win (Std.BitVec.ofNat n.succ i))
#eval (List.range 10).map alice_wins
#eval (List.range 10).map alice_wins'
#eval (List.range 10).map bob_wins
proof_wanted key_lemma (n : ℕ) : alice_wins' n = (bob_wins n).succ
proof_wanted bob_advantage (n : ℕ) : alice_wins n.succ.succ < bob_wins n.succ.succ
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment