MvPowerSeries and HahnSeries

Stream: mathlib4

[Yaël Dillies]

I just realised today that docs#MvPowerSeries isn't defined in terms of docs#HahnSeries. MvPowerSeries σ R is (σ →₀ ℕ) → R with convolution product. Therefore it could be defined as HahnSeries (σ →₀ ℕ) R, which comes equipped with the convolution product too.

[Eric Wieser]

Because every Set (σ →₀ ℕ) is PWO?

[Yaël Dillies]

Yes, that's precisely the point

[Eric Wieser]

What would "defined in terms of" mean here?

[Eric Wieser]

An abbrev?

[Eric Wieser]

(and give isPWO_support' an autoParam that knows how to handle finsupp and nat)

[Yaël Dillies]

Either an auto-param or a constructor for HahnSeries Γ R whenever Γ is well-founded

[Eric Wieser]

I think the autoparam is the simpler approach, especially if it's just apply the generic theorem about well-founded-ness

[Filippo A. E. Nuccio]

Pinging @Antoine Chambert-Loir with whom we had a discussion about this.

[Antoine Chambert-Loir]

I believe it's a good idea, but it will become very good if the next move is generalizing accordingly the API for Hahn Series. Otherwise, I don't feel it's very useful. I am worried about abbrev, though, I can already hear complaints on Zulip of people working of multivariate power series asking why there's nothing in mathlib because Lean is expecting result for Hahn series.

[Yaël Dillies]

Hopefully we would mitigate your last concern by adding a big flashy warning in the docstring of MvPowerSeries