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