OAI/Analysis/MatrixSigning/Matrices/PivotHistory.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W07.appendIndexEquiv line 12
2. def OAI.KS.W07.selectedSchur line 24
3. theorem OAI.KS.W07.selectedSchur_reindex_selected line 30
4. theorem OAI.KS.W07.selectedSchur_restrict line 41
5. theorem OAI.KS.W07.originalBorder_reindex line 48
6. theorem OAI.KS.W07.selectedSchur_entry_minor_ratio line 59
7. theorem OAI.KS.W07.selectedSchur_multiplier_minor_ratio line 73
8. theorem OAI.KS.W07.selectedSchur_new_det_ne_zero line 88
9. theorem OAI.KS.W07.selectedSchur_append_step line 97
10. inductive OAI.KS.W07.PivotTrace line 161
11. theorem OAI.KS.W07.PivotTrace.originalSchur line 174
12. theorem OAI.KS.W07.PivotTrace.size_bound line 203
13. theorem OAI.KS.W07.PivotTrace.state_posSemidef line 208
14. theorem OAI.KS.W07.PivotTrace.entry_minor_ratio line 218
15. theorem OAI.KS.W07.PivotTrace.multiplier_minor_ratio line 227