OAI/Analysis/LaughlinFock/LocalEnergy.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Local Energy.

  1. theorem OAI.LaughlinFock.coefficientPairAnnihilator_smul line 15
  2. def OAI.LaughlinFock.localPairAnnihilator line 29
  3. def OAI.LaughlinFock.limitPairAnnihilator line 34
  4. def OAI.LaughlinFock.localDelta line 37
  5. def OAI.LaughlinFock.localDeltaInv line 40
  6. theorem OAI.LaughlinFock.localDelta_factor_ne_zero line 43
  7. theorem OAI.LaughlinFock.localDelta_inv_mul line 47
  8. theorem OAI.LaughlinFock.localDelta_mul_inv line 51
  9. theorem OAI.LaughlinFock.localPair_conjugation line 56
  10. theorem OAI.LaughlinFock.localFour_conjugation line 72
  11. theorem OAI.LaughlinFock.localDelta_tendsto line 92
  12. theorem OAI.LaughlinFock.localDeltaInv_tendsto line 109
  13. theorem OAI.LaughlinFock.localDelta_posSemidef line 128
  14. theorem OAI.LaughlinFock.localDelta_le_identity line 135
  15. theorem OAI.LaughlinFock.localDelta_contraction line 145
  16. theorem OAI.LaughlinFock.gram_bound_of_scaled_contraction line 163
  17. def OAI.LaughlinFock.localHamiltonian line 186
  18. def OAI.LaughlinFock.limitHamiltonian line 189
  19. theorem OAI.LaughlinFock.localPair_energy_transfer line 192
  20. theorem OAI.LaughlinFock.localHamiltonian_energy_transfer line 211
  21. theorem OAI.LaughlinFock.star_dotProduct_self line 223
  22. theorem OAI.LaughlinFock.row_isometry_gram_complement line 228
  23. theorem OAI.LaughlinFock.row_isometry_contracts line 245
  24. theorem OAI.LaughlinFock.row_isometry_contracts_family line 256
  25. theorem OAI.LaughlinFock.twoAnnihilators_contract line 264
  26. theorem OAI.LaughlinFock.limitHamiltonian_quadratic_form line 272
  27. theorem OAI.LaughlinFock.finite_annihilator_family_bound line 281
  28. def OAI.LaughlinFock.entryNormBound line 302
  29. theorem OAI.LaughlinFock.entryNormBound_nonneg line 305
  30. theorem OAI.LaughlinFock.entryNormBound_quadratic_form line 309
  31. theorem OAI.LaughlinFock.entryNormBound_lower_bound line 335
  32. theorem OAI.LaughlinFock.entryNormBound_tendsto_zero line 352
  33. theorem OAI.LaughlinFock.relative_compression_bound line 365