# Zulip Chat Archive

## Stream: maths

### Topic: complex forms uniform space

#### Kenny Lau (Oct 04 2018 at 22:59):

import analysis.real analysis.complex theorem complex.conj_sub (z w : ℂ) : complex.conj (z - w) = complex.conj z - complex.conj w := complex.conj_add _ _ theorem complex.uniform_continuous_conj : uniform_continuous complex.conj := uniform_continuous_of_metric.2 $ λ ε hε, ⟨ε, hε, λ z w hzw, show complex.abs _ < ε, by rwa [← complex.conj_sub, complex.abs_conj]⟩ theorem complex.uniform_continuous_re : uniform_continuous complex.re := uniform_continuous_of_metric.2 $ λ ε hε, ⟨ε, hε, λ z w hzw, calc dist z.re w.re ≤ complex.abs (z-w) : complex.abs_re_le_abs (z-w) ... < ε : hzw⟩ theorem complex.uniform_continuous_im : uniform_continuous complex.im := uniform_continuous_of_metric.2 $ λ ε hε, ⟨ε, hε, λ z w hzw, calc dist z.im w.im ≤ complex.abs (z-w) : complex.abs_im_le_abs (z-w) ... < ε : hzw⟩ example (f : filter ℂ) (hf : cauchy f) : ∃ x, f ≤ nhds x := let ⟨xr, hxr⟩ := complete_space.complete (cauchy_map complex.uniform_continuous_re hf) in let ⟨xi, hxi⟩ := complete_space.complete (cauchy_map complex.uniform_continuous_im hf) in ⟨⟨xr, xi⟩, sorry⟩ /- state: f : filter ℂ, hf : cauchy f, xr : ℝ, hxr : filter.map complex.re f ≤ nhds xr, xi : ℝ, hxi : filter.map complex.im f ≤ nhds xi ⊢ f ≤ nhds {re := xr, im := xi} -/

half-completed proof

#### Kenny Lau (Oct 04 2018 at 23:00):

@Andreas Swerdlow

#### Kenny Lau (Oct 04 2018 at 23:21):

import analysis.real analysis.complex theorem complex.conj_sub (z w : ℂ) : complex.conj (z - w) = complex.conj z - complex.conj w := complex.conj_add _ _ theorem complex.uniform_continuous_conj : uniform_continuous complex.conj := uniform_continuous_of_metric.2 $ λ ε hε, ⟨ε, hε, λ z w hzw, show complex.abs _ < ε, by rwa [← complex.conj_sub, complex.abs_conj]⟩ theorem complex.uniform_continuous_re : uniform_continuous complex.re := uniform_continuous_of_metric.2 $ λ ε hε, ⟨ε, hε, λ z w hzw, calc dist z.re w.re ≤ complex.abs (z-w) : complex.abs_re_le_abs (z-w) ... < ε : hzw⟩ theorem complex.uniform_continuous_im : uniform_continuous complex.im := uniform_continuous_of_metric.2 $ λ ε hε, ⟨ε, hε, λ z w hzw, calc dist z.im w.im ≤ complex.abs (z-w) : complex.abs_im_le_abs (z-w) ... < ε : hzw⟩ theorem complex.uniform_continuous_of_real : uniform_continuous complex.of_real := uniform_continuous_of_metric.2 $ λ ε hε, ⟨ε, hε, λ z w hzw, calc dist (complex.of_real z) (complex.of_real w) = dist z w : complex.abs_of_real _ ... < ε : hzw⟩ example (f : filter ℂ) (hf : cauchy f) : ∃ x, f ≤ nhds x := let ⟨xr, hxr⟩ := complete_space.complete (cauchy_map complex.uniform_continuous_re hf) in let ⟨xi, hxi⟩ := complete_space.complete (cauchy_map complex.uniform_continuous_im hf) in have hxr2 : filter.tendsto (complex.of_real ∘ complex.re) f (nhds (complex.of_real xr)), from filter.tendsto.comp hxr (continuous.tendsto (uniform_continuous.continuous complex.uniform_continuous_of_real) xr), have hxi2 : filter.tendsto (complex.of_real ∘ complex.im) f (nhds (complex.of_real xi)), from filter.tendsto.comp hxi (continuous.tendsto (uniform_continuous.continuous complex.uniform_continuous_of_real) xi), have filter.tendsto (λ z:ℂ, (z.re + z.im * complex.I:ℂ)) f (nhds _), from tendsto_add hxr2 (tendsto_mul hxi2 (@tendsto_const_nhds _ _ _ complex.I _)), ⟨(xr+xi*complex.I), by rw [funext complex.re_add_im] at this; rw [← (filter.map_id : _ = f)]; exact this⟩

#### Kenny Lau (Oct 04 2018 at 23:21):

complete proof

#### Andreas Swerdlow (Oct 04 2018 at 23:58):

Wow thank you!

#### Andreas Swerdlow (Oct 04 2018 at 23:59):

@Joseph Corneli look what Kenny did

#### Kenny Lau (Oct 05 2018 at 00:01):

I should probably extract a lemma

#### Mario Carneiro (Oct 05 2018 at 00:01):

that proof looks like a good advertisement for bundling continuous functions

#### Mario Carneiro (Oct 05 2018 at 00:02):

For a while I was thinking that maybe we want to work with continuous functions as a predicate, but compositional proofs of continuity really suck from a readability standpoint

#### Kenny Lau (Oct 05 2018 at 00:03):

another thing to refactor :P

#### Kenny Lau (Oct 05 2018 at 00:12):

import analysis.real analysis.complex theorem complex.conj_sub (z w : ℂ) : complex.conj (z - w) = complex.conj z - complex.conj w := complex.conj_add _ _ theorem complex.uniform_continuous_conj : uniform_continuous complex.conj := uniform_continuous_of_metric.2 $ λ ε hε, ⟨ε, hε, λ z w hzw, show complex.abs _ < ε, by rwa [← complex.conj_sub, complex.abs_conj]⟩ theorem complex.uniform_continuous_re : uniform_continuous complex.re := uniform_continuous_of_metric.2 $ λ ε hε, ⟨ε, hε, λ z w hzw, calc dist z.re w.re ≤ complex.abs (z-w) : complex.abs_re_le_abs (z-w) ... < ε : hzw⟩ theorem complex.uniform_continuous_im : uniform_continuous complex.im := uniform_continuous_of_metric.2 $ λ ε hε, ⟨ε, hε, λ z w hzw, calc dist z.im w.im ≤ complex.abs (z-w) : complex.abs_im_le_abs (z-w) ... < ε : hzw⟩ theorem complex.uniform_continuous_of_real : uniform_continuous complex.of_real := uniform_continuous_of_metric.2 $ λ ε hε, ⟨ε, hε, λ z w hzw, calc dist (complex.of_real z) (complex.of_real w) = dist z w : complex.abs_of_real _ ... < ε : hzw⟩ theorem complex.continuous_conj : continuous complex.conj := uniform_continuous.continuous complex.uniform_continuous_conj theorem complex.continuous_re : continuous complex.re := uniform_continuous.continuous complex.uniform_continuous_re theorem complex.continuous_im : continuous complex.im := uniform_continuous.continuous complex.uniform_continuous_im theorem complex.continuous_of_real : continuous complex.of_real := uniform_continuous.continuous complex.uniform_continuous_of_real theorem complex.filter_le_iff (f : filter ℂ) (z : ℂ) : f ≤ nhds z ↔ filter.tendsto complex.re f (nhds z.re) ∧ filter.tendsto complex.im f (nhds z.im) := ⟨λ h, ⟨le_trans (filter.map_mono h) (continuous.tendsto complex.continuous_re z), le_trans (filter.map_mono h) (continuous.tendsto complex.continuous_im z)⟩, λ ⟨hr, hi⟩, have hr2 : filter.tendsto (λ z:ℂ, (z.re:ℂ)) f (nhds z.re), from filter.tendsto.comp hr (continuous.tendsto (complex.continuous_of_real) z.re), have hi2 : filter.tendsto (λ z:ℂ, (z.im:ℂ)) f (nhds z.im), from filter.tendsto.comp hi (continuous.tendsto (complex.continuous_of_real) z.im), have _ := tendsto_add hr2 (tendsto_mul hi2 (@tendsto_const_nhds _ _ _ complex.I _)), by rw [funext complex.re_add_im, complex.re_add_im] at this; rw [← (filter.map_id : _ = f)]; exact this⟩ example (f : filter ℂ) (hf : cauchy f) : ∃ x, f ≤ nhds x := let ⟨xr, hxr⟩ := complete_space.complete (cauchy_map complex.uniform_continuous_re hf) in let ⟨xi, hxi⟩ := complete_space.complete (cauchy_map complex.uniform_continuous_im hf) in ⟨⟨xr,xi⟩, (complex.filter_le_iff _ _).2 ⟨hxr, hxi⟩⟩

#### Kenny Lau (Oct 05 2018 at 00:12):

@Andreas Swerdlow

#### Mario Carneiro (Oct 05 2018 at 00:18):

I think there should be another way to say this in terms of the product topology

#### Mario Carneiro (Oct 05 2018 at 00:19):

That is, this should follow from the fact that C is homeomorphic to R x R with `re`

and `im`

as the projections

#### Kenny Lau (Oct 05 2018 at 00:20):

is this a fact yet? and will that be easier to use?

#### Mario Carneiro (Oct 05 2018 at 00:21):

that remains to be seen

#### Mario Carneiro (Oct 05 2018 at 00:21):

I don't think we have homeos yet (@Patrick Massot ? @Johannes Hölzl ?)

#### Mario Carneiro (Oct 05 2018 at 00:22):

But I think you can prove `filter_le_iff`

pretty easily if you do it on a product space with fst and snd

#### Mario Carneiro (Oct 05 2018 at 00:24):

And in any case what you really need is just plain continuity of the relevant functions and I think you already have that

#### Kenny Lau (Oct 05 2018 at 00:24):

I see

#### Mario Carneiro (Oct 05 2018 at 00:27):

wait, does C have the metric topology or the product topology by definition?

#### Kenny Lau (Oct 05 2018 at 06:58):

metric

#### Patrick Massot (Oct 05 2018 at 06:59):

Those are meant to be defeq

#### Kenny Lau (Oct 05 2018 at 07:00):

C isn't even defined to be a product

#### Patrick Massot (Oct 05 2018 at 07:01):

I meant that product topology and metric topology on a product of metric spaces are defeq, I don't really know how C is constructed in Lean

#### Mario Carneiro (Oct 05 2018 at 07:03):

It is possible to state this theorem using `(co)map`

on topologies. You want to say that the topology on C is induced by the map `\lam z, (z.re, z.im)`

, or coinduced by `\lam p, p.1 + I p.2`

#### Kenny Lau (Oct 05 2018 at 07:20):

I meant that product topology and metric topology on a product of metric spaces are defeq, I don't really know how C is constructed in Lean

are they?

#### Kenny Lau (Oct 05 2018 at 07:20):

isn't it a theorem?

#### Kenny Lau (Oct 05 2018 at 07:20):

that involves drawing a cirlce inside a square inside a circle inside a square?

#### Johan Commelin (Oct 05 2018 at 07:20):

that involves drawing a cirlce inside a square inside a circle inside a square?

Can Lean do that?

#### Patrick Massot (Oct 05 2018 at 07:21):

there is no circle in Lean. The product metric is defined as the max metric

#### Kenny Lau (Oct 05 2018 at 07:22):

oh well then it isn't defeq to the metric in C then

#### Kenny Lau (Oct 05 2018 at 07:22):

the metric in C is the circle metric

#### Mario Carneiro (Oct 05 2018 at 07:23):

the balls in C are circles because it uses the metric topology

#### Johan Commelin (Oct 05 2018 at 07:25):

Right, but not the product metric...

#### Mario Carneiro (Oct 05 2018 at 07:26):

if we wanted, we could define the topology on C as the product topology (or rather a mapping thereof), and then the typeclass would force us to prove this theorem

#### Mario Carneiro (Oct 05 2018 at 07:27):

but given that C has no pre-existing topology on it, it seems okay to just use the metric topology as the definition; but this means that we don't get any help with the homeo proof

#### Kenny Lau (Oct 05 2018 at 07:28):

I mean, my filter lemma *is* the homeomorphism

#### Patrick Massot (Oct 05 2018 at 07:28):

I don't think we have homeos yet (Patrick Massot** ? Johannes Hölzl ?)

This is not in mathlib, mostly because I don't know whether it should use the category theory stuff or be as in https://github.com/PatrickMassot/lean-scratchpad/blob/master/src/homeos.lean

#### Mario Carneiro (Oct 05 2018 at 07:31):

no categories in the definition

#### Mario Carneiro (Oct 05 2018 at 07:31):

it should be 100% topology

#### Patrick Massot (Oct 05 2018 at 07:31):

do you want me to PR that file then?

#### Mario Carneiro (Oct 05 2018 at 07:32):

I don't see why not... I will leave the merging to Johannes though since he's been involved more

#### Kenny Lau (Oct 05 2018 at 07:35):

I really think the circle metric is the right one

#### Kenny Lau (Oct 05 2018 at 07:35):

hmm, never mind

#### Mario Carneiro (Oct 05 2018 at 07:39):

The circle *metric* is certainly the right one, but I wonder if the *topology* should be defined using something like `comap re \sqcap comap im`

#### Mario Carneiro (Oct 05 2018 at 07:41):

which will make your filter theorem essentially by definition, and the bulk of that proof will be transferred to the construction of the metric_space instance

Last updated: May 12 2021 at 08:14 UTC