# Zulip Chat Archive

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