continuous functions commute with limits?

Stream: Is there code for X?

[Jalex Stark]

import tactic
import data.nat.basic
import analysis.complex.exponential
open real

lemma cont_of_cau_is_cau (f : ℝ → ℝ) (hf : continuous f) (xn : ℕ → ℝ ) (hx : is_cau_seq abs xn) :  (is_cau_seq abs (λ n, f $ xn n)) := sorry

def mapply (f : ℝ → ℝ) (hf : continuous f) (xn : cau_seq ℝ abs) : cau_seq ℝ abs :=
begin
cases xn, split, swap, exact λ n, f $ xn_val n, apply cont_of_cau_is_cau,
assumption, assumption,
end

lemma cont_lim_eq_lim_cont (f : ℝ → ℝ) (hf : continuous f) (xn : cau_seq ℝ abs) : (cau_seq.lim $ mapply f hf xn) = (f $ cau_seq.lim xn) := sorry

[Yury G. Kudryashov]

You should use filter.tendsto if possible.

[Yury G. Kudryashov]

Most lemmas about continuity etc. are written in terms of tendsto, filter.cauchy etc

[Yury G. Kudryashov]

cau_seq is an "implementation detail" of the current definition of real numbers. IMO using it in complex.exponential is an unfortunate leak of the internal API.

[Yury G. Kudryashov]

It would be nice to redefine exp, sin, cos for any normed banach algebra instead.

[Yury G. Kudryashov]

If you use filter.tendsto, then there is a continuous.tendsto and tendsto.comp.

[Patrick Massot]

Let me expand Yury's answer a bit. As he wrote, cau_seq and is_cau_seq are not meant for end-users, they are intermediate notions used to build the topology on real and $p$-adic numbers. But of course, once you have a metric space (or more generally a uniform space) we do have Cauchy sequences in them, the predicate is named cauchy_seq. In order to get you started I proved your first lemma, but this is almost certainly not what you really wanted (here I mean in maths, nothing to do with Lean). For instance the statement suggested by the name is not at all what your Leaned.

import topology.instances.real

open filter
open_locale topological_space

lemma cont_of_cau_is_cau (f : ℝ → ℝ) (hf : continuous f) (xn : ℕ → ℝ)
  (hx : cauchy_seq xn) :  (cauchy_seq (f ∘ xn)) :=
begin
  obtain ⟨x, limx⟩ : ∃ x, tendsto xn at_top (𝓝 x),
    from cauchy_seq_tendsto_of_complete hx,
  have : tendsto (f ∘ xn) at_top (𝓝 (f x)),
    from tendsto.comp hf.continuous_at limx,
  exact cauchy_seq_of_tendsto_nhds _ this
end

[Patrick Massot]

If you are afraid of filters, you can define the notation local notation f ` ⟶ ` limit := tendsto f at_top (𝓝 limit) that you'll find in a couple of files in mathlib (written by people before they started loving filters)

[Yury G. Kudryashov]

We have something similar as a localized notation in locale filter (!) defined in normed_space/basic.

[Yury G. Kudryashov]

But it uses nhds for both filters.

[Yury G. Kudryashov]

And we have local notation for limits at_top in topology/sequences

[Jalex Stark]

but this is almost certainly not what you really wanted (here I mean in maths, nothing to do with Lean). For instance the statement suggested by the name is not at all what your Leaned.
Hmm I'm not sure I understand why.

I'll try writing a different definition for exp. If I can prove the theorems I want about it (right now i'm looking for x < exp x), I'll then tackle the question of proving it equal to the old one .

[Yury G. Kudryashov]

How are you going to define exp?

[Kevin Buzzard]

For the normed Banach algebra definition, $x<e^x$ doesn't make sense because there will be no ordering on the elements (for example the complexes is a normed Banach algebra). In Lean we have

real.add_one_le_exp_of_nonneg : ∀ {x : ℝ}, 0 ≤ x → x + 1 ≤ real.exp x
real.exp_pos : ∀ (x : ℝ), 0 < real.exp x

[Kevin Buzzard]

There's a freebie PR out there -- x + 1 ≤ real.exp x is true for all real numbers, not just non-negative ones.