lean_workbook_plus_65724
ProvedLet be the expected number of white balls left after all black balls get chosen, starting with white and black balls. Then , and . This lets us compute as many values as we like, in particular . If we look at a few computed values, it also lets us conjecture that , which then follows immediately from the recursion by induction.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_65724 (f : ℕ → ℕ → ℝ) (h₀ : ∀ b, f 0 b = 0) (h₁ : ∀ a, f a 0 = a) (h₂ : ∀ a b, (a + b) * f a b = a * f (a - 1) b + b * f a (b - 1)) : f 15 10 = 15 / 11 := by sorry
Source