OAI/Analysis/FreeGroupFactor/UnitaryEvaluation.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.UnitaryEvaluation.wordHom line 17
  2. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.wordHom_of line 20
  3. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.wordHom_inv line 24
  4. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.wordHom_word line 30
  5. def OAI.FreeGroupFactorMain.UnitaryEvaluation.algebraHom line 45
  6. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.algebraHom_of line 48
  7. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.eval_encode line 52
  8. def OAI.FreeGroupFactorMain.UnitaryEvaluation.coefficientHom line 66
  9. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.coefficientHom_single line 69
  10. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.algebraHom_ofCoeff line 73
  11. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.coefficientHom_shift line 77
  12. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.derivative_of line 93
  13. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.eval_derivative_of line 100
  14. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.eval_encodedField_pos line 106
  15. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.eval_encodedField_neg line 114
  16. def OAI.FreeGroupFactorMain.UnitaryEvaluation.extendUnitary line 131
  17. def OAI.FreeGroupFactorMain.UnitaryEvaluation.laurentValue line 134
  18. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.wordHom_extend line 137
  19. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.coefficientHom_laurent line 145
  20. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.coefficientHom_fieldCoefficients line 159
  21. def OAI.FreeGroupFactorMain.UnitaryEvaluation.signedTrajectory line 173
  22. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.signedTrajectory_some_pos line 177
  23. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.signedTrajectory_some_neg line 182
  24. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.signedTrajectory_none_pos line 187
  25. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.signedTrajectory_none_neg line 192
  26. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.signedTrajectory_ode line 197