OAI/LinearAlgebra/MatrixFields/Histories/ScheduledPositivity.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledYield.workCapacity line 21
2. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledYield.workCapacity_stageC line 24
3. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledYield.sum_interiorPairs line 31
4. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledYield.stageCSourceCapacity_native line 45
5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledYield.active_native_capacity line 63
6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledYield.physical_order_native_capacity line 71
7. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledYield.order_capacity_eq_physical line 78
8. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledYield.order_capacity_eq_native line 98
9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledYield.order_dilation_capacity line 106
10. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledYield.physicalYield line 117
11. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledYield.scheduledYield line 122
12. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledYield.physicalYield_eq_scheduled line 126
13. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledYield.balanced_scheduledYield line 133
14. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledYield.nativeLC_tendsto line 138
15. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledYield.tickCapacity_tendsto line 145
16. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledYield.scheduledYield_tendsto line 160
17. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledYield.physicalYield_tendsto_balanced line 171
18. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledYield.exists_balanced_allocation_sequence line 180
19. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledYield.exists_physicalYield_limit line 204
20. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledYield.initial_capacity line 213
21. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledYield.initial_dilation_capacity line 221
22. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledPositivity.nativeH0_pos line 245
23. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledPositivity.initial_capacity_pos line 276
24. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledPositivity.tickCapacity_pos line 279
25. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledPositivity.physical_order_capacity_pos line 291
26. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldScheduledPositivity.eventually_physical_order_capacity_pos line 301