Generalize/abstract geometric series

Stream: mathlib4

[Weiyi Wang]

In mathlib there is docs#geom_series_mul_neg, which is stated for NormedRing. I have a similar lemma for PowerSeries for my own use (I didn't find this in mathlib. Is it there?)

theorem PowerSeries.geom_series_mul_neg {M : Type*} [CommRing M] [TopologicalSpace M] [T2Space M]
    [IsTopologicalRing M] {x : M⟦X⟧} (hx : x.order ≠ 0) :
    (∑' (j : ℕ), x ^ j) * (1 - x) = 1 := sorry

I could PR this as-is, but I wonder if there is a way to have a more abstract way to include both, and possibly more forms of geometric series?

[Weiyi Wang]

(btw I think the thoerem is misnamed because there isn't a "neg" in the statement)

[Kenny Lau]

Weiyi Wang said:

more abstract way to include both

maybe state it in terms of Int[[x]]?

[Weiyi Wang]

What do you mean?
I probably should clarify that "include both" means a general theorem that implies the NormedRing version and the PowerSeries version (with possibly some modification to hypothesis). Int[[X]] doesn't imply the NormedRing version, right?

[Kenny Lau]

well I would hope that if f and g are power series and they both converge in a normed ring (for b) then f(b) g(b) = (fg)(b)

[Kenny Lau]

and 1-x and 1 always converge

[Weiyi Wang]

I don't think there are theory of evaluating power series in normed ring in mathlib yet

[Yakov Pechersky]

There is, it just uses FormalMultilinearSeries

[Kenny Lau]

of course

[Weiyi Wang]

But I am doing combinatorics and I don't need to evaluate. The original question was just asking if there is a way to unify, and I am fine if the answer is "no" or "too difficult"

[Weiyi Wang]

Oh, I might have misread your message. Let me think a bit...

[Scott Carnahan]

For PowerSeries, there is docs#PowerSeries.mk_add_choose_mul_one_sub_pow_eq_one

[Weiyi Wang]

Yeah I am aware of that, but the one I need is substituting X with an arbitrary (x : PowerSeries R) (I haven't tried actually using the substitution lemmas for PowerSeries yet, which I will do soon)

[Scott Carnahan]

Sorry for missing that! You may be able to use docs#HahnSeries.SummableFamily.one_sub_self_mul_hsum_powers after some translation.

[Riccardo Brasca]

I am almost sure we have the substituon of one power series into another in maximal generality (even for infinitely many variables).