OAI/LinearAlgebra/MatrixFields/Histories/HistoryRecovery.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.fullOrbitFilter line 19
  2. def OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.rejectedFilter line 24
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.orbitSet_eq_fullOrbitFilter line 27
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.rejectedFilter_congr line 34
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.fullOrbitFilter_bad_fraction_eq_orbit line 39
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.orbit_bad_fraction_eq_fullOrbitFilter_of_iff line 53
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.full_orbitSet_as_filter line 64
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.PermutationMatching.finite_selectedWordPair_full_filter_inverse_linear_of_windows line 78
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.testedClasses_parent line 118
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.rightProbability_le_one line 122
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.left_density_le line 131
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.right_density_le line 150
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.mixture_error_zero line 169
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.orbitSet_as_filter line 177
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.full_filter_loss_le line 187
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryMasks.orbit_loss_le line 232
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.OrbitLoss.missing_card_partition line 259
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.OrbitLoss.missing_fraction_partition line 276
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.OrbitLoss.combined_inverse_linear line 283
  20. def OAI.MatrixAllFields.MatrixMultiplication.JointOrbitRecovery.SeparatedLoss line 308
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrbitRecovery.separatedLoss_transport line 316
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrbitRecovery.combined_loss line 329
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrbitRecovery.repair_of_separated_losses line 338
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrbitRecovery.subexponential_copies line 378
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.ideal_coordinates line 406
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.ideal_support_windows line 418
  27. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.raw_pair_loss_le line 433
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.ideal_support_marginals line 469
  29. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.sideWeights line 482
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.ideal_support_weights line 489
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.stageCWeights_of_sideWeights line 558
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.completeKeep_of_supported line 570
  33. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.occupied_split_le line 581
  34. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.ideal_smul line 587
  35. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.Used line 598
  36. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.used_windows line 603
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.used_keep_iff_rawPass line 614
  38. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.used_smul line 629
  39. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.deterministic_loss_le line 642
  40. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.holedIdeal line 666
  41. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.ideal_eq_delete_source line 675
  42. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.sideVariable_zero line 690
  43. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.sideVariable_one line 693
  44. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.sideVariable_two line 696
  45. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.branch_eq_holedIdeal line 699
  46. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.support_filter_eq line 729
  47. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.repair_selected line 736
  48. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryRecovery.repair_selected_branch line 792