OAI/Analysis/CharacterCriterion/SymmetryFlow.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KirchbergRordam.SymmetryFlow.phase line 38
  2. lemma OAI.KirchbergRordam.SymmetryFlow.phase_continuous line 40
  3. lemma OAI.KirchbergRordam.SymmetryFlow.phase_zero line 41
  4. lemma OAI.KirchbergRordam.SymmetryFlow.phase_one line 42
  5. lemma OAI.KirchbergRordam.SymmetryFlow.phase_unitary line 43
  6. def OAI.KirchbergRordam.SymmetryFlow.involutionValue line 49
  7. lemma OAI.KirchbergRordam.SymmetryFlow.involutionValue_continuous line 52
  8. lemma OAI.KirchbergRordam.SymmetryFlow.involutionValue_unitary line 56
  9. def OAI.KirchbergRordam.SymmetryFlow.flow line 94
  10. lemma OAI.KirchbergRordam.SymmetryFlow.coe_flow line 97
  11. lemma OAI.KirchbergRordam.SymmetryFlow.flow_zero line 99
  12. lemma OAI.KirchbergRordam.SymmetryFlow.flow_one line 102
  13. lemma OAI.KirchbergRordam.SymmetryFlow.flow_continuous line 105
  14. lemma OAI.KirchbergRordam.SymmetryFlow.phase_add line 107
  15. lemma OAI.KirchbergRordam.SymmetryFlow.flow_add line 110
  16. lemma OAI.KirchbergRordam.SymmetryFlow.flow_neg line 123
  17. lemma OAI.KirchbergRordam.SymmetryFlow.flow_commute line 128
  18. lemma OAI.KirchbergRordam.SymmetryFlow.flow_map line 131
  19. structure OAI.KirchbergRordam.UnitaryConjugacySquare.Flow line 143
  20. instance OAI.KirchbergRordam.UnitaryConjugacySquare.(instance at line 148) line 148
  21. lemma OAI.KirchbergRordam.UnitaryConjugacySquare.flow_zero line 149
  22. lemma OAI.KirchbergRordam.UnitaryConjugacySquare.flow_add line 150
  23. lemma OAI.KirchbergRordam.UnitaryConjugacySquare.flow_neg line 151
  24. lemma OAI.KirchbergRordam.UnitaryConjugacySquare.flow_continuous line 155
  25. def OAI.KirchbergRordam.UnitaryConjugacySquare.symmetry line 157
  26. abbrev OAI.KirchbergRordam.UnitaryConjugacySquare.Square line 163
  27. def OAI.KirchbergRordam.UnitaryConjugacySquare.radius line 165
  28. def OAI.KirchbergRordam.UnitaryConjugacySquare.ratio line 166
  29. lemma OAI.KirchbergRordam.UnitaryConjugacySquare.radius_continuous line 167
  30. lemma OAI.KirchbergRordam.UnitaryConjugacySquare.radius_nonneg line 168
  31. lemma OAI.KirchbergRordam.UnitaryConjugacySquare.fst_le_radius line 173
  32. lemma OAI.KirchbergRordam.UnitaryConjugacySquare.snd_le_radius line 178
  33. lemma OAI.KirchbergRordam.UnitaryConjugacySquare.radius_le_one line 183
  34. lemma OAI.KirchbergRordam.UnitaryConjugacySquare.radius_eq_zero_iff line 188
  35. lemma OAI.KirchbergRordam.UnitaryConjugacySquare.ratio_nonneg line 198
  36. lemma OAI.KirchbergRordam.UnitaryConjugacySquare.ratio_le_one line 200
  37. lemma OAI.KirchbergRordam.UnitaryConjugacySquare.scaled_ratio_nonneg line 204
  38. lemma OAI.KirchbergRordam.UnitaryConjugacySquare.scaled_ratio_le line 206
  39. lemma OAI.KirchbergRordam.UnitaryConjugacySquare.scaled_ratio_tendsto line 208
  40. def OAI.KirchbergRordam.UnitaryConjugacySquare.square line 214
  41. lemma OAI.KirchbergRordam.UnitaryConjugacySquare.square_origin line 217
  42. lemma OAI.KirchbergRordam.UnitaryConjugacySquare.square_error line 220
  43. lemma OAI.KirchbergRordam.UnitaryConjugacySquare.square_continuous line 238
  44. lemma OAI.KirchbergRordam.UnitaryConjugacySquare.square_bottom line 270
  45. lemma OAI.KirchbergRordam.UnitaryConjugacySquare.square_right line 272
  46. lemma OAI.KirchbergRordam.UnitaryConjugacySquare.square_top line 274
  47. lemma OAI.KirchbergRordam.UnitaryConjugacySquare.square_left line 282
  48. structure OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data line 296
  49. def OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.Hp line 308
  50. def OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.Kp line 309
  51. def OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.U line 310
  52. def OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.R line 311
  53. def OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.W line 312
  54. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.Hp_one line 315
  55. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.Kp_one line 316
  56. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.H_star line 317
  57. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.K_star line 318
  58. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.H_inv line 319
  59. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.K_inv line 320
  60. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.Hp_commute line 321
  61. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.Kp_commute line 325
  62. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.U_zero line 329
  63. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.R_zero line 330
  64. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.HH line 332
  65. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.KK line 333
  66. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.U_continuous line 334
  67. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.R_continuous line 335
  68. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.W_continuous line 338
  69. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.W_bottom line 344
  70. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.W_right line 348
  71. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.W_left line 356
  72. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.W_top line 366
  73. abbrev OAI.KirchbergRordam.UnitaryDisplacement.conj line 381
  74. def OAI.KirchbergRordam.UnitaryDisplacement.displacement line 382
  75. lemma OAI.KirchbergRordam.UnitaryDisplacement.conj_mul line 383
  76. lemma OAI.KirchbergRordam.UnitaryDisplacement.conj_star line 385
  77. lemma OAI.KirchbergRordam.UnitaryDisplacement.norm_sub line 388
  78. lemma OAI.KirchbergRordam.UnitaryDisplacement.displacement_mul line 390
  79. lemma OAI.KirchbergRordam.UnitaryDisplacement.displacement_star line 399
  80. lemma OAI.KirchbergRordam.UnitaryDisplacement.displacement_conjugate line 407
  81. lemma OAI.KirchbergRordam.UnitaryDisplacement.conj_eq_of_commute line 414
  82. lemma OAI.KirchbergRordam.UnitaryDisplacement.displacement_zero line 417
  83. lemma OAI.KirchbergRordam.UnitaryDisplacement.displacement_near_fixed line 419
  84. lemma OAI.KirchbergRordam.UnitaryDisplacement.transport_error line 427
  85. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.Kp_fixes line 445
  86. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.Hp_fixes line 447
  87. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.U_control line 450
  88. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.square_control line 455
  89. theorem OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.half_flip_control line 469
  90. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.symmetry_mem line 492
  91. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.W_bottom_mem line 500
  92. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.W_right_mem line 505
  93. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.W_left_mem line 513
  94. lemma OAI.KirchbergRordam.SymmetryConjugacyDiagram.Data.W_top_mem line 519