An interesting maths proof (to me anyway).

This is a comment I left on a blog but the comment box had no preview button and my comment came out kinda mangled, so I'm posting it here.

First of all, it's a long time since I proved anything so I may be wrong. Secondly, the markup is probably going to be terrible, there seems to be no preview button and I can't find wordpress's help section for markup. Finally, apologies if this is straying too far from the original idea of proof automation but I think this answers the question of whether this is true for Complex also. I can't really claim that this proof is discoverable by pattern matching as it's not really an epsilon-delta proof. That said, if I haven't made a mistake, the problem becomes "easy" if you consider a compactification of R and maybe looking at compactifications is a reasonable strategy for theorem provers.

Anyway, I think you can capture all of the fiddly parts and the proof-by-contradiction inside the Heine-Borel Theorem instead of using the Baire Category Theorem, which seems to be a bit more heavy-weight.

The essence is to show that for any δ > 0, there is a single N_δ such that |f(nX)| < δ for X ∈ [0,1] and n > N_δ. The conclusion follows from the fact that any Real > N_δ is something in [0,1] times an integer at least as big as N and therefore |f| will be < δ for this Real too.

Let X ∈ Real. We are given that f(nX) -> 0 as n -> ∞. More formally, ∀ δ > 0, ∀ X ∈ Real, ∃ N_δ,X ∈ Natural such that |f(nX)| < δ ∀ n > N_δ,X. Since f(X) is continuous there is an open set, O_δ,X containing X such that |f(N_δ,X y)| < δ ∀ y ∈ O_δ,X (it is the inverse image of (-δ, δ)).

For a fixed δ, {O_δ,X: X ∈ [0,1]} gives us an open cover of [0,1] and Heine-Borel tells us that there is a finite subcover. This means we have a finite set of O_δ,X, each with an N_δ,X and we can take the maximum N_δ,X and call it N_δ. This is a Natural such that |f(nX)| < δ ∀ X ∈ [0,1], ∀ n > N_δ.

Now let X ∈ Real, X > N_δ. Let N = [X]+1, where [] is the greatest integer function and let θ = X/N. Note that θ ∈ [0,1] and N > N_δ. So |f(Nθ)| < δ. That is, |f(X)| < δ.

So all you need is the compactness of [0,1] and the fact that you can generate all of Real+ from [0,1] and multiplication by Natural. So it seems that is true for Complex or Real^N etc. where you take x -> ∞ to mean |x| -> ∞ and you use [-1,1] instead of [0,1].

If Real itself was compact you could skip the scaling step entirely. I think rephrasing the question in terms of Real ∪ {-∞, ∞} makes it almost trivial but I must admit I'm going beyond what I can remember from my student days, I expect someone will tell me that rephrasing it like that causes something else to break.

I think it would be reasonable for a theorem prover to start by choosing a δ to aim for and use continuity to construct the cover of Real from the inverse images of (-δ, -δ). It would get stuck then and I don't know whether there is a reasonable automated bridge to the solution from there.