Zulip Chat Archive

Stream: maths

Topic: complex forms uniform space


view this post on Zulip 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 $ λ ε , ε, ,
λ 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 $ λ ε , ε, , λ 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 $ λ ε , ε, , λ 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

view this post on Zulip Kenny Lau (Oct 04 2018 at 23:00):

@Andreas Swerdlow

view this post on Zulip 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 $ λ ε , ε, ,
λ 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 $ λ ε , ε, , λ 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 $ λ ε , ε, , λ 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 $ λ ε , ε, , λ 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

view this post on Zulip Kenny Lau (Oct 04 2018 at 23:21):

complete proof

view this post on Zulip Andreas Swerdlow (Oct 04 2018 at 23:58):

Wow thank you!

view this post on Zulip Andreas Swerdlow (Oct 04 2018 at 23:59):

@Joseph Corneli look what Kenny did

view this post on Zulip Kenny Lau (Oct 05 2018 at 00:01):

I should probably extract a lemma

view this post on Zulip Mario Carneiro (Oct 05 2018 at 00:01):

that proof looks like a good advertisement for bundling continuous functions

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 05 2018 at 00:03):

another thing to refactor :P

view this post on Zulip 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 $ λ ε , ε, ,
λ 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 $ λ ε , ε, , λ 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 $ λ ε , ε, , λ 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 $ λ ε , ε, , λ 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⟩⟩

view this post on Zulip Kenny Lau (Oct 05 2018 at 00:12):

@Andreas Swerdlow

view this post on Zulip Mario Carneiro (Oct 05 2018 at 00:18):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 05 2018 at 00:20):

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

view this post on Zulip Mario Carneiro (Oct 05 2018 at 00:21):

that remains to be seen

view this post on Zulip Mario Carneiro (Oct 05 2018 at 00:21):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 05 2018 at 00:24):

I see

view this post on Zulip Mario Carneiro (Oct 05 2018 at 00:27):

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

view this post on Zulip Kenny Lau (Oct 05 2018 at 06:58):

metric

view this post on Zulip Patrick Massot (Oct 05 2018 at 06:59):

Those are meant to be defeq

view this post on Zulip Kenny Lau (Oct 05 2018 at 07:00):

C isn't even defined to be a product

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Oct 05 2018 at 07:20):

isn't it a theorem?

view this post on Zulip Kenny Lau (Oct 05 2018 at 07:20):

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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Oct 05 2018 at 07:21):

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

view this post on Zulip Kenny Lau (Oct 05 2018 at 07:22):

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

view this post on Zulip Kenny Lau (Oct 05 2018 at 07:22):

the metric in C is the circle metric

view this post on Zulip Mario Carneiro (Oct 05 2018 at 07:23):

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

view this post on Zulip Johan Commelin (Oct 05 2018 at 07:25):

Right, but not the product metric...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 05 2018 at 07:28):

I mean, my filter lemma is the homeomorphism

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 05 2018 at 07:31):

no categories in the definition

view this post on Zulip Mario Carneiro (Oct 05 2018 at 07:31):

it should be 100% topology

view this post on Zulip Patrick Massot (Oct 05 2018 at 07:31):

do you want me to PR that file then?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 05 2018 at 07:35):

I really think the circle metric is the right one

view this post on Zulip Kenny Lau (Oct 05 2018 at 07:35):

hmm, never mind

view this post on Zulip 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

view this post on Zulip 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