Taylor expansions of elementary functions

Stream: Is there code for X?

[Vasilii Nesterov]

Hi there!
Do we have theorems about Taylor expansions of elementary functions? More precisely, I would like to use something like "for $|x| < 1$, the series with coefficients $[1, -1, 1, -1, \dots]$ converges to $1/(1+x)$" and similar results for $\log$, $\exp$, and so on.

[Yaël Dillies]

Yes we do, see eg docs#NormedSpace.expSeries_hasSum_exp

[Vasilii Nesterov]

Thanks! It took a while for me to understand the API. I see the results about $\log$ and $\exp$, but can't find anything about $(1+x)^{-1}$. Am I missing something? If not, I can submit a PR for this.

[Daniel Weber]

docs#hasSum_geometric_of_lt_one (or more generally docs#hasSum_geometric_of_norm_lt_one )

[Luigi Massacci]

@loogle  ∑' (i : ℕ), (-1)^i * (?x ^ i) = (1 + ?x)⁻¹

[loogle]

:shrug: nothing found

[Luigi Massacci]

@loogle "neumann"

[loogle]

:search: VonNeumannAlgebra, VonNeumannAlgebra.commutant, and 18 more

[Luigi Massacci]

Ok should have thought of that not working

[Luigi Massacci]

@Vasily Nesterov it does indeed appear to be missing

[Vasilii Nesterov]

Thanks!

[Vasilii Nesterov]

Sorry for necrobumping, but I again can't cope with finding series' API, now for $(1+x)^a$. I've tried loogle and moogle, but found nothing. Do we have something about it in Mathlib?

[Ruben Van de Velde]

What's x and a?

[Vasilii Nesterov]

Sorry for ambiguity. I am looking for binomail series:
$(1 + x)^a = \sum_{k=0}^{\infty} \; \binom{a}{k} \; x^k = 1 + a x + \frac{a(a-1)}{2!} x^2 + \frac{a(a-1)(a-2)}{3!} x^3 + \cdots$
where $x$ is a real-valued variable, and $a$ is a real parameter.

[Vasilii Nesterov]

What I hope to find is some theorem stating that this series converges to $(1 + x)^a$ in some neighborhood of $0$.

[Daniel Weber]

I can't find one, it might be missing