The mean ergodic theorem is a central tool in the study of dynamical systems. On its face, the theorem gives no bounds for the quantities it asserts to exist; this is unfortunate, since the theorem is used routinely in ergodic proofs of combinatorial statements. In this setting, it is often desirable to "unwind" these ergodic proofs to extract combinatorial bounds for the quantities involved. I describe how limited constructive information can be extracted from the mean ergodic theorem in a systematic way using Godel's Dialectica translation.
Logic and Computation Seminar
Monday, April 21, 2008 - 4:30pm
Henry Towsner
Carnegie Mellon University