OAI/Analysis/CharacterCriterion/PrimeSquare.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KirchbergRordam.PrimeSquareUnitary.diagram line 39
  2. lemma OAI.KirchbergRordam.PrimeSquareUnitary.R_eq line 58
  3. lemma OAI.KirchbergRordam.PrimeSquareUnitary.cross_H line 60
  4. lemma OAI.KirchbergRordam.PrimeSquareUnitary.cross_K line 64
  5. lemma OAI.KirchbergRordam.PrimeSquareUnitary.bottom line 69
  6. lemma OAI.KirchbergRordam.PrimeSquareUnitary.left line 74
  7. lemma OAI.KirchbergRordam.PrimeSquareUnitary.right line 79
  8. lemma OAI.KirchbergRordam.PrimeSquareUnitary.top line 84
  9. lemma OAI.KirchbergRordam.PrimeSquareUnitary.corner00 line 90
  10. lemma OAI.KirchbergRordam.PrimeSquareUnitary.corner10 line 93
  11. lemma OAI.KirchbergRordam.PrimeSquareUnitary.corner01 line 98
  12. lemma OAI.KirchbergRordam.PrimeSquareUnitary.corner11 line 101
  13. lemma OAI.KirchbergRordam.PrimeSquareUnitary.fibers line 107
  14. def OAI.KirchbergRordam.PrimeSquareUnitary.unitarySection line 135
  15. lemma OAI.KirchbergRordam.PrimeSquareUnitary.section_mem line 136
  16. def OAI.KirchbergRordam.PrimeSquareUnitary.continuousUnitary line 139
  17. lemma OAI.KirchbergRordam.PrimeSquareUnitary.unitary_lift line 146
  18. lemma OAI.KirchbergRordam.PrimeSquareUnitary.section_unitary line 157
  19. lemma OAI.KirchbergRordam.PrimeSquareUnitary.section_exists_raw line 164
  20. lemma OAI.KirchbergRordam.PrimeSquareUnitary.reflect_unitary line 167
  21. lemma OAI.KirchbergRordam.PrimeSquareUnitary.section_image_unitary line 175
  22. lemma OAI.KirchbergRordam.PrimeSquareUnitary.section_reflect line 181
  23. theorem OAI.KirchbergRordam.PrimeSquareUnitary.exists_unitary line 198
  24. lemma OAI.KirchbergRordam.PrimeSquareUnitary.conj_map line 209
  25. lemma OAI.KirchbergRordam.PrimeSquareUnitary.conj_commute line 214
  26. lemma OAI.KirchbergRordam.PrimeSquareUnitary.pointwise_control line 219
  27. lemma OAI.KirchbergRordam.PrimeSquareUnitary.norm_bound_in_sections line 269
  28. theorem OAI.KirchbergRordam.PrimeSquareUnitary.exists_half_flip_control line 281