OAI/Analysis/IrrationalRotation/Rotation/CocycleSupport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.CocycleSupport.uniform_floor_ne_zero_le line 14
2. theorem OAI.Invariant233.CocycleSupport.ae_finite_support_of_tsum_ne_top line 48
3. theorem OAI.Invariant233.CocycleSupport.ae_all_finite_support_of_tsum_ne_top line 55
4. theorem OAI.Invariant233.CocycleSupport.measure_floor_ne_zero_le line 64
5. theorem OAI.Invariant233.CocycleSupport.ae_all_int_finite_floor_support line 78