OAI/Analysis/KadisonKastler/BilateralTwistedErgodicity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Unitary-cocycle invariant L2 functions on the bilateral walk are constant.

  1. theorem OAI.KadisonKastler.bilateral_twisted_invariant_constant line 18