Zulip Chat Archive

Stream: maths

Topic: Convergence uniform in one argument


view this post on Zulip Yury G. Kudryashov (Nov 20 2019 at 16:03):

Hi, do we have a special name for f(x,y)f(x, y) converges to g(y)g(y) as x...x\to... uniformly in yy? I probably can define it using uniformity and comap but I'd prefer to avoid reinventing the wheel.

view this post on Zulip Mario Carneiro (Nov 20 2019 at 16:05):

I don't think so. What definition are you thinking?

view this post on Zulip Yury G. Kudryashov (Nov 20 2019 at 16:16):

Should be something like tendsto (λ p, (g p.2, f p.1 p.2)) ((nhds a).comap prod.snd) uniformity (not tested).

view this post on Zulip Mario Carneiro (Nov 20 2019 at 16:16):

what is a there?

view this post on Zulip Yury G. Kudryashov (Nov 20 2019 at 16:17):

xax\to a. Actually, we can use any other filter instead of nhds a.

view this post on Zulip Mario Carneiro (Nov 20 2019 at 16:17):

oh, nhds a should be the limit filter on x

view this post on Zulip Mario Carneiro (Nov 20 2019 at 16:20):

yeah, this looks like a good definition. Perhaps tendsto_uniformly?

view this post on Zulip Yury G. Kudryashov (Nov 20 2019 at 16:23):

Maybe I'll PR it later. Now I'm trying to formalize rotation numbers of circle homeomorphisms without adding things not required for this task.

view this post on Zulip Sebastien Gouezel (Nov 20 2019 at 16:33):

Maybe we should first do the universal cover, and the lift of a map to the universal cover -- or are you planning to just do the specific case of lifting circle maps to the real line?

view this post on Zulip Yury G. Kudryashov (Nov 20 2019 at 16:48):

@Sebastien Gouezel I'd take a shortcut for now, and work with the lifts.

view this post on Zulip Yury G. Kudryashov (Nov 20 2019 at 16:49):

Something like

structure circle_deg1 : Type :=
(to_fun : End )
(mono' : monotone to_fun)
(deg1' :  x, to_fun (x + 1) = to_fun x + 1)

view this post on Zulip Sebastien Gouezel (Nov 20 2019 at 17:13):

This makes sense (maybe replacing monotone with strict_mono, and adding continuity). I don't know if we already have the circle as a compact topological space in mathlib. I am aware of angle in analysis.complex.exponential, but maybe there are other instances scattered around.


Last updated: May 06 2021 at 18:20 UTC