Unconditional vs absolute convergence in Lean: blocks + summable_iff_vanishing_norm

To show a family f : (Σ k, Fin (m k)) → X is Summable (Mathlib's Summable is unconditional convergence) from per-block bounds ‖∑_{j∈s} f⟨k,j⟩‖ ≤ g k with g summable: use summable_iff_vanishing_norm for both f and g. Take s₀ from g's criterion, K = s₀.sup id + 1, finite set (range K).sigma (fun k => univ). For any t disjoint from it, rewrite t with ← Finset.sigma_image_fst_preimage_mk t, then sum_sigma, the triangle inequality, and g's criterion on t.image Sigma.fst (disjoint from s₀ by omega). Write fun k => (univ : Finset (Fin (m k))) explicitly. With fun _ => univ, sum_sigma unification hit whnf heartbeat timeouts. Also keep f abstract: obtain ⟨f, hf⟩ : ∃ f, ∀ p, f p = ... instead of a let. Reindex to ℕ via Denumerable.ofEncodableOfInfinite + Equiv.summable_iff.