OAI/Analysis/FreeGroupFactor/Cocycles.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FreeGroupFactorMain.Coeff line 14
  2. def OAI.FreeGroupFactorMain.coefficientShift line 16
  3. theorem OAI.FreeGroupFactorMain.coefficientShift_apply line 19
  4. theorem OAI.FreeGroupFactorMain.coefficientShift_one line 22
  5. theorem OAI.FreeGroupFactorMain.coefficientShift_mul line 27
  6. def OAI.FreeGroupFactorMain.coefficientAction line 32
  7. def OAI.FreeGroupFactorMain.cocycleGraph line 43
  8. theorem OAI.FreeGroupFactorMain.cocycleGraph_right line 48
  9. def OAI.FreeGroupFactorMain.freeCocycle line 55
  10. theorem OAI.FreeGroupFactorMain.freeCocycle_of line 58
  11. theorem OAI.FreeGroupFactorMain.freeCocycle_one line 62
  12. theorem OAI.FreeGroupFactorMain.freeCocycle_mul line 65
  13. theorem OAI.FreeGroupFactorMain.freeCocycle_inv line 72
  14. def OAI.FreeGroupFactorMain.UnitaryEvaluation.hamiltonianLinear line 81
  15. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.hamiltonianLinear_eq line 84
  16. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.hamiltonianLinear_shift line 93
  17. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.wordHom_mem_unitary line 109
  18. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.hasDerivAt_wordHom_cocycle line 112
  19. def OAI.FreeGroupFactorMain.groupUnitaryUHom line 153
  20. theorem OAI.FreeGroupFactorMain.laurentValue_group line 158
  21. theorem OAI.FreeGroupFactorMain.wordHom_original line 174
  22. theorem OAI.FreeGroupFactorMain.hamiltonianLinear_original_bound line 184
  23. theorem OAI.FreeGroupFactorMain.hamiltonianLinear_map line 204
  24. theorem OAI.FreeGroupFactorMain.hamiltonianLinear_single_one line 212
  25. theorem OAI.FreeGroupFactorMain.unitary_curve_displacement line 221
  26. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.hamiltonianLinear_norm_map line 269
  27. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.generator_displacement line 278
  28. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.word_displacement line 292
  29. theorem OAI.FreeGroupFactorMain.wordHom_extend_none_zpow line 313
  30. theorem OAI.FreeGroupFactorMain.flow_iso_fix_laurent line 320
  31. theorem OAI.FreeGroupFactorMain.flow_iso_hamiltonian_bound line 332
  32. theorem OAI.FreeGroupFactorMain.laurent_bounded_flow line 349
  33. theorem OAI.FreeGroupFactorMain.flow_displacements_from_bounds line 375
  34. theorem OAI.FreeGroupFactorMain.laurent_flow_displacement line 403
  35. def OAI.FreeGroupFactorMain.groupL2 line 432
  36. abbrev OAI.FreeGroupFactorMain.twoNorm line 442
  37. theorem OAI.FreeGroupFactorMain.groupL2_apply line 444
  38. theorem OAI.FreeGroupFactorMain.twoNorm_le_norm line 447
  39. theorem OAI.FreeGroupFactorMain.twoNorm_sq line 454
  40. theorem OAI.FreeGroupFactorMain.twoNorm_star line 460
  41. theorem OAI.FreeGroupFactorMain.twoNorm_mul_unitary_left line 470
  42. theorem OAI.FreeGroupFactorMain.twoNorm_mul_unitary_right line 476
  43. theorem OAI.FreeGroupFactorMain.twoNorm_iso line 483
  44. theorem OAI.FreeGroupFactorMain.canonicalTrace_star line 495