Trocq summable — summability transfers across an equivalence

Trocq's summable example transfers summability across a change of index type. The paradigm case: a type equivalence e : α ≃ β transfers Summable in both directions (Equiv.summable_iff), because reindexing a sum by a bijection preserves it. This is the analytic counterpart of the engine's representation transfers — a statement moved across an equivalence — for a noncomputable, topological predicate.

theorem Transfer.Examples.Trocq.Summable.summable_transfer {α β M : Type} [AddCommMonoid M] [TopologicalSpace M] (e : α ≃ β) (f : β → M) : Summable (f ∘ ⇑e) ↔ Summable f

Summability transfers across a reindexing bijection. For any equivalence of index types, a family is summable after reindexing iff it was summable.