complex forms uniform space

Stream: maths

[Kenny Lau]

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]

@Andreas Swerdlow

[Kenny Lau]

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]

complete proof

[Andreas Swerdlow]

Wow thank you!

[Andreas Swerdlow]

@Joseph Corneli look what Kenny did

[Kenny Lau]

I should probably extract a lemma

[Mario Carneiro]

that proof looks like a good advertisement for bundling continuous functions

[Mario Carneiro]

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]

another thing to refactor :P

[Kenny Lau]

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]

@Andreas Swerdlow

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

that remains to be seen

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

I see

[Mario Carneiro]

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

[Kenny Lau]

metric

[Patrick Massot]

Those are meant to be defeq

[Kenny Lau]

C isn't even defined to be a product

[Patrick Massot]

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]

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]

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]

isn't it a theorem?

[Kenny Lau]

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

[Johan Commelin]

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

Can Lean do that?

[Patrick Massot]

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

[Kenny Lau]

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

[Kenny Lau]

the metric in C is the circle metric

[Mario Carneiro]

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

[Johan Commelin]

Right, but not the product metric...

[Mario Carneiro]

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]

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]

I mean, my filter lemma is the homeomorphism

[Patrick Massot]

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]

no categories in the definition

[Mario Carneiro]

it should be 100% topology

[Patrick Massot]

do you want me to PR that file then?

[Mario Carneiro]

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

[Kenny Lau]

I really think the circle metric is the right one

[Kenny Lau]

hmm, never mind

[Mario Carneiro]

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]

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