OAI/Analysis/MatrixSigning/Matrices/PivotHistoryRun.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.KS.W07.PivotSnapshot line 11
2. def OAI.KS.W07.initialPivotSnapshot line 18
3. def OAI.KS.W07.nextPivotSnapshot line 21
4. def OAI.KS.W07.ldlHistory line 31
5. def OAI.KS.W07.SnapshotValid line 35
6. theorem OAI.KS.W07.SnapshotValid.next line 38
7. theorem OAI.KS.W07.ldlHistory_valid line 58
8. theorem OAI.KS.W07.ldlHistory_originalSchur line 65
9. theorem OAI.KS.W07.ldlHistory_size_bound line 76
10. theorem OAI.KS.W07.ldlHistory_entry_minor_ratio line 84