Uniform convergence mean we can swap limits!

Stream: Codewars

[Patrick Lutz]

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]

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

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]

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]

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]

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

[Patrick Lutz]

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

[Patrick Lutz]

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]

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

[Patrick Lutz]

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]

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]

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]

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]

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

[Patrick Lutz]

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

[Patrick Lutz]

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]

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]

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]

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]

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]

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]

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

[Patrick Lutz]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

But in real life do these things exist?

[Kevin Buzzard]

Or is it just in calc 1?

[Patrick Lutz]

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]

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]

I'll write a solution soon

[Patrick Lutz]

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

[Patrick Lutz]

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]

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

[Patrick Lutz]

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]

Should I do something with it?

[Kevin Buzzard]

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]

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

[Jason KY.]

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

But now I see that I'm terribly wrong!

[Jason KY.]

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]

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]

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]

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]

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]

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

[Patrick Lutz]

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]

Should I put it on github or something?

[Donald Sebastian Leung]

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]

@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]

@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