feat: uniform asymptotics

[llllvvuu]

trafficstars

Example usage: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/15f08ef06df37286bf8636b4573e84f69994aa4b/PrimeNumberTheoremAnd/PerronFormula.lean#L385-L503. Tools introduced:

1. f =Θ[x -> principal s, y -> any] 1 where f(x, y) = C(x) on compact s
2. 1 =o[x -> any, y -> atTop] y
3. Extract big-O of integral along x, as y -> top
4. Extract big-O of f(x, y) as y -> top, at each fixed x in s

\1. and 2. combined give f =o[x -> principal s, y -> atTop] y, although I did not make this a lemma.

---

• [x] depends on: #10285

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#10285~~ By Dependent Issues (🤖). Happy coding!

[github-actions[bot]]

PR summary fce93532b1

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.MeasureTheory.Integral.Asymptotics	1664	1694	+30 (+1.80%)

Import changes for all files

Files	Import difference
Mathlib.MeasureTheory.Integral.Asymptotics	30

---

Declarations diff

+ IsBigO.comp_fst + IsBigO.comp_snd + IsBigO.eventually_integrableOn + IsBigO.fiberwise_left + IsBigO.fiberwise_right + IsBigO.set_integral_isBigO + IsLittleO.comp_fst + IsLittleO.comp_snd + IsTheta.comp_fst + IsTheta.comp_snd + IsTheta.fiberwise_left + IsTheta.fiberwise_right + isBigOWith_principal + isBigOWith_rev_principal + isBigO_principal + isBigO_rev_principal + isTheta_bot + isTheta_principal

You can run this locally as follows

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

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

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

[mathlib-bors[bot]]

Build failed:

• Build

[mathlib-bors[bot]]

:v: llllvvuu can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[llllvvuu]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style