OAI/Analysis/MatrixSigning/Realization/DenseInputArrays.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.DenseInputArrays.fields line 11
2. def OAI.CurrentKS.DenseInputArrays.records line 16
3. def OAI.CurrentKS.DenseInputArrays.canonical line 18
4. lemma OAI.CurrentKS.DenseInputArrays.fields_length line 20
5. lemma OAI.CurrentKS.DenseInputArrays.flatten_fields line 24
6. lemma OAI.CurrentKS.DenseInputArrays.complex_fields line 31
7. lemma OAI.CurrentKS.DenseInputArrays.fields_raw line 38
8. lemma OAI.CurrentKS.DenseInputArrays.records_length line 42
9. lemma OAI.CurrentKS.DenseInputArrays.records_field_length line 44
10. lemma OAI.CurrentKS.DenseInputArrays.records_raw line 50
11. lemma OAI.CurrentKS.DenseInputArrays.field_raw_le_dense line 54
12. lemma OAI.CurrentKS.DenseInputArrays.field_raw_le_input line 65
13. lemma OAI.CurrentKS.DenseInputArrays.canonical_length_le_raw line 69
14. lemma OAI.CurrentKS.DenseInputArrays.canonical_length_le_input line 79
15. lemma OAI.CurrentKS.DenseInputArrays.count_le_length line 84
16. lemma OAI.CurrentKS.DenseInputArrays.dimension_sq_le_length line 94
17. lemma OAI.CurrentKS.DenseInputArrays.dimension_le_length line 100
18. theorem OAI.CurrentKS.DenseInputArrays.canonical_scan_spec line 104
19. lemma OAI.CurrentKS.DenseInputArrays.canonical_scan_polynomial line 114