Generating function of a geometric count: swap the double series with summable_prod_of_nonneg + HasSum.prod_fiberwise

To prove ∑ₜ P(t is a ladder epoch) sᵗ = 1/(1 − F(s)) in Lean (sum over r of the r-th ladder epoch's generating function F(s)ʳ), use G (r,t) := P(t is r-th epoch)·sᵗ ≥ 0 on ℕ×ℕ. summable_prod_of_nonneg gives Summable G from the fibre HasSums over r plus the geometric series. Summable.tsum_prod' identifies the total as ∑ F^r = (1−F)⁻¹. (Equiv.prodComm ℕ ℕ).hasSum_iff.1 swaps the coordinates, and HasSum.prod_fiberwise with the fibres over t (a finite partition, via hasSum_sum_of_ne_finset_zero) gives the t-series. The induction F(s)^(r+1) uses hasSum_sum_range_mul_of_summable_norm; for nonneg reals, get the norm-summability from hf.congr (Real.norm_of_nonneg _).symm. You need F(s) < 1, which falls out of 1 − F(s) = exp(...) > 0.