OAI/LinearAlgebra/MatrixFields/Histories/HistorySourceAssignment.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.curryFamily line 25
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.average_subtype_restrict line 31
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.average_history_restrict line 42
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.average_half_history_restrict line 56
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.orbit_fraction_of_uniform_projection line 84
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.rejected_fraction_of_uniform_projection line 98
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.conjugated_projection_smul line 117
  8. def OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.transportedOrbit line 133
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.transported_projection_fraction line 137
  10. def OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.projectPair line 159
  11. def OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.projectShifts line 165
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.projectPair_smul line 171
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.complete_orbit_projection_fraction line 175
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.orbit_union_fraction_le line 199
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.finset_union_fraction_le line 232
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.rejected_union_fraction_le line 252
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.complete_group_union_fraction_le line 274
  18. def OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.groupCounts line 304
  19. def OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.projectTarget line 306
  20. def OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.projectRaw line 309
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.pairEquiv_projectRaw line 314
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.projectRaw_pairEquiv_symm line 322
  23. def OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.rawOrbit line 334
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.raw_orbit_projection_fraction line 339
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.GroupOrbitProjection.raw_group_passing_rejection_fraction_le line 368
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.RecoveryOrbitDecisions.orbitSet_instances line 432
  27. theorem OAI.MatrixAllFields.MatrixMultiplication.RecoveryOrbitDecisions.orbitSet_eq_transportedOrbit line 440
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.RecoveryOrbitDecisions.transportedOrbit_eq_orbitSet line 448
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupedRecovery.coordinates_project line 472
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupedRecovery.idealSide_iff_all_groups line 483
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupedRecovery.project_joinGroupTargets line 497
  32. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupedRecovery.groupedAssignment line 507
  33. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupedRecovery.groupedAssignment_sound line 521
  34. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupedRecovery.localOrbit line 559
  35. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupedRecovery.localAssigned line 566
  36. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupedRecovery.grouped_assigned_iff line 573
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupedRecovery.filter_eq_rejected line 588
  38. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupedRecovery.grouped_collision_le line 594
  39. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryGroupedRecovery.repair_grouped line 671
  40. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistorySource.groupedAssignment_coherent line 723