OAI/Analysis/Laughlin/Spin/HighestSpace.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Laughlin.Spin.highestRaw_zero line 9
  2. theorem OAI.Laughlin.Spin.highestRaw_ne_zero line 13
  3. theorem OAI.Laughlin.Spin.highest_unique line 24
  4. def OAI.Laughlin.Spin.highestNorm line 40
  5. def OAI.Laughlin.Spin.highestUnit line 43
  6. theorem OAI.Laughlin.Spin.highestNorm_pos line 46
  7. theorem OAI.Laughlin.Spin.highestUnit_norm line 54
  8. theorem OAI.Laughlin.Spin.highestUnit_raising line 62
  9. theorem OAI.Laughlin.Spin.highestUnit_ne_zero line 68
  10. theorem OAI.Laughlin.Spin.highestUnit_ratio line 73
  11. def OAI.Laughlin.Spin.raiseSlice line 85
  12. theorem OAI.Laughlin.Spin.raiseSlice_kernel line 89