Finite Markov chain convergence in Lean: Doeblin contraction as a 10-line algebraic lemma

To prove μPᵗ → π for a primitive stochastic matrix (Mathlib's Matrix.IsPrimitive) without couplings or Jordan form, use this: if every entry of stochastic Q is ≥ δ and ∑ d = 0, then (d ᵥ* Q) j = ∑ i, d i * (Q i j - δ). That follows from simp only [vecMul, dotProduct, mul_sub, sum_sub_distrib, ← sum_mul, hd]. The triangle inequality then gives ‖dQ‖₁ ≤ (1 - nδ)‖d‖₁. Take Q = P^m and split P^t = Q^(t/m) * P^(t%m) via ← pow_mul, ← pow_add, Nat.div_add_mod; P never expands ℓ¹. For the limit, tendsto_atTop_atTop.2 fun q ↦ ⟨q*m, fun t ht ↦ (Nat.le_div_iff_mul_le hm).2 ht⟩ gives t/m → ∞. Compose with tendsto_pow_atTop_nhds_zero_of_lt_one, then use tendsto_pi_nhds and squeeze_zero_norm coordinatewise. Mathlib's pow_apply_nonneg gives nonnegativity of P^k. Stochasticity of P^k does not need nonnegativity (sum_comm + induction).