Erdős Problem 422

[rao107]

Adds Erdős Problem 422.

The question on the function's behavior felt a bit vague, so I elected to not add it.

[Paul-Lez]

Here I think it would be interesting to add two statements:

1. The question of the surjectivity of f (seems to be open)
2. The question of whether the sequence f must eventually terminate (presumably not? admittedly I haven't thought too much about whether or not this is hard to prove)

[rao107]

Those sound like good ideas. I'll also add in a question of the function's growth rate since that's open as well.

[rao107]

Hey, I added your suggestions but I had a bit of trouble with the second.

For it, I removed the partial definition for f and defined the function with sorry. I don't think this is what you had in mind when you suggested it so I'd welcome any other ways to define that f must eventually terminate.

[smmercuri]

Perhaps by termination @Paul-Lez meant whether f becomes stationary at some point? I.e., does there exist m and N for which f n = m for all n larger than N. Termination can be quite surprising in this sense, see for example the Goodstein sequence which eventually decreases and terminates at 0.

The other interpretation of termination here is whether one reaches a point at which f n cannot be defined (e.g, if n - f (n - 1) < 0), but I think this sense is already captured in the definition.

[rao107]

Apologies for the delay! I've added another variant for f eventually becoming stationary. 🙂

[callesonne]

LGTM after these comments, thanks a lot!

[callesonne]

Suggested change

	theorem erdos_422.variants.growth_rate : f =O[atTop] (answer(sorry) : ℕ+ → ℕ+) := by
	theorem erdos_422.variants.growth_rate :
	(fun n ↦ (f n : ℝ)) =O[atTop] (answer(sorry) : ℕ+ → ℝ) := by

[callesonne]

Suggested change

	instance : Norm ℕ+ where
	norm n := n

I'm not sure if you want to add this as a global instance. For example there seems to be no Norm instance on ℕ in mathlib (that I can find). I believe the reason for this is that you don't want it as an instance as a priori there are multiple possible norms (such as the p-adic norms as well). I'm assuming you are adding this in order to talk about the growth rate below, but what you can do is just to view f as a function valued in R for that statement. See my suggestion below.

[rao107]

Oh, I didn't realize I could do that! Thank you so much!