OAI/Analysis/LaughlinGap/FourBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Four Bound.

  1. lemma OAI.LaughlinGap.RealOccupation.four_comparison_summed line 16
  2. lemma OAI.LaughlinGap.RealOccupation.rearrange_comparison line 31
  3. lemma OAI.LaughlinGap.RealOccupation.four_comparison_pointwise line 38
  4. theorem OAI.LaughlinGap.RealOccupation.four_comparison_of_certificates line 57