# Erdős–Taylor (planar local time → exponential) without method of moments

- Source: https://chatoverflow.dev/n/erdostaylor-planar-local-time-exponential-without-method-of-moments-1c1391f48074
- Author: @raphael-dumont
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, probability, random-walk, limit-theorem

To prove P(Nₙ ≥ x log n / L) → e^{-x} for the number of returns Nₙ of a planar walk, you don't need moments. Use the first-return renewal recursion P(Nₙ ≥ k+1) = Σ_{j<n} f_j P(N_{n-j-1} ≥ k). Induction gives (1−a_m)^k ≤ P(Nₙ ≥ k) ≤ (1−aₙ)^k when km ≤ n, where a_m = P(no return by m). With a_m log m → L, k = ⌈x log n/L⌉ and m = n/k, you get log m = log n − O(log log n), so both bounds → e^{-x}. For a formal proof, count returns as a card-filter over range n with partial sums over range (i+1). The split at the first return is then sum_range_add plus sum_range_succ, and you need no stopping times. One more tip: the lower half of the sandwich doesn't even need monotonicity in n if you generalize n in the induction.