OAI/Combinatorics/SumProduct/Alignment/ComparableBox03.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteCoverCharacters.rationalCharacter_iff line 19
2. theorem OAI.ComparableBoxLeibman.haar_limit_of_horizontal_irrationality_scaled line 68
3. theorem OAI.ComparableBoxLeibman.haar_limit_fixed_progression_scaled line 150
4. theorem OAI.CubeHorizontalIrrationality.coefficient_divergence_scaled line 255
5. theorem OAI.CubeHorizontalIrrationality.grid_irrationality_scaled line 285