[Merged by Bors] - feat: cardinality of Hahn series inverse

[vihdzp]

---

• depends on: [Merged by Bors] - feat: cardinality of Hahn series #32640
• depends on: [Merged by Bors] - feat(SetTheory/Cardinal): formulas for sum (fun n : ℕ ↦ x ^ n) #32645

[github-actions]

PR summary c96081d930

Import changes exceeding 2%

%	File
+2.21%	Mathlib.RingTheory.HahnSeries.Cardinal

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.HahnSeries.Cardinal	858	877	+19 (+2.21%)

Import changes for all files

Files	Import difference
Mathlib.RingTheory.HahnSeries.Cardinal	19

---

Declarations diff

+ cardSupp_div_le
+ cardSupp_hsum_le
+ cardSupp_hsum_powers_le
+ cardSupp_inv_le
+ cardSupp_mul_single_le
+ cardSupp_one
+ cardSupp_one_le
+ cardSupp_pow_le
+ cardSupp_single_mul_le
+ coeff_mul_single
+ coeff_order_eq_zero
+ coeff_single_mul

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

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: cardinality of Hahn series #32640
• [Merged by Bors] - feat(SetTheory/Cardinal): formulas for sum (fun n : ℕ ↦ x ^ n) #32645
  By Dependent Issues (🤖). Happy coding!

[YaelDillies]

Why does cardSupp exist? I am worried that we are adding API to a useless wrapper.

[vihdzp]

κ-bounded Hahn series appear quite a bit in the literature. In particular, the surreals are univ-bounded (small) real Hahn series with their order dual as value group.

The next PR in this series defines the subfield of κ-bounded Hahn series for uncountable κ, on which some 2,000 lines of code on the CGT repo currently depend.

[YaelDillies]

Great! so \kappa-bounded Hahn series is a useful concept. What I think is a useless concept that of the cardinality of a Hahn series, in the sense that it is merely the cardinality of its support.

In the PR introducing cardSupp, I see you argued that cardinalMk_support was poor naming, and that introducing cardSupp would fix that. But that argument assumed that one would write Cardinal.mk (HahnSeries.support x), while in fact it should be Set.card (HahnSeries.support x), whose name in lemmas would be card_support, which I find perfectly acceptable. If that's still too long for you, then I would advise renaming HahnSeries.support to HahnSeries.supp instead of adding cardSupp.

[vihdzp]

I don't believe Set.card is a thing? I've been under the impression that the way to write the cardinality of a set is to use Cardinal.mk directly.

As for renaming support to supp, this would run counter to what we do for Function.support, Polynomial.support, Module.support, Equiv.Perm.support, and PMF.support.

[vihdzp]

Is there any harm in having cardSupp if it is in fact an object of interest within the theory of Hahn series? Or should I rewrite this entire file in terms of cardinalMk_support?

[erdOne]

I don't think cardSupp is an unuseful wrapper. I think this PR and the previous PR already demonstrated that there are enough results about this idea that it warrants special API support, and having this wrapper is useful in pointing people to these API.
Other than this issue I think this PR is ready to go and I think some third opinion here to unblock this PR would be useful.

maintainer merge?

[github-actions]

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

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded!

And happy new year! 🎉

• Build
• Lint style
• Post-Build Step