## Stream: maths

### Topic: Convergence uniform in one argument

#### Yury G. Kudryashov (Nov 20 2019 at 16:03):

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

#### Mario Carneiro (Nov 20 2019 at 16:05):

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

#### 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).

#### Mario Carneiro (Nov 20 2019 at 16:16):

what is a there?

#### Yury G. Kudryashov (Nov 20 2019 at 16:17):

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

#### Mario Carneiro (Nov 20 2019 at 16:17):

oh, nhds a should be the limit filter on x

#### Mario Carneiro (Nov 20 2019 at 16:20):

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

#### 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.

#### 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?

#### Yury G. Kudryashov (Nov 20 2019 at 16:48):

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

#### 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)


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