OAI/Analysis/MatrixSigning/Machines/SchurBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KS.W30.schur_scalar_det_ratio line 12
2. theorem OAI.KS.W30.integer_schur_scalar_det_ratio line 23
3. theorem OAI.KS.W30.natAbs_det_le_two_pow_fintype line 41
4. theorem OAI.KS.W30.integer_det_ratio_parts_size_le line 48
5. theorem OAI.KS.W30.minor_natAbs_le_two_pow line 65
6. theorem OAI.KS.W30.minor_ratio_parts_size_le line 73
7. theorem OAI.KS.W30.scaled_minor_ratio_parts_size_le line 87
8. theorem OAI.KS.W30.cleared_minor_ratio_parts_size_le line 111
9. theorem OAI.KS.W30.schur_smul line 125