Zulip Chat Archive

Stream: Codewars

Topic: Uniform convergence mean we can swap limits!


view this post on Zulip Patrick Lutz (Jun 10 2020 at 00:35):

I have a question about the kata titled "Uniform convergence mean [sic] we can swap limits!" I successfully completed the kata, but I believe that the statement that the instructions claim is being proved does not quite make sense and arguably does not agree with the formal statement in the kata.

Here is the statement from the instructions of the kata (mildly paraphrased): If fn\langle f_n \rangle is a sequence of functions RR\R \to \R which converge uniformly to a function gg then for any aa, limnlimxafn(x)=limxalimnfn(x)\lim_{n \to \infty}\lim_{x \to a} f_n(x) = \lim_{x \to a}\lim_{n \to \infty} f_n(x). The problem is basically that there is no reason to assume that the limits limxafn(x)\lim_{x \to a}f_n(x) or limxag(x)\lim_{x \to a}g(x) exist.

The formal statement in the kata explicitly assumes that limxag(x)\lim_{x \to a}g(x) exists and implicitly assumes the limits limxafn(x)\lim_{x \to a}f_n(x) do all exist and that limxafn(x)=fn(a)\lim_{x \to a}f_n(x) = f_n(a). With these assumptions, the statement basically becomes trivial; the only thing to show is that limxag(x)=g(a)\lim_{x \to a}g(x) = g(a). And it doesn't require uniform convergence of the fnf_n's to gg, just convergence at aa.

If you don't assume the limits exist then the statement doesn't make sense and it is not possible to prove that they exist even if you assume that limxag(x)\lim_{x \to a}g(x) exists. (Of course, if you assume that limxafn(x)\lim_{x \to a}f_n(x) exists for each nn then you can prove that limxag(x)\lim_{x \to a}g(x) also exists but this is not what the kata asks you to do.)

view this post on Zulip Patrick Lutz (Jun 10 2020 at 00:40):

In summary: I think the only way I can think of to interpret the statement in the kata's instructions so that it's not false or trivial is as "a uniformly convergent sequence of functions which are all continuous at a point converge to something which is also continuous at that point." But this is not the formal statement found in the kata.

view this post on Zulip Jason KY. (Jun 10 2020 at 11:47):

Sorry about the confusion! I see what you mean!
I just wanted to make a simple kata for an exercise found on my lecture notes but I guess I should pay more attention to how I phrase things. How would you describe the description? I will update it

view this post on Zulip Patrick Lutz (Jun 10 2020 at 20:21):

I think I now understand the root of the problem with this kata. The problem is that the formal definition of limit given in the kata is not the usual one and it makes the kata more trivial than it's supposed to be

view this post on Zulip Patrick Lutz (Jun 10 2020 at 20:22):

The formal definition of limit of a function at a point given in the kata is

limxaf(x)=l    ϵ>0δ>0xxa<δ    f(x)l<ϵ.\lim_{x \to a}f(x) = l \iff \forall \epsilon > 0\, \exists \delta > 0\, \forall x\, | x - a | < \delta \implies |f(x) - l| < \epsilon.

view this post on Zulip Patrick Lutz (Jun 10 2020 at 20:22):

This definition has the feature that if limxaf(x)\lim_{x \to a}f(x) exists then it's equal to f(a)f(a)

view this post on Zulip Patrick Lutz (Jun 10 2020 at 20:23):

But that's not implied by the usual definition of limit

view this post on Zulip Patrick Lutz (Jun 10 2020 at 20:23):

The usual definition is

limxaf(x)=l    ϵ>0δ>0x0<xa<δ    f(x)l<ϵ.\lim_{x \to a}f(x) = l \iff \forall \epsilon > 0\, \exists \delta > 0\, \forall x\, 0 < | x - a | < \delta \implies |f(x) - l| < \epsilon.

view this post on Zulip Patrick Lutz (Jun 10 2020 at 20:24):

see, e.g., Wikipedia: https://en.wikipedia.org/wiki/Limit_of_a_function#Functions_of_a_single_variable

view this post on Zulip Patrick Lutz (Jun 10 2020 at 20:24):

Under the standard definition, if e.g. ff has a jump discontinuity at aa then it is possible for limxaf(x)\lim_{x \to a}f(x) to exist but to not equal f(a)f(a)

view this post on Zulip Patrick Lutz (Jun 10 2020 at 20:25):

Under the usual definition of limit, the statement that limits commute when you have uniform convergence is not trivial and the uniform convergence is really required

view this post on Zulip Patrick Lutz (Jun 10 2020 at 20:28):

Although the statement of the kata is no longer correct: it is possible to have a uniformly converging sequence of functions fn\langle f_n \rangle converging to a function gg where the limit of each fnf_n at aa exists and the limit of gg at aa exists, but limninftyfn(a)\lim_{n \to infty} f_n(a) is not equal to limxag(x)\lim_{x \to a}g(x) (it is equal to g(a)g(a) of course, but the point is that g(a)g(a) may not be equal to limxag(x)\lim_{x \to a}g(x))

view this post on Zulip Patrick Lutz (Jun 10 2020 at 20:32):

The right statement is to use the standard definition of limit of a function at a point and then say

If fn\langle f_n\rangle is a sequence of functions RR\mathbb{R} \to \mathbb{R} which converges uniformly to a function gg and if limxafn(x)\lim_{x \to a}f_n(x) exists for each nn then limxag(x)\lim_{x \to a}g(x) exists and is equal to limnlimxafn(x)\lim_{n \to \infty}\lim_{x \to a}f_n(x).

view this post on Zulip Patrick Lutz (Jun 10 2020 at 20:32):

However, this statement does not match the formal statement in the kata

view this post on Zulip Patrick Lutz (Jun 10 2020 at 20:33):

Anyway, I now see that some of the stuff in my original post in this thread is pretty confused

view this post on Zulip Patrick Lutz (Jun 10 2020 at 20:34):

Basically I somehow didn't notice that the kata's definition of limit of a function at a point is wrong and I started also using this wrong definition

view this post on Zulip Patrick Lutz (Jun 10 2020 at 20:39):

One solution would be to amend the kata's description to explain that the formal definition of limit used in the kata is not the standard one

view this post on Zulip Patrick Lutz (Jun 10 2020 at 20:40):

And to make it clear that the kata's formal statement does not have much to do with uniform convergence and does not say that limits commute

view this post on Zulip Patrick Lutz (Jun 10 2020 at 20:41):

I don't know if it's possible to change the kata itself (and not just the description). If so, I would change it to the statement above

view this post on Zulip Patrick Lutz (Jun 10 2020 at 20:41):

Patrick Lutz said:

The right statement is to use the standard definition of limit of a function at a point and then say

If fn\langle f_n\rangle is a sequence of functions RR\mathbb{R} \to \mathbb{R} which converges uniformly to a function gg and if limxafn(x)\lim_{x \to a}f_n(x) exists for each nn then limxag(x)\lim_{x \to a}g(x) exists and is equal to limnlimxafn(x)\lim_{n \to \infty}\lim_{x \to a}f_n(x).

This one

view this post on Zulip Kevin Buzzard (Jun 10 2020 at 20:46):

If you change the kata if l is breaks solutions, which isn't the end of the world. Another approach is that you just write a new Kata! Probably Jason will post it and credit you if you don't have 300 rep on codewars

view this post on Zulip Patrick Lutz (Jun 10 2020 at 20:47):

Btw, does what I've said now make sense? I want to make sure I'm not saying crazy stuff here

view this post on Zulip Patrick Lutz (Jun 10 2020 at 20:48):

I currently have 141 rep, maybe in another week I can get to 300

view this post on Zulip Kevin Buzzard (Jun 10 2020 at 20:50):

I never know what the definition of a limit is. My impression is that it's the thing about x not being allowed to be a in a first course on analysis when you're learning about differentiability and then everyone forgets this soon after.

view this post on Zulip Patrick Lutz (Jun 10 2020 at 20:50):

Yeah, I mean it seems useful to be able to talk about jump discontinuities in a non-awkward way

view this post on Zulip Kevin Buzzard (Jun 10 2020 at 20:54):

But in real life do these things exist?

view this post on Zulip Kevin Buzzard (Jun 10 2020 at 20:54):

Or is it just in calc 1?

view this post on Zulip Patrick Lutz (Jun 10 2020 at 21:00):

I spent several weeks last fall trying to build a function with a discontinuity at a single point which had some other features (although I wasn't successful). But I work in computability so it was a function on a subspace of {0,1}N\{0, 1\}^\mathbb{N}

view this post on Zulip Patrick Lutz (Jun 10 2020 at 21:10):

Okay, I've written a formal version of the statement I wrote earlier

import data.real.basic

/- We first define uniform convergence -/
def unif_convergence (f :     ) (g :   ) :=
 ε > 0,  N : ,  n  N,  x : , abs (f n x - g x) < ε

/- Use the notation f → g to denote that the sequence fₙ converges uniformly to g
    You can type → by writing \hom -/
notation f `` g := unif_convergence f g

/- We also define the notion of the limit of a function ℝ → ℝ at a point -/
def fun_limit (f :   ) (a l) :=
 ε > 0,  δ > 0,  x : , x  a  abs (x - a) < δ  abs (f x - l) < ε

/- And the notion of the limit of a sequence -/
def seq_limit (f :   ) (l) :=
 ε > 0,  N : ,  n  N, abs (f n - l) < ε

/- If fₙ converges uniformly to g and if lim_{x → a} fₙ(x) = lₙ for
    each n then lim_{x → a} g(x) exists and is equal to lim_{n → ∞} lₙ -/
theorem limits_commute (f :     ) (g :   ) (l :   ) (a : ) :
    (f  g)  ( n, fun_limit (f n) a (l n)) 
    ( l', fun_limit g a l'  seq_limit l l') := sorry

view this post on Zulip Patrick Lutz (Jun 10 2020 at 21:10):

I'll write a solution soon

view this post on Zulip Patrick Lutz (Jun 10 2020 at 21:14):

Although maybe having to prove the limit exists makes the kata a lot harder

view this post on Zulip Patrick Lutz (Jun 10 2020 at 21:14):

you could also just assume limxag(x)\lim_{x \to a} g(x) exists and show it's equal to limnlimxafn(x)\lim_{n \to \infty}\lim_{x \to a} f_n(x)

view this post on Zulip Patrick Lutz (Jun 10 2020 at 21:14):

maybe that's more in the spirit of the original kata

view this post on Zulip Patrick Lutz (Jun 10 2020 at 21:49):

Kevin Buzzard said:

If you change the kata if l is breaks solutions, which isn't the end of the world. Another approach is that you just write a new Kata! Probably Jason will post it and credit you if you don't have 300 rep on codewars

I now have a completed solution for the easier version where limxag(x)\lim_{x \to a}g(x) is assumed to exist.

view this post on Zulip Patrick Lutz (Jun 10 2020 at 21:50):

Should I do something with it?

view this post on Zulip Kevin Buzzard (Jun 10 2020 at 21:56):

Good question! If we can't persuade @Jason KY. to take it on, I'll upload it after the weekend (I have a grant proposal deadline :-/ )

view this post on Zulip Patrick Lutz (Jun 10 2020 at 21:58):

Okay, I'll probably complete the "harder" version later today

view this post on Zulip Jason KY. (Jun 11 2020 at 16:24):

Patrick Lutz said:

The usual definition is

limxaf(x)=l    ϵ>0δ>0x0<xa<δ    f(x)l<ϵ.\lim_{x \to a}f(x) = l \iff \forall \epsilon > 0\, \exists \delta > 0\, \forall x\, 0 < | x - a | < \delta \implies |f(x) - l| < \epsilon.

Ah, I see. I was under the impression that those two definitions are equivalent since I proved something similar to it a while ago.

view this post on Zulip Jason KY. (Jun 11 2020 at 16:25):

But now I see that I'm terribly wrong!

view this post on Zulip Jason KY. (Jun 11 2020 at 16:35):

Patrick Lutz said:

One solution would be to amend the kata's description to explain that the formal definition of limit used in the kata is not the standard one

I have now updated the description to say that it is not using the standard definition.

view this post on Zulip Patrick Lutz (Jun 11 2020 at 20:43):

Jason KY. said:

Ah, I see. I was under the impression that those two definitions are equivalent since I proved something similar to it a while ago.

Yeah, they're the same if all you care about is the case limxaf(x)=f(a)\lim_{x \to a}f(x) = f(a) but not the same in general.

view this post on Zulip Patrick Lutz (Jun 11 2020 at 20:46):

By the way, I have now written a proof in Lean that if fn\langle f_n \rangle converges uniformly to gg and limxafn(x)\lim_{x \to a}f_n(x) exists for each nn then limxag(x)\lim_{x \to a}g(x) also exists, which is the first half of the statement I mentioned above (the second half I formalized in Lean yesterday).

view this post on Zulip Patrick Lutz (Jun 12 2020 at 03:26):

I'm trying to make two kumites in codewars for the things I formalized (limxag(x)\lim_{x \to a}g(x) exists and if it exists then it's equal to limnlimxafn(x)\lim_{n \to \infty}\lim_{x \to a} f_n(x)) so that they can be converted to kata. But it seems like latex doesn't work in the descriptions of kumite? I found this about adding latex to the description of kata: https://github.com/Codewars/codewars.com/issues/1527. But it doesn't seem to work for kumite. Does anyone know anything about this?

view this post on Zulip Donald Sebastian Leung (Jun 12 2020 at 11:57):

Not sure about kumite, you may wish to ask kazk about on the issue you linked above

Also, even though the button for converting kumite to kata is present, I wouldn't recommend it because 1) kumite are visible to the public which means that solvers may get a glimpse of the full solution before it gets converted into a kata and 2) if you don't yet have 300 honor, the server might reject your request anyway.

view this post on Zulip Patrick Lutz (Jun 12 2020 at 15:25):

@Donald Sebastian Leung Okay, thanks for the advice. I've added a comment on the github issue.

view this post on Zulip Patrick Lutz (Jun 12 2020 at 15:25):

Also, does anyone on here want to post the kata themselves (or perhaps two separate kata)? If so, what should I do to send it?

view this post on Zulip Patrick Lutz (Jun 12 2020 at 15:25):

Should I put it on github or something?

view this post on Zulip Donald Sebastian Leung (Jun 13 2020 at 02:50):

Also, does anyone on here want to post the kata themselves (or perhaps two separate kata)? If so, what should I do to send it?

Should I put it on github or something?

@Patrick Lutz You could PM or email the person you would like to host the kata on your behalf and share your code with them privately. I personally don't feel very comfortable publishing others' content since it gives me free points for someone else's work, but I'm sure there are others here who are happy to help.

In any case, I would strongly recommend against publicizing your solution on GitHub if you intend to make it a kata, since others could then just copy/paste your solution and submit it for free points.

view this post on Zulip Patrick Lutz (Jun 13 2020 at 06:39):

@Donald Sebastian Leung It hadn't even really occurred to me that people would try to cheat on codewars (after all, what's the point?) but I will certainly follow your advice.

view this post on Zulip Patrick Lutz (Jul 05 2020 at 05:52):

@Jason KY. @Kevin Buzzard I now have enough honor to create kata, so I've added a new kata here which uses the more standard definition of limit. Please let me know if you have any feedback


Last updated: May 08 2021 at 22:13 UTC