OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/Populations.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. structure OAI.MatrixMultiplication.AllFieldHistory.Allocation line 22
  2. abbrev OAI.MatrixMultiplication.AllFieldHistory.Placement line 27
  3. abbrev OAI.MatrixMultiplication.AllFieldHistory.Initial line 28
  4. def OAI.MatrixMultiplication.AllFieldHistory.initialShape line 30
  5. theorem OAI.MatrixMultiplication.AllFieldHistory.initialShape_mem line 32
  6. abbrev OAI.MatrixMultiplication.AllFieldHistory.InitialPositive line 35
  7. abbrev OAI.MatrixMultiplication.AllFieldHistory.ASplit line 37
  8. abbrev OAI.MatrixMultiplication.AllFieldHistory.AfterA line 38
  9. def OAI.MatrixMultiplication.AllFieldHistory.aSplit line 40
  10. def OAI.MatrixMultiplication.AllFieldHistory.halfShape line 43
  11. def OAI.MatrixMultiplication.AllFieldHistory.aShape line 46
  12. theorem OAI.MatrixMultiplication.AllFieldHistory.aSplit_mem line 49
  13. theorem OAI.MatrixMultiplication.AllFieldHistory.aShape_mem line 52
  14. theorem OAI.MatrixMultiplication.AllFieldHistory.stageA_children_size line 56
  15. theorem OAI.MatrixMultiplication.AllFieldHistory.aShape_size line 59
  16. abbrev OAI.MatrixMultiplication.AllFieldHistory.APositive line 62
  17. abbrev OAI.MatrixMultiplication.AllFieldHistory.BSplit line 63
  18. abbrev OAI.MatrixMultiplication.AllFieldHistory.AfterB line 64
  19. def OAI.MatrixMultiplication.AllFieldHistory.bSplit line 66
  20. def OAI.MatrixMultiplication.AllFieldHistory.bShape line 69
  21. theorem OAI.MatrixMultiplication.AllFieldHistory.bSplit_mem line 72
  22. theorem OAI.MatrixMultiplication.AllFieldHistory.bShape_mem line 75
  23. theorem OAI.MatrixMultiplication.AllFieldHistory.stageB_children_size line 79
  24. theorem OAI.MatrixMultiplication.AllFieldHistory.bShape_size line 82
  25. abbrev OAI.MatrixMultiplication.AllFieldHistory.BPositive line 85
  26. abbrev OAI.MatrixMultiplication.AllFieldHistory.PartC line 86
  27. abbrev OAI.MatrixMultiplication.AllFieldHistory.AfterC line 87
  28. def OAI.MatrixMultiplication.AllFieldHistory.cParameterParent line 89
  29. def OAI.MatrixMultiplication.AllFieldHistory.cShapeParent line 90
  30. def OAI.MatrixMultiplication.AllFieldHistory.cSplit line 92
  31. def OAI.MatrixMultiplication.AllFieldHistory.cShape line 94
  32. theorem OAI.MatrixMultiplication.AllFieldHistory.cShape_zero line 97
  33. instance OAI.MatrixMultiplication.AllFieldHistory.initialPositiveFintype line 105
  34. instance OAI.MatrixMultiplication.AllFieldHistory.aPositiveFintype line 108
  35. instance OAI.MatrixMultiplication.AllFieldHistory.bPositiveFintype line 111
  36. inductive OAI.MatrixMultiplication.AllFieldHistory.CanonicalHistory line 114
  37. abbrev OAI.MatrixMultiplication.AllFieldHistory.History line 122
  38. def OAI.MatrixMultiplication.AllFieldHistory.initialAmount line 124
  39. def OAI.MatrixMultiplication.AllFieldHistory.aAmount line 125
  40. def OAI.MatrixMultiplication.AllFieldHistory.bAmount line 127
  41. def OAI.MatrixMultiplication.AllFieldHistory.partAmount line 129
  42. def OAI.MatrixMultiplication.AllFieldHistory.cAmount line 131
  43. def OAI.MatrixMultiplication.AllFieldHistory.canonicalAmount line 134
  44. def OAI.MatrixMultiplication.AllFieldHistory.amount line 141
  45. theorem OAI.MatrixMultiplication.AllFieldHistory.initialAmount_pos line 144
  46. theorem OAI.MatrixMultiplication.AllFieldHistory.aAmount_pos line 147
  47. theorem OAI.MatrixMultiplication.AllFieldHistory.bAmount_pos line 150
  48. theorem OAI.MatrixMultiplication.AllFieldHistory.partAmount_pos line 153
  49. theorem OAI.MatrixMultiplication.AllFieldHistory.cAmount_nonneg line 156
  50. theorem OAI.MatrixMultiplication.AllFieldHistory.amount_nonneg line 160
  51. theorem OAI.MatrixMultiplication.AllFieldHistory.placement_amount_eq line 170
  52. theorem OAI.MatrixMultiplication.AllFieldHistory.sum_placement_amount line 174
  53. theorem OAI.MatrixMultiplication.AllFieldHistory.initial_amount_sum line 181
  54. theorem OAI.MatrixMultiplication.AllFieldHistory.root_mass_sum_lot line 187
  55. theorem OAI.MatrixMultiplication.AllFieldHistory.a_transition line 193
  56. theorem OAI.MatrixMultiplication.AllFieldHistory.b_transition line 200
  57. theorem OAI.MatrixMultiplication.AllFieldHistory.part_transition line 207
  58. theorem OAI.MatrixMultiplication.AllFieldHistory.c_transition line 211
  59. def OAI.MatrixMultiplication.AllFieldHistory.population line 215
  60. def OAI.MatrixMultiplication.AllFieldHistory.populationLength line 218
  61. theorem OAI.MatrixMultiplication.AllFieldHistory.population_cast line 221
  62. theorem OAI.MatrixMultiplication.AllFieldHistory.population_zero_iff line 226
  63. theorem OAI.MatrixMultiplication.AllFieldHistory.initial_population_sum line 231
  64. theorem OAI.MatrixMultiplication.AllFieldHistory.a_population_transition line 240
  65. theorem OAI.MatrixMultiplication.AllFieldHistory.b_population_transition line 248
  66. theorem OAI.MatrixMultiplication.AllFieldHistory.part_population_transition line 256
  67. theorem OAI.MatrixMultiplication.AllFieldHistory.c_population_transition line 264
  68. theorem OAI.MatrixMultiplication.AllFieldHistory.a_half_counts_eq line 272
  69. theorem OAI.MatrixMultiplication.AllFieldHistory.b_half_counts_eq line 278
  70. theorem OAI.MatrixMultiplication.AllFieldHistory.c_half_counts_eq line 284