OAI/Analysis/FreeGroupFactor/MomentFlow.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.FreeGroupFactorMain.groupVN_normedSpaceReal line 14
  2. instance OAI.FreeGroupFactorMain.groupHilbert_nontrivial line 18
  3. instance OAI.FreeGroupFactorMain.groupVN_normOneClass line 25
  4. def OAI.FreeGroupFactorMain.groupUnitaryHom line 30
  5. def OAI.FreeGroupFactorMain.groupAlgebraEvaluation line 35
  6. theorem OAI.FreeGroupFactorMain.groupAlgebraEvaluation_of line 39
  7. theorem OAI.FreeGroupFactorMain.canonicalTrace_groupAlgebraEvaluation line 43
  8. theorem OAI.FreeGroupFactorMain.canonicalTrace_eval line 58
  9. theorem OAI.FreeGroupFactorMain.source_laurent_moments line 70
  10. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.norm_signedTrajectory_le_one line 112
  11. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.smooth_signedTrajectory line 120
  12. theorem OAI.FreeGroupFactorMain.groupUnitary_mem_unitary line 138
  13. def OAI.FreeGroupFactorMain.generatorUnitary line 145
  14. theorem OAI.FreeGroupFactorMain.wordHom_generatorUnitary line 148
  15. theorem OAI.FreeGroupFactorMain.laurent_flow_moments line 157
  16. theorem OAI.FreeGroupFactorMain.actual_laurent_flow_moments line 203
  17. theorem OAI.FreeGroupFactorMain.PolynomialFlow.coe_wordList line 231
  18. theorem OAI.FreeGroupFactorMain.PolynomialFlow.coe_field line 241
  19. theorem OAI.FreeGroupFactorMain.PolynomialFlow.solution_mem_subalgebra line 247