lean_workbook_plus_57364
ProvedDefine to be the probability that the ant stays on the same side after more moves if the previous move stayed on the same side (top or bottom). Define to be the probability that the ant stays on the same side after more moves if the previous move switched between top and bottom. After switching sides, the next move cannot, so . We also have the recursion since with one-half probability it stays on the same side and with one-half probability, it switches sides and the probability that we return to the original is . \n\n We wish to compute . It is easy to see that and . \n\n Now, using the recursion we compute \n\n \begin{tabular}{c | c} n & P_n \ 1 & \frac 12 \ 2 & \frac 14 \ 3 & \frac 38 \ 4 & \frac{9}{16} \ 5 & \frac{19}{32} \ 6 & \frac{33}{64} \ 7 & \frac{59}{128} \ \end{tabular} \n\n at which point it is easy to compute
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_57364 (p q : ℕ → ℚ) (h₀ : p 1 = 1 / 2) (h₁ : p 2 = 1 / 4) (h₂ : ∀ n, p (n + 2) = 1 / 2 * p (n + 1) + 1 / 2 * (1 - p n)) (h₃ : ∀ n, q (n + 1) = p n) (h₄ : 0 < 7) : (2 / 3 * (1 - p 7) + 1 / 3 * q 7) = 17 / 32 := by sorry