feat: prove Cauchy's upper bound on polynomial roots

[Command-Master]

---

• [x] depends on: #16582

[github-actions[bot]]

PR summary 3eff16e2be

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.SpecialFunctions.Polynomials	-1324
Mathlib.Analysis.Polynomial.CauchyBound	1125
Mathlib.Analysis.Polynomial.Basic	1324

---

Declarations diff

+ IsRoot.norm_lt_cauchyBound + cauchyBound + cauchyBound_C + cauchyBound_X + cauchyBound_X_add_C + cauchyBound_X_sub_C + cauchyBound_one + cauchyBound_smul + cauchyBound_zero + geom_sum_mul_of_le_one + geom_sum_mul_of_one_le + geom_sum_of_lt_one + geom_sum_of_one_lt + geom_sum₂_mul_of_ge + geom_sum₂_mul_of_le + geom₂_sum_of_gt + geom₂_sum_of_lt + one_le_cauchyBound

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.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

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

[jcommelin]

maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by jcommelin.

[jcommelin]

@Command-Master Would you mind taking up the points that Yury raised? If you don't have time, I'll try to get to it later.

[urkud]

I'm going to move lemmas from Nonneg tonight.

[jcommelin]

This looks good to me now, but CI seems unhappy. And since I contributed a substantial part of the PR, I can't merge it myself.

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by jcommelin.

[urkud]

Thanks! bors d+

[mathlib-bors[bot]]

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

[Command-Master]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style