OAI/Analysis/LaughlinFock/PairNormalization.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Pair Normalization.

  1. def OAI.LaughlinFock.euler line 12
  2. def OAI.LaughlinFock.variance line 13
  3. theorem OAI.LaughlinFock.coeff_euler line 14
  4. theorem OAI.LaughlinFock.euler_mul line 19
  5. theorem OAI.LaughlinFock.euler_add line 23
  6. theorem OAI.LaughlinFock.variance_mul line 25
  7. theorem OAI.LaughlinFock.variance_X_add_one line 29
  8. theorem OAI.LaughlinFock.variance_X_add_one_pow line 32
  9. theorem OAI.LaughlinFock.weighted_antidiagonal line 41
  10. theorem OAI.LaughlinFock.pair_binomial_identity line 78
  11. theorem OAI.LaughlinFock.pairCoefficient_sq line 92
  12. theorem OAI.LaughlinFock.orbital_sum_eq_antidiagonal line 112
  13. theorem OAI.LaughlinFock.pairCoefficient_ordered_norm line 144
  14. theorem OAI.LaughlinFock.sum_eq_twice_upper line 166
  15. theorem OAI.LaughlinFock.pairCoefficient_norm line 193
  16. theorem OAI.LaughlinFock.pairCoefficient_orthogonal line 212