Monday, July 28, 2008

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

Sunday, July 27, 2008

Nice beer

This is mostly just a note for myself, not knowing the first thing about beer and drinking less than a pint a month these days means my opinion may be "wrong" but I wanted to make a note of this beer so that I buy again next time I have a beer drinking opportunity.

While R<&iactute>ona was sleeping, I cooked some spicy tomatoey rib things (the butcher gave me ribs when I asked for belly and I found a recipe that seemed easy). Afterwards I had a bottle of quite nice beer. It's called Franziskaner (as in Fanciscan Monks I think) and is a weisse bier (funnily enough the photo on that page is the beer I drank so maybe it really is good). It was very easy to drink after my dinner.

Tuesday, July 22, 2008

I became a real parent today.

1 week after the birth of my second child I became a "real" parent. Ríona was in the buggy with her hand out, rubbing against things as she went. She rubbed against a dirty car tyre and got some nasty black stuff on her fingertips. I didn't want her to get that all over her clothes, so I did the only thing I could think of. I took out my hanky, spat on it a little and cleaned her.

Technically, the standard for "real" parenthood is to spit on a hanky and clean your child's face but that wasn't an option. I suppose I could have waited for her to rub her face with her dirty fingers. Maybe next time.