OAI/Analysis/IrrationalRotation/Rotation/PositiveDiagonal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.Fields.projection_diagonal_mem_Icc line 12
2. theorem OAI.Invariant233.Fields.ae_strict_diagonal_of_ergodic line 23
3. theorem OAI.Invariant233.Fields.tendsto_measure_small_of_ae_pos line 63
4. theorem OAI.Invariant233.Fields.tendsto_measure_diagonal_endpoints line 85