Power series

Stream: Is there code for X?

[Jireh Loreaux]

In my outline for Gelfand's formula, I need to prove that the coefficients of two power series are equal because they represent the same function on a ball of positive radius. I don't think we already know this. So I went to prove it, but I think we don't know the formula for the derivative of a power series yet either. My method for showing this would be to use the lemma that if a convergent sequence of differentiable functions has derivatives which converge (locally) uniformly then their limit is the derivative of the limit of the original sequence. I think this is not in mathlib either. Does this all seem accurate, or am I missing pieces of the library again?

[Eric Rodriguez]

Sorry if I'm pointing to bad info, I don't know this part of the library:

the derivative of a power series seems to be here.

[Yury G. Kudryashov]

I think that @Sebastien Gouezel will tell us the right generality of this statement. Basically, if you prove by induction, then due to docs#has_fpower_series_at.is_O_sub_partial_sum_pow you only need to show that two k-linear continuous_multilinear_maps are equal (in the sense of some natural equivalence) if their difference is O(z^(k+1)).

[Yury G. Kudryashov]

Do you work in dimension one?

[Jireh Loreaux]

Yes, just dimension 1. Doesn't docs#has_fpower_series_at.has_strict_deriv_at just say that the derivative at the the center of the ball is the second coefficient of the power series. It's not saying that the derivative has a power series representation, right?

[Yury G. Kudryashov]

Right.

[Yury G. Kudryashov]

I was going to add this but the formula in the higher dimensional case is not trivial (AFAIR, I may be wrong).

[Yury G. Kudryashov]

I can look into this again next week-end.

[Yury G. Kudryashov]

But you can prove equality of power series coefficients directly using docs#has_fpower_series_at.is_O_sub_partial_sum_pow.

[Yury G. Kudryashov]

Let p and q be two formal power series that represent the same function. Let n be the first index such that p n ≠ q n (e.g., you can prove ∀ n, p n = q n by strong induction on n or use nat.find).

[Jireh Loreaux]

I see. That makes sense.

[Yury G. Kudryashov]

Then we have p.partial_sum p (n + 1) y - p.partial_sum q (n + 1) y = O(y ^ (n + 1))

[Yury G. Kudryashov]

Since p k = q k for k < n, LHS = p n (λ _, y) - q n (λ _, y).

[Jireh Loreaux]

yes, this is clear to me.

[Yury G. Kudryashov]

Do you deal with a general formal power series, of p is constructed using docs#continuous_multilinear_map.mk_pi_field?

[Yury G. Kudryashov]

In the latter case, you can say that p n (λ _, y) = a * y ^ n and q n (λ _, y) = b * y ^ n, so you have (a - b) * y ^ n = O(y ^ (n + 1)) which is possible only for a - b = 0.

[Jireh Loreaux]

@Yury G. Kudryashov Just got back to looking at this, it seems that docs#has_fpower_series_at.is_O_sub_partial_sum_pow should have a stronger conclusion, namely: ^ (n + 1) instead of ^ n, right? Otherwise, I can't even use this to prove that the constant term of p is f x.

[Yury G. Kudryashov]

ppartial_sum n is the sum over k=0..n-1

[Jireh Loreaux]

ah, I see, so p.partial_sum 0 is what, defeq 0?

[Jireh Loreaux]

I guess because it's a the sum over an empty finset

[Yury G. Kudryashov]

Yes.