feat(Analysis.Normed.Ring.Seminorm): add SmoothingSeminorm

[mariainesdff]

We prove [BGR, Proposition 1.3.2/1][bosch-guntzer-remmert] : if f is a nonarchimedean seminorm on R, then iInf (λ (n : pnat), (f(x^(n : ℕ)))^(1/(n : ℝ))) is a power-multiplicative nonarchimedean seminorm on R.

---

• [ ] depends on: #18173
• [ ] depends on: #18172
• [ ] depends on: #18171
• [x] depends on: #16767
• [x] depends on: #16768
• [x] depends on: #16770

[github-actions[bot]]

PR summary e1af4db594

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.Normed.Ring.SmoothingSeminorm (new file)	1603

---

Declarations diff

+ isNonarchimedean_smoothingFun + isPowMul_smoothingFun + pow_mul_apply_eq_pow_mul + smoothingFun + smoothingFun_apply_of_map_mul_eq_mul + smoothingFun_le + smoothingFun_le_self + smoothingFun_nonneg + smoothingFun_of_map_mul_eq_mul + smoothingFun_of_powMul + smoothingFun_one_le + smoothingSeminorm + smoothingSeminormSeq + smoothingSeminormSeq_bddBelow + smoothingSeminorm_apply_of_map_mul_eq_mul + smoothingSeminorm_map_one_le_one + smoothingSeminorm_of_mul + tendsto_smoothingFun_comp + tendsto_smoothingFun_of_eq_zero + tendsto_smoothingFun_of_map_one_le_one + tendsto_smoothingFun_of_ne_zero + zero_mem_lowerBounds_smoothingSeminormSeq_range

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.

---

No changes to technical debt.

You can run this locally as

./scripts/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).

[jcommelin]

This PR is quite large. Are you planning to split it up?

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#18173~~
• ~~leanprover-community/mathlib4#18172~~
• ~~leanprover-community/mathlib4#18171~~
• ~~leanprover-community/mathlib4#16767~~
• ~~leanprover-community/mathlib4#16768~~
• ~~leanprover-community/mathlib4#16770~~ By Dependent Issues (🤖). Happy coding!

[mariainesdff]

Haven't looked at the mathematics, but here's style and naming comments

Thanks!

[faenuccio]

I left some answers to your comments, I'll now check the remaining sections.

[faenuccio]

Thanks for all the work, LGTM!

[faenuccio]

maintainer merge

[github-actions[bot]]

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

[mathlib-bors[bot]]

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

[mathlib-bors[bot]]

Build failed (retrying...):

• Build

[bryangingechen]

bors r-

Please merge master, fix the build and place back on the queue by commenting bors merge. Thanks!

[mathlib-bors[bot]]

Canceled.

[mariainesdff]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style