lim (Re) = Re( lim)?

Stream: new members

[Alex Kontorovich]

Hello, can I please have help proving (or even properly stating) something like this?

lemma lim_re (f : cau_seq ℂ complex.abs) : (f.lim).re = (f.re).lim :=
begin
    sorry,
end

Of course the problem is that f.re isn't defined... (How do I define it, or is something related in mathlib somewhere and I can't find it?) Thanks!

[Yury G. Kudryashov]

Why do you need cau_seq?

[Yury G. Kudryashov]

I know that it's not documented at all but cau_seq is considered to be an implementation detail of def real := ...

[Yury G. Kudryashov]

Most of the topology library relies on cauchy_seq.

[Yury G. Kudryashov]

Some day we should migrate complex.exp from cau_seq, but I don't want to do this migration until we have a glue between mv_power_series and analytic functions.

[Yury G. Kudryashov]

(then we'll port it to analytic functions)

[Alex Kontorovich]

I think I've figured out the statement?

lemma lim_re (f : cau_seq ℂ  complex.abs) (g : cau_seq ℝ   abs) (h : ∀ i, f i = (g i:ℂ )) : f.lim = (g.lim:ℂ ) :=
begin
    sorry,
end

[Alex Kontorovich]

I need something with exp, which is defined in terms of cau_seq... Thanks!

[Yury G. Kudryashov]

We should prove has_sum (λ z, z^n / n!) (exp z), may be even before migrating to analytic functions.

[Yury G. Kudryashov]

I can do it tonight or tomorrow.

[Yury G. Kudryashov]

Which fact about exp do you want to prove?

[Yury G. Kudryashov]

I'm sorry that you have to deal with cau_seq here. I was going to migrate it to at least cauchy_seq for months.

[Yury G. Kudryashov]

I think, we should have a fact that cau_seq tends to its lim.

[Yury G. Kudryashov]

Then continuous_re should help you.

[Yury G. Kudryashov]

See docs#cau_seq.tendsto_limit

[Yury G. Kudryashov]

lemma lim_re (f : cau_seq ℂ  complex.abs) (g : cau_seq ℝ abs) (h : ∀ i, f i = (g i:ℂ )) : f.lim = (g.lim : ℂ) :=
begin
  refine tendsto_nhds_unique f.tendsto_limit _,
  rw [show ⇑f = λ i, (g i : ℂ), from funext h],
  exact (complex.continuous_of_real.tendsto g.lim).comp g.tendsto_limit
end

[Yury G. Kudryashov]

@Alex Kontorovich :up:

[Alex Kontorovich]

Ah, thanks. But I'm getting an error at f.tendsto_limit...:

'tendsto_limit' is not a valid "field" because environment does not contain 'subtype.tendsto_limit'
f
which has type
{f // is_cau_seq complex.abs f}

?? Thanks!

[Heather Macbeth]

You might be missing the import?

import topology.metric_space.cau_seq_filter

[Alex Kontorovich]

Maybe I should cut to the chase of what I'm trying to prove; perhaps there's an easier way to do it.

theorem expLinearization : Π x, complex.abs x ≤ 1
                                 → Π z, complex.abs (complex.exp (x * z) - (x * z + 1))
                                      ≤ (complex.abs x * complex.abs x) * real.exp (complex.abs z) :=
begin
   sorry,
end

That is, if |x|\le 1 and z is any complex number, then
|exp(x z ) - (1 + xz)| \le |x|^2 exp(|z|).

Human proof:
|exp(x z ) - (1 + xz)| = | (xz)^2/2! + (xz)^3/3!+... |
\le |x|^2 (|z|^2/2!+|z|^3/3!+...) (here using |x|\le 1)
\le |x|^2(1+|z|+|z|^2/2!+|z|^3/3!+...)
= |x|^2 exp(|z|).

[Alex Kontorovich]

That did it, thanks!...

[Heather Macbeth]

I think you could prove this by Taylor's theorem, right? That might be the "high-level" way (interacting with the API about the derivative of exp, rather than the details of the construction).

[Heather Macbeth]

Here's a PR by an undergraduate student of mine, doing something similar to prove bounds about arctan: #4228

[Heather Macbeth]

Minor problem -- no Taylor's theorem in mathlib yet :) (though messing round with the mean value theorem on a suitable auxiliary function would probably work)