OAI/Analysis/LaughlinGap/NestedAveraging.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Nested Averaging.

  1. def OAI.LaughlinGap.Spin.LadderMap.changeSource line 19
  2. lemma OAI.LaughlinGap.Spin.LadderMap.changeSource_single line 23
  3. lemma OAI.LaughlinGap.Spin.nestedTensor_weight_support line 30
  4. lemma OAI.LaughlinGap.Spin.nestedTensor_flip line 42
  5. def OAI.LaughlinGap.Spin.nestedAtDeficit line 52
  6. lemma OAI.LaughlinGap.Spin.nestedAtDeficit_single line 57
  7. lemma OAI.LaughlinGap.RealOccupation.Covariant.equal_descendant_average line 71
  8. lemma OAI.LaughlinGap.RealOccupation.Covariant.distinct_descendant_average line 83
  9. def OAI.LaughlinGap.RealOccupation.physicalFour line 91
  10. lemma OAI.LaughlinGap.RealOccupation.physicalFour_covariant line 96
  11. lemma OAI.LaughlinGap.RealOccupation.annihilation_anticommute' line 101
  12. lemma OAI.LaughlinGap.RealOccupation.physicalFour_flip line 107
  13. lemma OAI.LaughlinGap.RealOccupation.four_combination_flip line 112
  14. lemma OAI.LaughlinGap.RealOccupation.physicalFour_even_null line 127