OAI/Analysis/Laughlin/FourBody/FastChoose.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Laughlin.Certificate.UFast line 7
  2. theorem OAI.Laughlin.Certificate.U_eq_fast line 14
  3. def OAI.Laughlin.Certificate.VFast line 17
  4. theorem OAI.Laughlin.Certificate.V_eq_fast line 20
  5. def OAI.Laughlin.Certificate.yEntryIntegralFast line 23
  6. theorem OAI.Laughlin.Certificate.yEntryIntegral_eq_fast line 36
  7. def OAI.Laughlin.Certificate.yRowIntegralFast line 40
  8. theorem OAI.Laughlin.Certificate.yRowIntegral_eq_fast line 43
  9. theorem OAI.Laughlin.Certificate.source_yRow_eq_fastIntegral line 47
  10. def OAI.Laughlin.Certificate.LFast line 51
  11. def OAI.Laughlin.Certificate.ZFast line 60
  12. theorem OAI.Laughlin.Certificate.L_eq_fast line 66
  13. theorem OAI.Laughlin.Certificate.Z_eq_fast line 69