OAI/Analysis/IrrationalRotation/Sampling/ErgodicCharacterCriterion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.Characters.integral_eq_zero_of_eigenfunction line 10
2. theorem OAI.Invariant233.Characters.eq_zero_of_dense_inner line 29
3. theorem OAI.Invariant233.Characters.ergodic_of_dense_L2_eigenfunctions line 44
4. theorem OAI.Invariant233.Characters.ergodic_of_dense_continuous_eigenfunctions line 119