How do I prove that a power series is zero, given a zero sum

Stream: mathlib4

[Zhuanhao Z Wu]

I'm trying to prove the following (on $\mathbb{R}$ of course): suppose the power series converges to zero, then its coefficients must be zero.

$$\sum_n a_n x^n = 0 \implies \forall i \in \mathbb{N}, a_i = 0$$

I have formalised it as follows and I feel this should be proven using one or two lemmas.
However, it seems that no lemmas related to ofScalarsSum would do the job.

So I'm wondering if I'm missing some conditions on the problem (sorry it's been long since I last did calculus), the lemma lies somewhere else, or I just miss it somehow.
Note that I need the f.sum so that I can later show a tsum is zero.

import Mathlib
import Mathlib.Analysis.Analytic.Basic
import Mathlib.Analysis.Analytic.OfScalars
import Mathlib.Analysis.Calculus.FormalMultilinearSeries


theorem fzero: ∀ (x: ℝ) (c: ℕ → ℝ) (f: FormalMultilinearSeries ℝ ℝ ℝ), f = (FormalMultilinearSeries.ofScalars ℝ c) ->f.sum = 0 -> f = 0 := by
  intro x c f hf hsum

[Notification Bot]

This topic was moved here from #lean4 > How do I prove that a power series is zero, given a zero sum by Eric Wieser.

[Eric Wieser]

Unfortunately I think the statement is false because mathlib defines the tsum of a non-converging sequence as zero

[Eric Wieser]

You can cut through the noise to see the problem with

  subst f
  simp [funext_iff, FormalMultilinearSeries.sum, FormalMultilinearSeries.ofScalars] at hsum ⊢

[Zhuanhao Z Wu]

Thanks! I suppose it would be possible to add more conditions such as HasSum or x ∈ EMetric.ball 0 f.radius.

And if that's the case, I wonder if we have a path to show f = 0 from some notation of its sum?

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

docs#FormalMultilinearSeries

[Zhuanhao Z Wu]

I hate to say this, but I wasn't able to find something that goes from p.sum to p = 0 under FormalMultilinearSeries. Specifically, I was looking for lemmas with the name sum under FormalMultilinearSeries. I have a feeling that I might be looking for the wrong name.

There are some lemmas go from p = 0 to p.sum in FormalMultilinearSeries.ofScalarsSum

[Zhuanhao Z Wu]

After playing with FormalMultilinearSeries and PowerSeries a bit more, I think Eric's claim now makes sense to me.

Sum manipulation should be done within FormalMultilinearSeries or PowerSeries and not tsum, once you go tsum, you cannot go back.