lean_workbook_plus_29673
ProvedNow in order to find the expected number of moves before we hit our first barrier, we get the same equations as before,except as well, so by symmetry, we know that which makes the system much easier to solve, reducing it to the following equations: \begin{align*} E_0 &=\frac{E_{-1}+E_1}{2}+1=E_1+1\ E_1 &=\frac{7}{8}E_0+7\end{align*} and receive , meaning that the expected number of moves to hit the first barrier from zero is 64, so in total, the expected number of moves to hit both barriers is .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_29673 (e : ℤ → ℝ) (h₀ : ∀ n, e (-n) = e n) (h₁ : e 0 = (e (-1) + e 1) / 2 + 1) (h₂ : e 1 = 7 / 8 * e 0 + 7) : e 0 = 64 := by sorry
Source