OAI/Analysis/FreeGroupFactor/PolynomialFlow.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.PolynomialFlow.wordList line 21
  2. def OAI.FreeGroupFactorMain.PolynomialFlow.word line 24
  3. def OAI.FreeGroupFactorMain.PolynomialFlow.hamiltonian line 26
  4. def OAI.FreeGroupFactorMain.PolynomialFlow.field line 29
  5. theorem OAI.FreeGroupFactorMain.PolynomialFlow.smooth_wordList line 33
  6. theorem OAI.FreeGroupFactorMain.PolynomialFlow.smooth_word line 47
  7. theorem OAI.FreeGroupFactorMain.PolynomialFlow.smooth_hamiltonian line 50
  8. theorem OAI.FreeGroupFactorMain.PolynomialFlow.smooth_field line 60
  9. theorem OAI.FreeGroupFactorMain.PolynomialFlow.selfAdjoint_hamiltonian line 68
  10. theorem OAI.FreeGroupFactorMain.PolynomialFlow.local_solution line 75
  11. theorem OAI.FreeGroupFactorMain.PolynomialFlow.tangent_star_mul line 86
  12. theorem OAI.FreeGroupFactorMain.PolynomialFlow.solution_star_mul_derivative line 95
  13. theorem OAI.FreeGroupFactorMain.PolynomialFlow.solution_star_mul_constant line 104
  14. theorem OAI.FreeGroupFactorMain.PolynomialFlow.local_unitary_solution line 115
  15. theorem OAI.FreeGroupFactorMain.PolynomialFlow.boundedLip_clip_coordinate line 155
  16. theorem OAI.FreeGroupFactorMain.PolynomialFlow.boundedLip_clip_wordList line 165
  17. theorem OAI.FreeGroupFactorMain.PolynomialFlow.boundedLip_clip_word line 175
  18. theorem OAI.FreeGroupFactorMain.PolynomialFlow.boundedLip_clip_hamiltonian line 179
  19. theorem OAI.FreeGroupFactorMain.PolynomialFlow.boundedLip_clip_field line 188
  20. theorem OAI.FreeGroupFactorMain.PolynomialFlow.tangent_clipped line 195
  21. theorem OAI.FreeGroupFactorMain.PolynomialFlow.global_unitary_solution line 207
  22. theorem OAI.FreeGroupFactorMain.PolynomialFlow.smooth_solution line 256
  23. theorem OAI.FreeGroupFactorMain.PolynomialFlow.norm_unitary_tuple_le line 272
  24. theorem OAI.FreeGroupFactorMain.PolynomialFlow.unitary_solutions_unique line 278