OAI/Probability/ClassicalON/DyadicModes.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClassicalON.groupedPoint line 11
2. def OAI.ClassicalON.groupedTorusPoint line 15
3. instance OAI.ClassicalON.dyadicModulus_neZero line 18
4. theorem OAI.ClassicalON.groupedTorusPoint_injective line 20
5. def OAI.ClassicalON.dyadicWeight line 31
6. theorem OAI.ClassicalON.dyadicWeight_pos line 34
7. theorem OAI.ClassicalON.dyadicWeight_sq line 39
8. theorem OAI.ClassicalON.dyadicWeight_mul_sqrt line 46
9. theorem OAI.ClassicalON.wave_commutator line 53