OAI/Analysis/Laughlin/FourBody/ErrorLimit.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Laughlin.Spin.sourceAlpha line 10
  2. def OAI.Laughlin.Spin.fourErrorEntry line 15
  3. def OAI.Laughlin.Spin.fourErrorLimitEntry line 22
  4. theorem OAI.Laughlin.Spin.fourErrorEntry_tendsto line 29
  5. theorem OAI.Laughlin.Spin.physical_list_sum_tendsto line 41
  6. theorem OAI.Laughlin.Spin.source_rows_admissible line 50
  7. def OAI.Laughlin.Spin.fourErrorRow line 53
  8. def OAI.Laughlin.Spin.fourErrorLimitRow line 55
  9. def OAI.Laughlin.Spin.physicalFourError line 58
  10. def OAI.Laughlin.Spin.limitFourError line 60
  11. theorem OAI.Laughlin.Spin.physicalFourError_tendsto line 63