## 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) :
... ≤ (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

#### 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