Post Made Community Wiki by François G. Dorais
show/hide this revision's text 1

One of the simplest is the monotone convergence principle, that every bounded increasing sequence of rationals is convergent.

Along with Henry Towsner's example of the Ergodic theorem there is Doob's martingale convergence theorem and Lebesgue's theorem that every function of bounded variation is differentiable a.e.

However, if more information is known then this non-constructivity can be overcome. For example, with a martingale, if the limit is computable in the $L^1$ norm and the $L^1$-bound is computable, then the rate of convergence is computable (both convergence in measure and a.e. convergence). (I assume the proof is constructive, but I haven't worked that out. However, computable rates of convergence are one of the most important consequences of constructive proofs.)

Similarly, the Lebesgue differentiation theorem has computable rates of convergence ($L^1$ convergence and a.e. convergence) since the limit is known (it is the function itself) and the Hardy-Littlewood maximal lemma controls the maximal amount of deviation from the limit.