OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/Support.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.population_dilation line 18
  2. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.branchPopulation_dilation line 22
  3. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.jointCounts_dilation line 27
  4. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.activeCounts_dilation line 33
  5. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.activeCounts_pos_iff line 38
  6. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.dilation_le_activeCounts line 44
  7. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.two_le_activeCounts line 52
  8. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.totalLength_dilation line 57
  9. def OAI.MatrixMultiplication.AllFieldHistorySupport.fixedBaseLength line 64
  10. def OAI.MatrixMultiplication.AllFieldHistorySupport.supportRate line 69
  11. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.supportRate_pos line 72
  12. abbrev OAI.MatrixMultiplication.AllFieldHistorySupport.ActiveRawPairs line 76
  13. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.raw_support_card_le_exp line 80
  14. abbrev OAI.MatrixMultiplication.AllFieldHistorySupport.ActiveClass line 93
  15. def OAI.MatrixMultiplication.AllFieldHistorySupport.selectedBaseCount line 95
  16. def OAI.MatrixMultiplication.AllFieldHistorySupport.selectedBasePopulation line 99
  17. abbrev OAI.MatrixMultiplication.AllFieldHistorySupport.selectedPositions line 102
  18. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.selected_count_dilation line 106
  19. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.selectedBaseCount_pos line 111
  20. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.selectedBasePopulation_pos line 117
  21. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.selected_populationSize line 124
  22. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.selected_two_le line 136
  23. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.selected_classWeight_formula line 143
  24. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.selected_classWeight_eq_one line 153
  25. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.selected_classProductMixture_eq_one line 160
  26. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.work_source_amount_pos line 169
  27. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.work_source_population_pos line 179
  28. def OAI.MatrixMultiplication.AllFieldHistorySupport.positiveClasses line 184
  29. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.positiveClasses_positive line 188
  30. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.positiveClasses_baseCount line 192
  31. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.positiveClasses_basePopulation_pos line 205
  32. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.positiveClasses_nonempty line 211
  33. theorem OAI.MatrixMultiplication.AllFieldHistorySupport.positiveClasses_populationSize line 218