OAI/Combinatorics/SumProduct/Alignment/RoughKernel04.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularResiduePieces.uniform_error_threshold line 31
2. theorem OAI.RegularResiduePieces.uniform_piece_selection line 86
3. def OAI.RoughKernelFactorization.sampledTest line 134
4. def OAI.RoughKernelFactorization.frozenSampledTest line 139
5. theorem OAI.RoughKernelFactorization.regular_sample_freezing line 150
6. theorem OAI.RoughKernelFactorization.regular_sample_select_frozen line 217