## 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 :=

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

I see

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

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

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

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