OAI/LinearAlgebra/MatrixFields/Entropy/TerminalStatisticLaws.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.AZero line 19
2. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.BZero line 22
3. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.TerminalZero line 25
4. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.aShape_mem_shapes line 29
5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.aShape_not_positive line 32
6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.aShape_mem_zeroSecond line 36
7. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.bParent line 39
8. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.bParent_mem_positiveSecond line 41
9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.bShape_mem_shapes line 44
10. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.bShape_mem_below line 47
11. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.bShape_max_lt_five line 50
12. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.bWeight line 55
13. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.bWeight_val line 58
14. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.Slot line 61
15. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.(instance at line 65) line 65
16. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.history line 68
17. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.history_inl line 72
18. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.history_inr line 75
19. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.law line 78
20. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.law_inl line 82
21. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.law_inr line 85
22. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.statisticLaw_nonnegative line 89
23. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.statisticLaw_total line 95
24. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.law_nonneg line 99
25. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.law_total line 104
26. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldTerminalStatisticLaws.history_amount_pos line 109