OAI/LinearAlgebra/MatrixFields/Certificates/InitialProbabilities.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.sortedInitial_list line 15
2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.positiveInitial_list line 46
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.positiveSecond_list line 68
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.zeroSecond_list line 90
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.allSecond_list line 115
6. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs line 162
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_0_0_16 line 195
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_0_1_15 line 197
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_0_2_14 line 199
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_0_3_13 line 201
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_0_4_12 line 203
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_0_5_11 line 205
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_0_6_10 line 207
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_0_7_9 line 209
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_0_8_8 line 211
16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_1_1_14 line 213
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_1_2_13 line 215
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_1_3_12 line 217
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_1_4_11 line 219
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_1_5_10 line 221
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_1_6_9 line 223
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_1_7_8 line 225
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_2_2_12 line 227
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_2_3_11 line 229
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_2_4_10 line 231
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_2_5_9 line 233
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_2_6_8 line 235
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_2_7_7 line 237
29. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_3_3_10 line 239
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_3_4_9 line 241
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_3_5_8 line 243
32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_3_6_7 line 245
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_4_4_8 line 247
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_4_5_7 line 249
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_4_6_6 line 251
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_5_5_6 line 253
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.initialProbs_sound line 255