3. World 3: Counting🔗

Throw n coins and count how often true comes up: that is the binomial distribution B(n, p), with P(k) = \binom{n}{k} p^k (1 - p)^{n - k}. In Lean it is binom p n. In world 2 you built B(2, p) from two coins; from the third level on it is a building block of its own.

Wirf n Münzen und zähle, wie oft true kommt: Das ist die Binomialverteilung B(n, p), mit P(k) = \binom{n}{k} p^k (1 - p)^{n - k}. In Lean heißt sie binom p n. In Welt 2 hast du B(2, p) aus zwei Münzen gebaut; ab dem dritten Level ist sie ein eigener Baustein.

Three coins. Count the trues among three coins.

Drei Münzen. Zähle die true unter drei Münzen.

Three throws are binom p 3. New: add_assoc : a + b + c = a + (b + c).

Tip. As in world 2, level 6, and add_assoc in the simp only.

Drei Würfe sind binom p 3. Neu: add_assoc : a + b + c = a + (b + c).

Tipp. Wie in Welt 2, Level 6, und add_assoc im simp only.

B(1, p). One throw, counted: a coin as a number.

B(1, p). Ein Wurf, gezählt: eine Münze als Zahl.

One coin as a number is B(1, p). The lemma you prove here is called binom_one; from the next level on it is in your inventory. New: map_eq_pure_bind : f <$> μ = do let x ← μ; pure (f x).

Tip. rw [binom_succ, binom_zero], simp only [pure_bind, add_zero], rw [map_eq_pure_bind].

Eine Münze als Zahl ist B(1, p). Das Lemma, das du hier beweist, heißt binom_one; ab dem nächsten Level ist es in deinem Inventar. Neu: map_eq_pure_bind : f <$> μ = do let x ← μ; pure (f x).

Tipp. rw [binom_succ, binom_zero], simp only [pure_bind, add_zero], rw [map_eq_pure_bind].

A new building block. B(2, p) and one more coin give B(3, p): one more throw, one more chance to count.

Ein neuer Baustein. B(2, p) und eine weitere Münze ergeben B(3, p): ein Wurf mehr, eine Chance mehr zu zählen.

binom_succ throws the new coin first; here it comes last, for every n. That needs induction, as in the Natural Number Game: induction' n with n ih leaves two goals, one after the other: the case 0, and the case n + 1, with the hypothesis ih for n. Rules can be given their arguments: binom_succ p n is the rule for this n only. New: zero_add : 0 + n = n. The lemma is called binom_succ'.

Tip. Case 0: rw [binom_zero, binom_succ, binom_zero], simp only [pure_bind, zero_add, add_zero]. Case n + 1: rw [binom_succ p n, binom_succ p (n + 1), ← ih], simp only [bind_assoc, pure_bind, add_assoc].

binom_succ wirft die neue Münze zuerst; hier kommt sie zuletzt, für jedes n. Dafür braucht es Induktion, wie im Natural Number Game: induction' n with n ih lässt zwei Ziele, eines nach dem anderen: den Fall 0, und den Fall n + 1, mit der Annahme ih für n. Regeln kann man ihre Argumente mitgeben: binom_succ p n ist die Regel nur für dieses n. Neu: zero_add : 0 + n = n. Das Lemma heißt binom_succ'.

Tipp. Fall 0: rw [binom_zero, binom_succ, binom_zero], simp only [pure_bind, zero_add, add_zero]. Fall n + 1: rw [binom_succ p n, binom_succ p (n + 1), ← ih], simp only [bind_assoc, pure_bind, add_assoc].

At least one true, as in world 2, but this time from B(2, p): when is a number at least 1?

Mindestens einmal true, wie in Welt 2, aber diesmal aus B(2, p): Wann ist eine Zahl mindestens 1?

At least 1 out of B(2, p) is: at least one of two coins.

Tip. As in the boss of world 2: unfold, clean up, go under the throws, four cases.

Mindestens 1 aus B(2, p) heißt: mindestens eine von zwei Münzen.

Tipp. Wie beim Endgegner von Welt 2: auswickeln, aufräumen, unter die Würfe gehen, vier Fälle.

Boss: B(2, p) * B(2, p) = B(4, p). Two independent binomials, no coins. The sum of independent random numbers has the convolution * of their distributions as its distribution. In Lean, (do let X ← binom p 2; let Y ← binom p 2; return X + Y) = binom p 4, for every p: a case of the lemma binom_add.

Endgegner: B(2, p) * B(2, p) = B(4, p). Zwei unabhängige Binomialverteilungen, keine Münzen. Die Summe unabhängiger Zufallszahlen hat die Faltung * ihrer Verteilungen als Verteilung. In Lean: (do let X ← binom p 2; let Y ← binom p 2; return X + Y) = binom p 4, für jedes p, ein Fall des Lemmas binom_add.

Boss. On the board it was B(2, p) * B(2, p) = B(4, p); here it is for all n and m: the sum of independent binomials is binomial. New: bind_pure : (do let x ← μ; pure x) = μ.

Tip. Induction on m. Case 0: rw [binom_zero], simp only [pure_bind, add_zero, bind_pure]. Case m + 1: write binom p (m + 1) with ← binom_succ' p m, then n + (m + 1) as n + m + 1 (← add_assoc) and that again with ← binom_succ' p (n + m); now ← ih, and clean up with simp only [bind_assoc, pure_bind, add_assoc].

Endgegner. Auf dem Spielfeld war es B(2, p) * B(2, p) = B(4, p); hier gilt es für alle n und m: Die Summe unabhängiger Binomialverteilungen ist binomial. Neu: bind_pure : (do let x ← μ; pure x) = μ.

Tipp. Induktion nach m. Fall 0: rw [binom_zero], simp only [pure_bind, add_zero, bind_pure]. Fall m + 1: schreibe binom p (m + 1) mit ← binom_succ' p m um, dann n + (m + 1) als n + m + 1 (← add_assoc) und das wieder mit ← binom_succ' p (n + m); jetzt ← ih, und räume auf mit simp only [bind_assoc, pure_bind, add_assoc].