OAI/Combinatorics/EditApproximation/Specification/RawBandPipelineBridges.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.preparedComputedCellSourceWithWorkRawBand_eq line 5
2. theorem OAI.EditApproximation.BinaryFraction.preparedLocalGroupScaleSourceWithWorkRawBand_eq line 9
3. theorem OAI.EditApproximation.BinaryFraction.preparedLocalCellGroupsSourceWithWorkRawBand_eq line 13
4. theorem OAI.EditApproximation.BinaryFraction.preparedLocalOnlineScaleSourceWithWorkRawBand_eq line 17
5. theorem OAI.EditApproximation.BinaryFraction.preparedLocalOnlineActionsSourceWithWorkRawBand_eq line 21
6. theorem OAI.EditApproximation.BinaryFraction.queryOnlineSelectWithWorkRawBand_eq line 25
7. theorem OAI.EditApproximation.BinaryFraction.queryGroupSelectWithWorkRawBand_eq line 29
8. theorem OAI.EditApproximation.queryLocalRefinementRawBand_eq line 33
9. theorem OAI.EditApproximation.queryLocalRandomSourcesRawBand_eq line 37
10. theorem OAI.EditApproximation.queryLocalBandRawBand_eq line 41
11. theorem OAI.EditApproximation.queryLocalProgramRawBand_eq line 45
12. theorem OAI.EditApproximation.queryPhysicalRandomDataRequestRawBand_eq line 49
13. theorem OAI.EditApproximation.queryFamilyRefinementRawBand_eq line 53
14. theorem OAI.EditApproximation.queryFamilyActiveRawBand_eq line 57
15. theorem OAI.EditApproximation.queryFamilyBoundedActiveRawBand_eq line 61
16. theorem OAI.EditApproximation.queryChargedFamilyTableRawBand_eq line 65
17. theorem OAI.EditApproximation.queryChargedFamilyGlobalRawBand_eq line 69
18. theorem OAI.EditApproximation.queryFamilyMemoRawRawBand_eq line 74
19. theorem OAI.EditApproximation.computedQueryMemoRawRawBand_eq line 78
20. theorem OAI.EditApproximation.computedQueryMemoNormalizedRawBand_eq line 82
21. theorem OAI.EditApproximation.computedQueryMemoResultRawBand_eq line 86
22. theorem OAI.EditApproximation.computedQueryLocalWorkRawBand_eq line 90
23. theorem OAI.EditApproximation.integerQueryLocalWorkRawBand_eq line 94
24. theorem OAI.EditApproximation.computedQueryAnswerWithWorkRawBand_eq line 98
25. theorem OAI.EditApproximation.integerBinaryOutputRawBand_eq line 102
26. theorem OAI.EditApproximation.integerBinaryAnswerRawBand_eq line 106
27. theorem OAI.EditApproximation.BinaryFraction.preparedComputedCellSourceAllocationRawBand_eq line 111
28. theorem OAI.EditApproximation.BinaryFraction.preparedLocalGroupScaleSourceAllocationRawBand_eq line 115
29. theorem OAI.EditApproximation.BinaryFraction.localGroupSourceScaleBlockRawBand_eq line 120
30. theorem OAI.EditApproximation.BinaryFraction.localGroupSourceScaleBlockAllocationRawBand_eq line 124
31. theorem OAI.EditApproximation.BinaryFraction.preparedLocalCellGroupsSourceAllocationRawBand_eq line 128
32. theorem OAI.EditApproximation.BinaryFraction.preparedLocalOnlineScaleSourceAllocationRawBand_eq line 132
33. theorem OAI.EditApproximation.BinaryFraction.preparedLocalOnlineActionsSourceAllocationRawBand_eq line 136
34. theorem OAI.EditApproximation.BinaryFraction.queryOnlineSelectAllocationRawBand_eq line 140
35. theorem OAI.EditApproximation.BinaryFraction.queryGroupSelectAllocationRawBand_eq line 144
36. theorem OAI.EditApproximation.integerBinaryWorkRawBand_eq line 148
37. theorem OAI.EditApproximation.integerFinalAllocationRawBand_eq line 152