# Zulip Chat Archive

## Stream: Codewars

### Topic: Uniform convergence mean we can swap limits!

#### 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 $\langle f_n \rangle$ is a sequence of functions $\R \to \R$ which converge uniformly to a function $g$ then for any $a$, $\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 $\lim_{x \to a}f_n(x)$ or $\lim_{x \to a}g(x)$ exist.

The formal statement in the kata explicitly assumes that $\lim_{x \to a}g(x)$ exists and implicitly assumes the limits $\lim_{x \to a}f_n(x)$ do all exist and that $\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 $\lim_{x \to a}g(x) = g(a)$. And it doesn't require uniform convergence of the $f_n$'s to $g$, just convergence at $a$.

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 $\lim_{x \to a}g(x)$ exists. (Of course, if you assume that $\lim_{x \to a}f_n(x)$ exists for each $n$ then you can prove that $\lim_{x \to a}g(x)$ also exists but this is not what the kata asks you to do.)

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

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

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

#### Patrick Lutz (Jun 10 2020 at 20:22):

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

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

#### Patrick Lutz (Jun 10 2020 at 20:22):

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

#### Patrick Lutz (Jun 10 2020 at 20:23):

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

#### Patrick Lutz (Jun 10 2020 at 20:23):

The usual definition is

$\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.$

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

#### Patrick Lutz (Jun 10 2020 at 20:24):

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

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

#### 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 $\langle f_n \rangle$ converging to a function $g$ where the limit of each $f_n$ at $a$ exists and the limit of $g$ at $a$ exists, but $\lim_{n \to infty} f_n(a)$ is not equal to $\lim_{x \to a}g(x)$ (it is equal to $g(a)$ of course, but the point is that $g(a)$ may not be equal to $\lim_{x \to a}g(x)$)

#### 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 $\langle f_n\rangle$ is a sequence of functions $\mathbb{R} \to \mathbb{R}$ which converges uniformly to a function $g$ and if $\lim_{x \to a}f_n(x)$ exists for each $n$ then $\lim_{x \to a}g(x)$ exists and is equal to $\lim_{n \to \infty}\lim_{x \to a}f_n(x)$.

#### Patrick Lutz (Jun 10 2020 at 20:32):

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

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

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

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

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

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

#### 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 $\langle f_n\rangle$ is a sequence of functions $\mathbb{R} \to \mathbb{R}$ which converges uniformly to a function $g$ and if $\lim_{x \to a}f_n(x)$ exists for each $n$ then $\lim_{x \to a}g(x)$ exists and is equal to $\lim_{n \to \infty}\lim_{x \to a}f_n(x)$.

This one

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

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

#### Patrick Lutz (Jun 10 2020 at 20:48):

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

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

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

#### Kevin Buzzard (Jun 10 2020 at 20:54):

But in real life do these things exist?

#### Kevin Buzzard (Jun 10 2020 at 20:54):

Or is it just in calc 1?

#### 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\}^\mathbb{N}$

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

#### Patrick Lutz (Jun 10 2020 at 21:10):

I'll write a solution soon

#### Patrick Lutz (Jun 10 2020 at 21:14):

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

#### Patrick Lutz (Jun 10 2020 at 21:14):

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

#### Patrick Lutz (Jun 10 2020 at 21:14):

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

#### 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 $\lim_{x \to a}g(x)$ is assumed to exist.

#### Patrick Lutz (Jun 10 2020 at 21:50):

Should I do something with it?

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

#### Patrick Lutz (Jun 10 2020 at 21:58):

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

#### Jason KY. (Jun 11 2020 at 16:24):

Patrick Lutz said:

The usual definition is

$\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.

#### Jason KY. (Jun 11 2020 at 16:25):

But now I see that I'm terribly wrong!

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

#### 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 $\lim_{x \to a}f(x) = f(a)$ but not the same in general.

#### Patrick Lutz (Jun 11 2020 at 20:46):

By the way, I have now written a proof in Lean that if $\langle f_n \rangle$ converges uniformly to $g$ and $\lim_{x \to a}f_n(x)$ exists for each $n$ then $\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).

#### Patrick Lutz (Jun 12 2020 at 03:26):

I'm trying to make two kumites in codewars for the things I formalized ($\lim_{x \to a}g(x)$ exists and if it exists then it's equal to $\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?

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

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

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

#### Patrick Lutz (Jun 12 2020 at 15:25):

Should I put it on github or something?

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

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

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