Commit 2026-03-17 19:12 5160b96e

feat(Mathlib/Analysis/Asymptotics/Defs): congr lemmas for IsBigO* (#35745) This PR primarily provides two calculational lemmas that are commonly used in bounding functions. First, it provides IsBigO*.sum_congr. This theorem allows the user to bound each term of a (finite) sum individually. This is different than IsBigO.sum which requires all terms to be bound by the same function. Second, it provides IsBigO*.sum_congr'. This theorem allows the user to bound the terms of a sum individually when the length of the sum changes with respect to the running variable. This is a common setup with certain techniques such as the method of the hyperbola. Note: This makes the overall length of this file go above 1500 lines. I'm happy to break it up at the request of reviewers, but that's a bigger change to the API. AI Usage: Looking up various lemma names in Google Gemini.