Identifying endpoints of [0, 1]

Stream: Is there code for X?

[David Loeffler]

Is there a proof anywhere in the library that the quotient of the real interval [0, 1], as a topological space, by the equivalence relation identifying 0 with 1 is homeomorphic to unit_add_circle? I needed this for some results on Fourier series, but it feels like the sort of thing which must have come up before.

[Junyan Xu]

I haven't seen it; if it indeed doesn't exist, you may use docs#continuous.homeo_of_equiv_compact_to_t2 with docs#continuous_quot_lift

[Matt Diamond]

docs#add_circle.equiv_Ico might be relevant, but it's not Icc

[David Loeffler]

Matt Diamond said:

docs#add_circle.equiv_Ico might be relevant, but it's not Icc

... and it's also not a homeomorphism.

[Kevin Buzzard]

Probably @Oliver Nash is your only other hope.:-)

[David Loeffler]

Kevin Buzzard said:

Probably Oliver Nash is your only other hope.:-)

It's not a difficult result; I have a proof coded up (which has just got substantially shorter thanks to @Junyan Xu's suggestions -- thanks!). I'm mostly asking because I don't want to go through the rigmarole of making a mathlib PR if someone else has done this already.

[Yaël Dillies]

Are you sure you need this result per se? To me it sounds like the kind of situation where an alternative argument would be much less painful.

[Yaël Dillies]

So maybe un-#xy :smile:

[Oliver Nash]

I only have a little time for Lean at the moment but this result is certainly worth having (even bearing in mind Yaël's point). Please ping me if you do PR it and also prove it for add_circle T rather than just for unit_add_circle.

[David Loeffler]

Yaël Dillies said:

Are you sure you need this result per se? To me it sounds like the kind of situation where an alternative argument would be much less painful.

Yaël: actually this was the alternative argument. What I need is to show that, given a continuous function on [0, 1] with f 0 = f 1 (e.g. the Bernoulli polynomial B_k(x) for k != 1), I can make from it a continuous function on unit_add_circle. My first attempt was to extend f to a periodic function on ℝ by composing with int.frac, show that this is continuous, and then apply continuous_quot_lift. But that involved a great deal of rather painful mucking around with continuous_within_at to show continuity at the bad points.

[Yaël Dillies]

My question then is: How did you end up with this function on [0, 1] in the first place?

[David Loeffler]

@Yaël Dillies I "ended up" with this function because it is essential to the proof I am trying to formalise.

In more detail: I have a polynomial B(x) on ℝ with B(0) = B(1), and I want to consider the unique function P(x) which is periodic with period 1, and satisfies P(x) = B(x) for x in [0, 1]. The reason I want to do this is because -- in the case when B is the k-th Bernoulli polynomial -- it happens to be the case that the n-th Fourier coefficient of P(x) is (constant) / n^k, and thus if you can show that the Fourier series of P converges pointwise to P, you get values of the Riemann zeta function (and in fact of all Dirichlet L-functions, by taking weighted sums of values at rationals in [0, 1].

[Yaël Dillies]

That still doesn't explain why this is a function on [0, 1]. Let me mention @Yury G. Kudryashov's work on the rotation number: docs#circle_deg1_lift.
Instead of having a function from the circle, he takes a function from ℝ with "gluing" hypotheses. The punchline is that no gluing actually happens, so there's no bad point.

[David Loeffler]

I think you are missing my point here: my starting polynomial B(x) is not a periodic function -- periodic polynomials being in rather short supply -- and thus doesn't satisfy any "gluing hypotheses", so P(x) is really different from B(x) and the bad point is genuinely bad.
(No offence, but I have the impression that you are rushing into telling me that my approach is wrong, without having understood what I am trying to do.)

[Yaël Dillies]

Ah, this is the reason :^)

[David Loeffler]

This is now PR # 17889.

[Eric Wieser]

If you remove the space then Zulip will linkify it