OAI/Combinatorics/EditApproximation/Specification/RawBandPipelineFootprintBridges.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.footprintRanked_congr line 34
2. theorem OAI.EditApproximation.queryLocalRefinementFootprintRawBand_heq line 45
3. theorem OAI.EditApproximation.queryLocalRandomSourcesFootprintRawBand_heq line 55
4. theorem OAI.EditApproximation.queryLocalBandFootprintRawBand_heq line 72
5. theorem OAI.EditApproximation.queryLocalProgramFootprintRawBand_heq line 89
6. theorem OAI.EditApproximation.queryPhysicalRandomDataRequestFootprintRawBand_heq line 106
7. theorem OAI.EditApproximation.queryFamilyRefinementFootprintRawBand_heq line 123
8. theorem OAI.EditApproximation.queryFamilyActiveFootprintRawBand_heq line 140
9. theorem OAI.EditApproximation.queryFamilyBoundedActiveFootprintRawBand_heq line 157
10. theorem OAI.EditApproximation.queryChargedFamilyTableFootprintRawBand_heq line 174
11. theorem OAI.EditApproximation.queryChargedFamilyGlobalFootprintRawBand_heq line 192
12. theorem OAI.EditApproximation.queryFamilyMemoRawFootprintRawBand_heq line 209
13. theorem OAI.EditApproximation.computedQueryMemoRawFootprintRawBand_heq line 226
14. theorem OAI.EditApproximation.computedQueryMemoFootprintRawBand_heq line 243
15. theorem OAI.EditApproximation.computedQueryTemporaryCellsFootprintRawBand_eq line 263
16. theorem OAI.EditApproximation.integerAcceptedSpaceTermsFootprintRawBand_eq line 273
17. theorem OAI.EditApproximation.integerBinarySpaceFootprintRawBand_eq line 282