OAI/LinearAlgebra/MatrixFields/Entropy/StageCLaw.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.assigned_mem_or_zero line 14
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.assigned_argument_bound line 23
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.splitWeight_positive line 29
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.list_sum_map_nonnegative line 37
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.list_sum_map_positive line 45
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.list_sum_map_div line 54
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.splitLaw_positive line 60
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.splitLaw_normalized line 71
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.stageA_table_arguments_bounded line 84
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.stageB_table_arguments_bounded line 86
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.zero_table_arguments_bounded line 88
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.stageA_support_nonempty line 90
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.stageB_support_nonempty line 92
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.stageA_support_complement line 94
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.stageB_support_complement line 97
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.stageALaw_positive line 100
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.stageBLaw_positive line 103
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.stageALaw_normalized line 106
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.stageBLaw_normalized line 110
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.stageALaw_complement line 114
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.stageBLaw_complement line 119
  22. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.initialMultiplicity line 124
  23. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.initialInteger line 127
  24. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.initialWeight line 129
  25. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.initialLaw line 132
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.initial_table_arguments_bounded line 135
  27. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.initialWeight_positive line 137
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.initialLaw_positive line 146
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.initialLaw_normalized line 151
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.binary_table_bounds line 161
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.binaryInteger_bounds line 163
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.binaryParameter_bounds line 171
  33. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.singletonSlot line 181
  34. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.littleLaw line 189
  35. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.littleLaw_nonnegative line 194
  36. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.littleLaw_normalized line 200
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.orderedPairWeight_positive line 216
  38. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.orderedPairs_nonempty line 221
  39. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.orderedPairs_support line 223
  40. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.zeroPairLaw_positive line 231
  41. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.zeroPairLaw_normalized line 238
  42. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCDistinguished line 257
  43. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCCanonicalAtom line 260
  44. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCAtom line 263
  45. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCWeight line 270
  46. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.positive_four_shapes line 273
  47. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCDistinguished_spec line 277
  48. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageC_children_length line 282
  49. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageC_children_geometry line 286
  50. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageC_middle_complement line 293
  51. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCAtom_injective line 299
  52. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCAtom_mem line 303
  53. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCAtom_exhaustive line 307
  54. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCAtom_middle line 311
  55. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCShapeWeight line 315
  56. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCLaw line 320
  57. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCLaw_source line 322
  58. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCLaw_nonnegative line 329
  59. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCWeight_nonnegative line 334
  60. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCWeight_normalized line 340
  61. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCWeight_single line 343
  62. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCWeight_cross line 348
  63. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCLaw_atom line 354
  64. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCShapeWeight_normalized line 360
  65. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCShapeWeight_normalized_below line 367
  66. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCLaw_normalized line 374
  67. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCLaw_normalized_below line 379
  68. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCLaw_outside_support line 384
  69. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCLaw_support line 388
  70. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCLaw_children_zero line 393
  71. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCLaw_complement line 399