OAI/Combinatorics/SumProduct/Alignment/IntegerArrays05.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SourceIntegerArrays.GlobalJoint.Target line 33
  2. def OAI.SourceIntegerArrays.GlobalJoint.slotBasis line 37
  3. def OAI.SourceIntegerArrays.GlobalJoint.slotProjection line 40
  4. lemma OAI.SourceIntegerArrays.GlobalJoint.slotProjection_unit line 45
  5. def OAI.SourceIntegerArrays.GlobalJoint.shiftAll line 55
  6. lemma OAI.SourceIntegerArrays.GlobalJoint.shiftAll_continuous line 64
  7. def OAI.SourceIntegerArrays.GlobalJoint.translateTarget line 69
  8. lemma OAI.SourceIntegerArrays.GlobalJoint.translateTarget_continuous line 80
  9. lemma OAI.SourceIntegerArrays.GlobalJoint.translateTarget_add line 86
  10. lemma OAI.SourceIntegerArrays.GlobalJoint.translateTarget_zero line 102
  11. def OAI.SourceIntegerArrays.GlobalJoint.targetAction line 115
  12. theorem OAI.SourceIntegerArrays.GlobalJoint.target_actions line 127
  13. def OAI.SourceIntegerArrays.GlobalJoint.FactorizedPhysical line 165
  14. theorem OAI.SourceIntegerArrays.GlobalJoint.factorized_physical line 187
  15. theorem OAI.SourceIntegerArrays.source_compact_physical line 272