power series

Stream: new members

[Alex Kontorovich]

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]

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]

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]

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]

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]

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]

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]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Alex Kontorovich]

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

[Yury G. Kudryashov]

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]

@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]

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]

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]

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]

I think that mk_pi_field should be generalized to a normed_algebra.

[Alex Kontorovich]

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]

This is a localized notation; you need open_locale big_operators to make it available.

[Yakov Pechersky]

It comes from import algebra.big_operators which is likely transitively imported

[Yakov Pechersky]

And to have access to the symbol, have open_locale big_operators after your imports

[Yury G. Kudryashov]

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