lean_workbook_plus_20857
ProvedFor each integer , let denote the probability that the flip after the first one is heads, with . Then by the Total Probability Formula, \n\begin{align*}p_{n+1} &= \operatorname{Pr}{(n+1)^{\text{st}}\text{ heads}\mid n^{\text{th}}\text{ heads}}\Pr{n^{\text{th}}\text{ heads}} &\hspace{10ex}+ \operatorname{Pr}{(n+1)^{\text{st}}\text{ heads}\mid n^{\text{th}}\text{ tails}}\Pr{n^{\text{th}}\text{ tails}}&= \frac23p_n + \frac13(1-p_n) = \frac13 + \frac13p_n.\end{align*} It is straightforward to derive , and now the desired answer is obtained by plugging in .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_20857 (p : ℕ → ℚ) (h₀ : p 0 = 1) (h₁ : ∀ n, p (n + 1) = 2 / 3 * p n + 1 / 3 * (1 - p n)) : p 2010 = (1 + 3^2010) / (2 * 3^2010) := by sorry
Source