Commit 2025-04-22 05:41 4724f11f

feat(Analysis/SpecialFunctions): multipliability lemmas (#23768) Prove that in any complete normed ring, a product ∏' i, (1 + f i) is convergent if the sum of real numbers ∑' i, ‖f i‖ is convergent.
As part of this, move some lemmas about summability of logs out of SpecialFunctions.Log to Log.Summable and rework results in the latter file to minimize non-vanishing / positivity conditions.