OAI/LinearAlgebra/MatrixMultiplication/Recovery/GroupOrbitProjection.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Finite orbit symmetries, masks and exact recovery operations.

  1. def OAI.MatrixMultiplication.GroupOrbitProjection.curryFamily line 26
  2. theorem OAI.MatrixMultiplication.GroupOrbitProjection.average_subtype_restrict line 32
  3. theorem OAI.MatrixMultiplication.GroupOrbitProjection.average_history_restrict line 43
  4. theorem OAI.MatrixMultiplication.GroupOrbitProjection.average_half_history_restrict line 57
  5. theorem OAI.MatrixMultiplication.GroupOrbitProjection.orbit_fraction_of_uniform_projection line 85
  6. theorem OAI.MatrixMultiplication.GroupOrbitProjection.rejected_fraction_of_uniform_projection line 99
  7. theorem OAI.MatrixMultiplication.GroupOrbitProjection.conjugated_projection_smul line 118
  8. def OAI.MatrixMultiplication.GroupOrbitProjection.transportedOrbit line 134
  9. theorem OAI.MatrixMultiplication.GroupOrbitProjection.transported_projection_fraction line 138
  10. def OAI.MatrixMultiplication.GroupOrbitProjection.projectPair line 160
  11. def OAI.MatrixMultiplication.GroupOrbitProjection.projectShifts line 166
  12. theorem OAI.MatrixMultiplication.GroupOrbitProjection.projectPair_smul line 172
  13. theorem OAI.MatrixMultiplication.GroupOrbitProjection.complete_orbit_projection_fraction line 176
  14. theorem OAI.MatrixMultiplication.GroupOrbitProjection.orbit_union_fraction_le line 200
  15. theorem OAI.MatrixMultiplication.GroupOrbitProjection.finset_union_fraction_le line 233
  16. theorem OAI.MatrixMultiplication.GroupOrbitProjection.rejected_union_fraction_le line 253
  17. theorem OAI.MatrixMultiplication.GroupOrbitProjection.complete_group_union_fraction_le line 275
  18. def OAI.MatrixMultiplication.GroupOrbitProjection.groupCounts line 303
  19. def OAI.MatrixMultiplication.GroupOrbitProjection.projectTarget line 305
  20. def OAI.MatrixMultiplication.GroupOrbitProjection.projectRaw line 308
  21. theorem OAI.MatrixMultiplication.GroupOrbitProjection.pairEquiv_projectRaw line 313
  22. theorem OAI.MatrixMultiplication.GroupOrbitProjection.projectRaw_pairEquiv_symm line 321
  23. def OAI.MatrixMultiplication.GroupOrbitProjection.rawOrbit line 335
  24. theorem OAI.MatrixMultiplication.GroupOrbitProjection.raw_orbit_projection_fraction line 340
  25. theorem OAI.MatrixMultiplication.GroupOrbitProjection.raw_group_passing_rejection_fraction_le line 369