4.2 Structured proofs

That was a lot of preliminary stuff, but it’s very important to understand definitions before you move on to proofs. Now, let’s prove that en0e^{-n} \to 0. What, specifically, do we need to prove? That for all ϵ>0\epsilon > 0, there is an integer NN such that en<ϵ\lvert e^{-n}\rvert < \epsilon for all n>Nn > N. So, we need to start with “Let ϵ>0\epsilon> 0” (this is how a lot of proofs start):

Proof. Let ϵ>0\epsilon> 0, and let N=logϵN = \lceil -\log \epsilon\rceil. Then for all n>Nn > N, en=enen is always positive<eNen is strictly decreasing=exp{logϵ}Definition of Nelogϵen decreasing=ϵ\begin{alignat*}{2} \lvert e^{-n}\rvert &= e^{-n} &\hspace{4em}& e^{-n} \text{ is always positive} \\ &< e^{-N} && e^{-n} \text{ is strictly decreasing}\\ &= \exp\{-\lceil-\log \epsilon\rceil\} && \text{Definition of } N \\ &\le e^{\log \epsilon} && e^{-n} \text{ decreasing} \\ &= \epsilon \end{alignat*} Thus, xn0\mathbf{x}_n \to 0.

The left column is a series of statements or claims; this is the main logic of what’s happening in the proof. Chaining all the lines together, we have en<ϵ\lvert e^{-n}\rvert < \epsilon. Thus, we’ve done what we needed to do: given any positive ϵ\epsilon, I can find always find an NN that meets the requirement. Thus, en0e^{-n} \to 0 by the definition of convergence.

The right column provides the justification for each step. For example, in the fourth line we claimed that exp{logϵ}elogϵ\exp\{-\lceil-\log \epsilon\rceil\} \le e^{\log \epsilon}. How do we know that this is true? Well, xx\lceil x \rceil \ge x since the operation involves rounding up, and exe^{-x} is a decreasing function of xx. So by replacing the argument to exe^{-x} (i.e., logϵ\lceil-\log \epsilon\rceil) with something smaller (i.e., logϵ-\log \epsilon), the result must be larger (or equal, since logϵ-\log\epsilon could be an integer already).

How far to go with these justification depends on what the reader of the proof would likely consider obvious, and is therefore a judgment call. For example, we could include a proof of the fact that exe^{-x} is a decreasing function of xx, but in my judgment this is going off on a bit of a tangent that distracts from the main point of the proof. In a similar fashion, I didn’t even provide a justification for the final step, but to be really thorough, I could have added that exp()\exp() and log()\log() are inverse functions. In general, for the purposes of a course, you should err on the side of being very thorough and justifying every step. In a paper or thesis, however, going into this level of detail for every proof is probably unnecessary as the audience (other people with PhDs in statistics or biostatistics) will probably find many of the steps obvious and not requiring justification.

One final comment: as the above proof should hopefully make clear, a final proof does not describe one’s thought process in terms of how you arrived at the result. Clearly I didn’t know what I should set NN equal to until I’d worked through the math to solve for nn in the previous section. If you’re reading the proof for the first time, the line “let N=logϵN = \lceil -\log \epsilon\rceil” is going to seem mysterious; where did that come from? Keep in mind that we’re writing a proof, not a novel of self-discovery. The point is to construct an iron-clad, rigorous argument, not to communicate our thoughts and feelings and realizations. It might not be immediately obvious why I am letting N=logϵN = \lceil -\log \epsilon\rceil, but it should be completely obvious that I can set N=logϵN = \lceil -\log \epsilon\rceil. One can certainly write about the thought process and intuition behind the proof, but the place for this is outside the formal mathematical proof – we don’t want to mix formal logic with informal intuition.