OAI/Analysis/Laughlin/Fock/SharpGap.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Laughlin.gammaStar line 10

    Also declared: ComparatorChallenges/LaughlinPlanar.lean:8 (same declaration text).

  2. theorem OAI.Laughlin.gammaStar_budget line 12
  3. theorem OAI.Laughlin.one_twenty_fifth_lt_gammaStar line 16
  4. theorem OAI.Laughlin.sharp_scalar_budget line 19
  5. theorem OAI.Laughlin.Fock.physical_fock_sharp_budget_eventually line 33
  6. theorem OAI.Laughlin.Fock.physical_fock_square_eventually_sharp line 48
  7. theorem OAI.Laughlin.Fock.physical_fock_square_uniform_sharp line 62
  8. theorem OAI.Laughlin.Fock.physical_fock_eigenvalue_gap_uniform_sharp line 68
  9. theorem OAI.Laughlin.Fock.physical_fock_kernel_distance_uniform_sharp line 87