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.

## 4 comments:

Not sure I completely understand your argument. First, don't you get an open cover of (0,1] rather than [0,1] as you claim (as the argument doesn't apply to x=0)? Secondly, when you construct your open intervals, they work for N_{delta,x} but not for every n>N_{delta,x}, and it seems to me that you need that later. I'd be quite surprised if compactness was enough, as it's such a standard application of the Baire category theorem.

I didn't read through all the proof, but the first paragraph ("The essence...") seems suspect to me. You want to prove that for any δ > 0, there is a single Nδ such that |f(nX)| < δ for X ∈ [0,1] and n > Nδ. This would imply that f(X) is arbitrarily small (and so would vanish) on the whole positive axis, not only for X big enough.

Andrea

Gowers,

thanks, they do seem to be 2 real problems. I'll see if I can fix things or find a counter-example

Andrea,

I'm not sure if I follow but if I had said nf(X) < δ ∀ n > N_δ then that would make f(X) arbitrarily small but the multiplication is inside the f() so I don't think I'm implying that f(X) vanishes.

Post a Comment