OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/ChildLaws.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. def OAI.MatrixMultiplication.AllFieldHistory.Work.Statistic line 17
  2. instance OAI.MatrixMultiplication.AllFieldHistory.(instance at line 22) line 22
  3. instance OAI.MatrixMultiplication.AllFieldHistory.(instance at line 25) line 25
  4. def OAI.MatrixMultiplication.AllFieldHistory.Work.statistic line 27
  5. def OAI.MatrixMultiplication.AllFieldHistory.Work.statisticWeight line 33
  6. theorem OAI.MatrixMultiplication.AllFieldHistory.Work.statistic_weight line 40
  7. def OAI.MatrixMultiplication.AllFieldHistory.Work.childLaw line 47
  8. theorem OAI.MatrixMultiplication.AllFieldHistory.Work.childLaw_nonnegative line 54
  9. theorem OAI.MatrixMultiplication.AllFieldHistory.Work.childLaw_normalized line 61
  10. theorem OAI.MatrixMultiplication.AllFieldHistory.Work.childLaw_outside_support line 69
  11. def OAI.MatrixMultiplication.AllFieldHistory.canonicalChildShape line 80
  12. theorem OAI.MatrixMultiplication.AllFieldHistory.canonicalChildShape_branchShape line 83
  13. theorem OAI.MatrixMultiplication.AllFieldHistory.Work.halfShape_mem line 88
  14. def OAI.MatrixMultiplication.AllFieldHistory.placedChildLawRat line 105
  15. def OAI.MatrixMultiplication.AllFieldHistory.childLawRat line 110
  16. def OAI.MatrixMultiplication.AllFieldHistory.rightChildLawRat line 113
  17. theorem OAI.MatrixMultiplication.AllFieldHistory.placedChildLawRat_branchShape line 116
  18. theorem OAI.MatrixMultiplication.AllFieldHistory.placedChildLawRat_nonnegative line 123
  19. theorem OAI.MatrixMultiplication.AllFieldHistory.placedChildLawRat_normalized_of_pos line 128
  20. def OAI.MatrixMultiplication.AllFieldHistory.childLaw line 136
  21. def OAI.MatrixMultiplication.AllFieldHistory.rightChildLaw line 139
  22. abbrev OAI.MatrixMultiplication.AllFieldHistory.ActiveStatistic line 142
  23. def OAI.MatrixMultiplication.AllFieldHistory.activeStatistic line 144
  24. def OAI.MatrixMultiplication.AllFieldHistory.leftChildLaw line 147
  25. def OAI.MatrixMultiplication.AllFieldHistory.rightClassChildLaw line 151
  26. theorem OAI.MatrixMultiplication.AllFieldHistory.leftChildLaw_nonnegative line 155
  27. theorem OAI.MatrixMultiplication.AllFieldHistory.rightClassChildLaw_nonnegative line 161
  28. theorem OAI.MatrixMultiplication.AllFieldHistory.leftChildLaw_normalized_of_pos line 167
  29. theorem OAI.MatrixMultiplication.AllFieldHistory.rightClassChildLaw_normalized_of_pos line 176
  30. abbrev OAI.MatrixMultiplication.AllFieldHistoryChildLaws.Statistic line 192
  31. abbrev OAI.MatrixMultiplication.AllFieldHistoryChildLaws.statistic line 194
  32. abbrev OAI.MatrixMultiplication.AllFieldHistoryChildLaws.leftLaw line 197
  33. abbrev OAI.MatrixMultiplication.AllFieldHistoryChildLaws.rightLaw line 200
  34. theorem OAI.MatrixMultiplication.AllFieldHistoryChildLaws.leftLaw_nonnegative line 203
  35. theorem OAI.MatrixMultiplication.AllFieldHistoryChildLaws.rightLaw_nonnegative line 207
  36. theorem OAI.MatrixMultiplication.AllFieldHistoryChildLaws.leftLaw_normalized line 211
  37. theorem OAI.MatrixMultiplication.AllFieldHistoryChildLaws.rightLaw_normalized line 217
  38. theorem OAI.MatrixMultiplication.AllFieldHistoryChildLaws.singleton_typeWindow line 223