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