Nonnegative discrete-time local martingale is a martingale (source code)

= Nonnegative discrete-time local martingale is a martingale

The <Fatou lemma> makes every time value of a nonnegative discrete-time <local martingale> integrable, assuming the usual integrable initial value. The integrable discrete-time result then makes it a true <martingale>.