## Stream: Is there code for X?

### Topic: continuous functions commute with limits?

#### Jalex Stark (Apr 18 2020 at 06:37):

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 (Apr 18 2020 at 07:43):

You should use filter.tendsto if possible.

#### Yury G. Kudryashov (Apr 18 2020 at 07:44):

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

#### Yury G. Kudryashov (Apr 18 2020 at 07:46):

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 (Apr 18 2020 at 07:47):

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

#### Yury G. Kudryashov (Apr 18 2020 at 07:47):

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

#### Patrick Massot (Apr 18 2020 at 09:21):

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 (Apr 18 2020 at 09:22):

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 (Apr 18 2020 at 23:00):

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

#### Yury G. Kudryashov (Apr 18 2020 at 23:00):

But it uses nhds for both filters.

#### Yury G. Kudryashov (Apr 18 2020 at 23:03):

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

#### Jalex Stark (Apr 19 2020 at 02:45):

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 (Apr 19 2020 at 19:11):

How are you going to define exp?

#### Kevin Buzzard (Apr 19 2020 at 19:24):

For the normed Banach algebra definition, $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 (Apr 19 2020 at 19:25):

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

Last updated: May 07 2021 at 20:11 UTC