Documentation

LeanPool.LeanModularForms.ForMathlib.Hassumunifon

HasSumUniformlyOn / cotTerm scratch file #

This file was an early scratch pad where Chris Birkbeck staged a long sequence of helper lemmas en route to results on HasSumUniformlyOn and on the cotangent product expansion. Almost every lemma here has since been upstreamed (under the same or a slightly different name) into Mathlib (Mathlib.Analysis.Series.LocallyUniform, Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent, Mathlib.Analysis.Complex.LocallyUniformLimit, etc.). The remaining purely-local helpers were not imported by any other file in this project, so we retire this file as a stub. The original lemmas remain in git history for reference.