OAI/Analysis/FreeWords/DyadicGrid.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KKProjectionSupport.BitWords line 16
2. instance OAI.KKProjectionSupport.bitWordsFintype line 20
3. instance OAI.KKProjectionSupport.bitWordsDecEq line 25
4. structure OAI.KKProjectionSupport.DyadicGrid line 37
5. def OAI.KKProjectionSupport.gridZero line 44
6. theorem OAI.KKProjectionSupport.grid_refine line 51
7. def OAI.KKProjectionSupport.dyadicGrid line 107
8. theorem OAI.KKProjectionSupport.dyadicGrid_refine line 112