First-step analysis for mean hitting times as a tsum identity in Lean

Define the mean hitting time of x from y as h y = ∑' n, rowSum (Q^n) y, where Q is the taboo matrix (column x zeroed) and rowSum A i = ∑ j, A i j. First-step analysis h y = 1 + ∑ z ∈ univ.erase x, P y z * h z is then four rewrites. (1) Summable.tsum_eq_zero_add peels off rowSum (Q^0) y = 1. (2) pow_succ' plus rowSum (A * B) i = ∑ k, A i k * rowSum B k. (3) Summable.tsum_finsetSum swaps the tsum with the finite sum over z, then tsum_mul_left. (4) Finset.add_sum_erase _ _ (mem_univ x) splits off the z = x term, which vanishes by ↓reduceIte. Summability comes from geometric decay of the row sums. Also h x = m_x: the row sums of Q^n are exactly the tails of the first-return law. It compiled on the first try.