OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/Recovery.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. theorem OAI.MatrixMultiplication.AllFieldHistoryRecovery.ideal_coordinates line 26
  2. theorem OAI.MatrixMultiplication.AllFieldHistoryRecovery.ideal_support_windows line 38
  3. theorem OAI.MatrixMultiplication.AllFieldHistoryRecovery.raw_pair_loss_le line 53
  4. theorem OAI.MatrixMultiplication.AllFieldHistoryRecovery.ideal_support_marginals line 89
  5. def OAI.MatrixMultiplication.AllFieldHistoryRecovery.sideWeights line 102
  6. theorem OAI.MatrixMultiplication.AllFieldHistoryRecovery.ideal_support_weights line 109
  7. theorem OAI.MatrixMultiplication.AllFieldHistoryRecovery.stageCWeights_of_sideWeights line 178
  8. theorem OAI.MatrixMultiplication.AllFieldHistoryRecovery.completeKeep_of_supported line 190
  9. theorem OAI.MatrixMultiplication.AllFieldHistoryRecovery.occupied_split_le line 201
  10. theorem OAI.MatrixMultiplication.AllFieldHistoryRecovery.ideal_smul line 207
  11. def OAI.MatrixMultiplication.AllFieldHistoryRecovery.Used line 218
  12. theorem OAI.MatrixMultiplication.AllFieldHistoryRecovery.used_windows line 223
  13. theorem OAI.MatrixMultiplication.AllFieldHistoryRecovery.used_keep_iff_rawPass line 234
  14. theorem OAI.MatrixMultiplication.AllFieldHistoryRecovery.used_smul line 249
  15. theorem OAI.MatrixMultiplication.AllFieldHistoryRecovery.deterministic_loss_le line 262
  16. def OAI.MatrixMultiplication.AllFieldHistoryRecovery.holedIdeal line 286
  17. theorem OAI.MatrixMultiplication.AllFieldHistoryRecovery.ideal_eq_delete_source line 295
  18. theorem OAI.MatrixMultiplication.AllFieldHistoryRecovery.sideVariable_zero line 322
  19. theorem OAI.MatrixMultiplication.AllFieldHistoryRecovery.sideVariable_one line 325
  20. theorem OAI.MatrixMultiplication.AllFieldHistoryRecovery.sideVariable_two line 328
  21. theorem OAI.MatrixMultiplication.AllFieldHistoryRecovery.branch_eq_holedIdeal line 331
  22. theorem OAI.MatrixMultiplication.AllFieldHistoryRecovery.support_filter_eq line 361
  23. theorem OAI.MatrixMultiplication.AllFieldHistoryRecovery.repair_selected line 368
  24. theorem OAI.MatrixMultiplication.AllFieldHistoryRecovery.repair_selected_branch line 424