Yury G. Kudryashov (Nov 20 2019 at 16:03):
Hi, do we have a special name for converges to as uniformly in ? 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):
Yury G. Kudryashov (Nov 20 2019 at 16:17):
. Actually, we can use any other filter instead of
Mario Carneiro (Nov 20 2019 at 16:17):
nhds a should be the limit filter on
Mario Carneiro (Nov 20 2019 at 16:20):
yeah, this looks like a good definition. Perhaps
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):
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
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
analysis.complex.exponential, but maybe there are other instances scattered around.
Last updated: May 06 2021 at 18:20 UTC