convergence of a power series

Stream: maths

[Filippo A. E. Nuccio]

Is there a nice way to say that a power series (say, with real coefficients) converges at a point x : ℝ? What I could come up with is

def conv_blah (f : power_series ℝ) (x : ℝ) : summable (λ k, (power_series.coeff ℝ k f) * x ^ k) :=

because I was unable to find a clearer "evaluation" operator. But I suspect that this should already be in mathlib as part of the API for power_series.

[Johan Commelin]

No, I don't think it's there yet.

[Johan Commelin]

power_series is completely algebraic for now

[Johan Commelin]

But connecting it to the analytic world should be done at some point

[Johan Commelin]

Do you want this for LTE?

[Heather Macbeth]

There is docs#formal_multilinear_series.radius, etc -- the problem is that this theory has not beeen connected to power_series. @Yury G. Kudryashov was working on this last year but I don't know if there's been any progress lately.

[Johan Commelin]

(Just for the record, I'm not sure that power_series will be useful for LTE.)

[Filippo A. E. Nuccio]

Thanks! I am trying to state/prove Harbater's lemma on the kernel of $\theta$. I agree I could work with laurent_measures (supported at a singleton) but it is not clear to me whether this is really an advantage. At any rate, I will try to introduce as little technology as possible beyond what is already in LTE.

[Johan Commelin]

But you need laurent_series, right?

[Johan Commelin]

You need to allow a_{-n} coefficients

[Filippo A. E. Nuccio]

Well, actually for Harbater's lemma 1.5 I don't think so (unless I have misread it).

[Filippo A. E. Nuccio]

His construction only needs positive nonnegative indexes.

[Filippo A. E. Nuccio]

Then Scholze-Clausen observe that the kernel of $\theta$ is generated by, for instance, that gadget. And since there are many units with negative coefficients, a generic element in the kernel will also have negative ones, but there exists a generator with positive nonnegative ones only, I think.

[Johan Commelin]

@Filippo A. E. Nuccio Can you copy-paste the statement of Harbater 1.5?

[Filippo A. E. Nuccio]

Sure (in the meanwhile, do you want to move our discussion to the LTE stream?)

[Johan Commelin]

In the case that we are interested in, the kernel of $θ$ should be easy to compute. (But for general $\theta_x$ you need to work harder.)

[Johan Commelin]

Filippo A. E. Nuccio said:

Sure (in the meanwhile, do you want to move our discussion to the LTE stream?)

Ooh, we can discuss it here. Doesn't matter too much I think

[Filippo A. E. Nuccio]

1.5. LEMMA. Let $r$ be a positive real number less than $1$ and let $x$ be a non-zero complex number of absolute value at most $r$. Then there is an $f \in \mathbb{Z}\{t\}$ congruent to 1 modulo $t$ which vanishes to order $1$ at $x$ and its complex conjugate, and vanishes nowhere else in the disc $\vert t \vert \leq r$.

[Filippo A. E. Nuccio]

(Of course, I was neglecting the "complex conj" business, working with real $x$)

[Johan Commelin]

Right. But we only need the case $x = \frac12$.

[Johan Commelin]

And then that lemma is obvious.

[Filippo A. E. Nuccio]

Ah, I see. This makes life easier indeed, I completely forgot that we can restrict to that case (most probably as I have never quite tried to really undestand why).

[Filippo A. E. Nuccio]

So, if I got it right, you are suggesting that from now on we specialize to $\xi=\frac{1}{2}$ and simplify all proofs accordingly?

[Johan Commelin]

Yes, for the kernel, and the corresponding short exact sequence, you only need to prove this for $1/2$

[Filippo A. E. Nuccio]

Ok, thanks. I will then move on to simplify all statements I have pushed so far and then try to prove them.

[Johan Commelin]

But please keep the stuff about surjectivity for general $x$. That was really nice!