# Zulip Chat Archive

## Stream: new members

### Topic: power series

#### Alex Kontorovich (Sep 24 2020 at 20:10):

Another stupid question please: what's the best way deal with a function defined by a power series? For example, if I want to access the power series of exp, is something like this available somewhere?

```
theorem expPowerSer : ∀ u v :ℂ , complex.exp u = v → (∀ ε:ℝ, 0<ε → ∃ N:ℕ , complex.abs(v- ((finset.range N).sum (λ n, u^n/ (nat.fact n) )))<ε)
:=
begin
intros,
-- by library_search,
sorry,
end
```

#### Heather Macbeth (Sep 24 2020 at 20:11):

At the moment, exp in particular is defined by power series, but in an ad-hoc way, that has not been connected yet to the general theory of power series.

#### Yakov Pechersky (Sep 24 2020 at 20:11):

Specifically:

```
/-- The Cauchy sequence consisting of partial sums of the Taylor series of
the complex exponential function -/
@[pp_nodot] def exp' (z : ℂ) :
cau_seq ℂ complex.abs :=
⟨λ n, ∑ m in range n, z ^ m / nat.fact m, is_cau_exp z⟩
/-- The complex exponential function, defined via its Taylor series -/
@[pp_nodot] def exp (z : ℂ) : ℂ := lim (exp' z)
```

#### Heather Macbeth (Sep 24 2020 at 20:12):

But "someday", everything will be neatly deduced from the general theory in

https://leanprover-community.github.io/mathlib_docs/analysis/analytic/basic.html

#### Alex Kontorovich (Sep 24 2020 at 20:18):

Yes, I saw that that's how it's defined. But then how do I actually access the power series if trying to prove something. E.g.

```
theorem expBnd : ∀ x:ℂ , complex.abs x < 1/2 → complex.abs (complex.exp x - (1+x))< 1:=
begin
intros,
sorry,
end
```

#### Alex Kontorovich (Sep 24 2020 at 20:21):

The "human" proof is of course that the tail is |x^2/2+x^3/3!+...| < |x|^2+|x|^3+...< 1/4+1/8+... = 1/2. What's a good way of executing such a thing in Lean?...

#### Yakov Pechersky (Sep 24 2020 at 20:22):

Here is a related existing mathlib proof:

```
lemma abs_exp_sub_one_sub_id_le {x : ℂ} (hx : abs x ≤ 1) :
abs (exp x - 1 - x) ≤ (abs x)^2 :=
calc abs (exp x - 1 - x) = abs (exp x - ∑ m in range 2, x ^ m / m.fact) :
by simp [sub_eq_add_neg, sum_range_succ, add_assoc]
... ≤ (abs x)^2 * (nat.succ 2 * (nat.fact 2 * (2 : ℕ))⁻¹) :
exp_bound hx dec_trivial
... ≤ (abs x)^2 * 1 :
mul_le_mul_of_nonneg_left (by norm_num) (pow_two_nonneg (abs x))
... = (abs x)^2 :
by rw [mul_one]
```

#### Yury G. Kudryashov (Sep 24 2020 at 20:24):

I think that we talk about "some day" too much. Let's discuss how to actually do it.

#### Yury G. Kudryashov (Sep 24 2020 at 20:25):

I know that I've started this discussion months ago...

#### Yury G. Kudryashov (Sep 24 2020 at 20:25):

First, we have power series in algebra and in `analysis/analytic`

.

#### Alex Kontorovich (Sep 24 2020 at 20:25):

Thanks, that's what I was looking for! (I think... we'll see if it works for what I need...)

#### Yury G. Kudryashov (Sep 24 2020 at 20:33):

If we want a theory of one-variable analytic functions, the first step would be to define

- docs#continuous_multilinear_map that computes the product of its arguments;
- docs#formal_multilinear_series from docs#power_series; this should be at least an
`alg_hom`

; - relate docs#formal_multilinear_series.radius to the coefficients of the original docs#power_series;
- define, e.g.,
`power_series.exp : power_series \Q`

and prove some properties of this formal series; - redefine
`exp`

as the sum of the corresponding`formal_multilinear_series`

.

#### Yury G. Kudryashov (Sep 24 2020 at 20:34):

@Sebastien Gouezel Which items do we already have? I know that we have a lot of theory about general analytic functions, so this is not included in the list.

#### Sebastien Gouezel (Sep 24 2020 at 20:36):

For the first point, we have

```
/-- The canonical continuous multilinear map on `𝕜^ι`, associating to `m` the product of all the
`m i` (multiplied by a fixed reference element `z` in the target module) -/
protected def mk_pi_field (z : E₂) : continuous_multilinear_map 𝕜 (λ(i : ι), 𝕜) E₂ :=
```

#### Sebastien Gouezel (Sep 24 2020 at 20:38):

But indeed all the glue specializing the general framework of analytic functions to one dimension (analogous to what we have for `fderiv`

/ `deriv`

) is completely missing.

#### Yury G. Kudryashov (Sep 24 2020 at 20:40):

As far as I understand, we also miss a framework for finite dimensional analytic functions (i.e., starting with `mv_power_series`

).

#### Yury G. Kudryashov (Sep 24 2020 at 20:41):

I think that `mk_pi_field`

should be generalized to a `normed_algebra`

.

#### Alex Kontorovich (Sep 24 2020 at 20:46):

Ok I'm still stuck on the first line: ∑ m in range 2, x ^ m / m.fact.

It doesn't know what "∑" is. I looked at the source code (https://github.com/leanprover-community/mathlib/blob/02ca5e2/src/data/complex/exponential.lean) and the symbol is used on line 90 without being defined. How do I get Lean to allow it? Thanks!

#### Yury G. Kudryashov (Sep 24 2020 at 20:51):

This is a localized notation; you need `open_locale big_operators`

to make it available.

#### Yakov Pechersky (Sep 24 2020 at 20:51):

It comes from `import algebra.big_operators`

which is likely transitively imported

#### Yakov Pechersky (Sep 24 2020 at 20:52):

And to have access to the symbol, have `open_locale big_operators`

after your imports

#### Yury G. Kudryashov (Sep 24 2020 at 20:52):

Note that it is the "sum" symbol, not "sigma"; I double checked, you use the correct symbol.

Last updated: Dec 20 2023 at 11:08 UTC