Convergence uniform in one argument

Stream: maths

[Yury G. Kudryashov]

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]

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

[Yury G. Kudryashov]

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

[Mario Carneiro]

what is a there?

[Yury G. Kudryashov]

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

[Mario Carneiro]

oh, nhds a should be the limit filter on x

[Mario Carneiro]

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

[Yury G. Kudryashov]

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]

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]

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

[Yury G. Kudryashov]

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]

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.