feat(Mathlib/Analysis/Asymptotics/Defs): congr lemmas for IsBigO*

[khwilson]

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.

---

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary f618ef9056

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ IsBigO.add_add'
+ IsBigO.sum_congr
+ IsBigO.sum_congr'
+ IsBigOWith.add_add'
+ IsBigOWith.sum_congr
+ IsBigOWith.sum_congr'
+ IsLittleO.add_add'

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.50)

Current number	Change	Type
2	1	large files

Current commit ac750488a3
Reference commit f618ef9056

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[j-loreaux]

Can you say a bit why you prefer the versions with nonnegativity assumptions as opposed to the sum of norms on the RHS (as in the existing IsLittleO.add_add)? I would understand it if it required the same / fewer assumptions, but it doesn't. Therefore, I suspect that the norm version is more useful in practice.

I do think these are nice lemmas to have, but I would prefer the norm versions unless you can convince me otherwise.

[j-loreaux]

Suggested change

	variable {g₁ g₂ : α → ℝ} in
	theorem IsBigO.add_add' (h₁ : f₁ =O[l] g₁) (h₂ : f₂ =O[l] g₂)
	theorem IsBigO.add_add {g₁ g₂ : α → ℝ} (h₁ : f₁ =O[l] g₁) (h₂ : f₂ =O[l] g₂)

[khwilson]

thanks @j-loreaux !

To answer your question, a common technique for bounding sums is that you break the sum up into parts (eg dyadic intervals) and then you show that each component is O of some positive number (eg H / 2^l for some running variable H). You then appeal to the fact that this is a geometric series to show the overall sum is O(H)

The current setup would end up with a sum over |H / 2^l| and so you’d have to get rid of the norms to apply a geometric sum type lemma

So I found this slightly easier to utilize for this style of argument in the proof I built about how many reducible polynomials there are of bounded height

[khwilson]

Also fwiw I thought that naming these with a prime would be a good way to distinguish the norm and nonnegative versions. I could add the norm versions in if that is preferable and make a note on naming conventions?