OAI/Analysis/CharacterCriterion/PrimePresentation.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.KirchbergRordam.PrimeDropPresentation.size_two line 40
  2. instance OAI.KirchbergRordam.PrimeDropPresentation.(instance at line 43) line 43
  3. instance OAI.KirchbergRordam.PrimeDropPresentation.(instance at line 44) line 44
  4. instance OAI.KirchbergRordam.PrimeDropPresentation.(instance at line 46) line 46
  5. lemma OAI.KirchbergRordam.PrimeDropPresentation.stage_step_norm line 48
  6. instance OAI.KirchbergRordam.PrimeDropPresentation.(instance at line 53) line 53
  7. instance OAI.KirchbergRordam.PrimeDropPresentation.(instance at line 54) line 54
  8. def OAI.KirchbergRordam.PrimeDropPresentation.Algebra line 56
  9. instance OAI.KirchbergRordam.PrimeDropPresentation.(instance at line 57) line 57
  10. instance OAI.KirchbergRordam.PrimeDropPresentation.(instance at line 58) line 58
  11. instance OAI.KirchbergRordam.PrimeDropPresentation.(instance at line 59) line 59
  12. def OAI.KirchbergRordam.PrimeDropPresentation.inclusion line 60
  13. lemma OAI.KirchbergRordam.PrimeDropPresentation.norm_inclusion line 61
  14. lemma OAI.KirchbergRordam.PrimeDropPresentation.inclusion_isometry line 63
  15. lemma OAI.KirchbergRordam.PrimeDropPresentation.inclusion_map line 64
  16. lemma OAI.KirchbergRordam.PrimeDropPresentation.inclusion_step line 66
  17. lemma OAI.KirchbergRordam.PrimeDropPresentation.denseRange_inclusion line 71
  18. theorem OAI.KirchbergRordam.PrimeDropPresentation.stage_to_central line 73
  19. theorem OAI.KirchbergRordam.PrimeDropPresentation.to_central line 82
  20. abbrev OAI.KirchbergRordam.PrimeDropPresentation.Iteration.diagonalSystem line 94
  21. lemma OAI.KirchbergRordam.PrimeDropPresentation.Iteration.eigen_lipschitz line 102
  22. lemma OAI.KirchbergRordam.PrimeDropPresentation.Iteration.iterate_full line 105
  23. def OAI.KirchbergRordam.PrimeDropPresentation.Iteration.normalizedPath line 117
  24. lemma OAI.KirchbergRordam.PrimeDropPresentation.Iteration.normalizedPath_continuous line 120
  25. lemma OAI.KirchbergRordam.PrimeDropPresentation.Iteration.normalizedPath_zero line 122
  26. lemma OAI.KirchbergRordam.PrimeDropPresentation.Iteration.untwist line 125
  27. lemma OAI.KirchbergRordam.PrimeDropPresentation.Iteration.untwist_norm line 132
  28. lemma OAI.KirchbergRordam.PrimeDropPresentation.Iteration.eventually_untwist_small line 140
  29. def OAI.KirchbergRordam.PrimeDropPresentation.HalfFlip.mappedUnitary line 154
  30. lemma OAI.KirchbergRordam.PrimeDropPresentation.HalfFlip.mappedUnitary_control line 159
  31. lemma OAI.KirchbergRordam.PrimeDropPresentation.HalfFlip.finite_stage line 165
  32. lemma OAI.KirchbergRordam.PrimeDropPresentation.HalfFlip.common_stage line 188
  33. lemma OAI.KirchbergRordam.PrimeDropPresentation.HalfFlip.finite_control line 192
  34. theorem OAI.KirchbergRordam.PrimeDropPresentation.HalfFlip.exists_half_flip line 208
  35. lemma OAI.KirchbergRordam.PrimeDropPresentation.Channels.zeroCount line 219
  36. lemma OAI.KirchbergRordam.PrimeDropPresentation.Channels.oneCount line 222
  37. lemma OAI.KirchbergRordam.PrimeDropPresentation.Channels.block_const_left line 225
  38. def OAI.KirchbergRordam.PrimeDropPresentation.Channels.zeroRep line 231
  39. def OAI.KirchbergRordam.PrimeDropPresentation.Channels.oneRep line 236
  40. lemma OAI.KirchbergRordam.PrimeDropPresentation.Channels.zeroRep_bound line 241
  41. lemma OAI.KirchbergRordam.PrimeDropPresentation.Channels.oneRep_bound line 258