Commit 2024-01-27 17:46 e4e10f95

feat(Topology/Algebra/InfiniteSum/Basic): add some lemmas on tsums (#10038) This is the fifth PR in a sequence that adds auxiliary lemmas from the EulerProducts project to Mathlib. It adds three lemmas on tsums:

lemma HasSum.tsum_fiberwise {α β γ : Type*} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α]
    [T2Space α] [RegularSpace α] [CompleteSpace α] {f : β → α}
    {a : α} (hf : HasSum f a) (g : β → γ) :
    HasSum (fun c : γ ↦ ∑' b : g ⁻¹' {c}, f b) a
lemma tsum_setProd_singleton_left {α β γ : Type*} [AddCommMonoid γ] [TopologicalSpace γ] [T2Space γ]
    (a : α) (t : Set β) (f : α × β → γ) : (∑' x : {a} ×ˢ t, f x) = ∑' b : t, f (a, b)
lemma tsum_setProd_singleton_right {α β γ : Type*} [AddCommMonoid γ] [TopologicalSpace γ] [T2Space γ]
    (s : Set α) (b : β) (f : α × β → γ) : (∑' x : s ×ˢ {b}, f x) = ∑' a : s, f (a, b)

and the necessary equivalences

def prod_singleton_left {α β : Type*} (a : α) (t : Set β) : ↑({a} ×ˢ t) ≃ ↑t
def prod_singleton_right {α β : Type*} (s : Set α) (b : β) : ↑(s ×ˢ {b}) ≃ ↑s