Proof of `Kingman's subadditive ergodic theorem`
groundedproofs/Lax606786Proofs/ErgodicStatements.lean · lax-606786
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Steele's proof (Steele 1989) of Kingman's theorem (Kingman 1968): the families are truncated from below, Birkhoff's theorem bounds the upper limit of the averages, and a covering of the orbit by blocks on which the averages are nearly minimal bounds the lower limit.