OAI/Analysis/LaughlinGap/Creation.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Creation.

  1. lemma OAI.LaughlinGap.Occupation.creation_anticommute line 14
  2. def OAI.LaughlinGap.Occupation.creationCombination line 20
  3. lemma OAI.LaughlinGap.Occupation.creationCombination_square line 25
  4. def OAI.LaughlinGap.Occupation.creationExteriorHom line 47
  5. lemma OAI.LaughlinGap.Occupation.creationCombination_single line 51
  6. lemma OAI.LaughlinGap.Occupation.creationExteriorHom_multi line 56
  7. lemma OAI.LaughlinGap.Occupation.word_ofFn_swap line 69
  8. theorem OAI.LaughlinGap.Occupation.normalizedReadout_antisymmetric line 81
  9. lemma OAI.LaughlinGap.Antisymmetric.perm line 92
  10. lemma OAI.LaughlinGap.Antisymmetric.eq_zero_of_not_injective line 99
  11. lemma OAI.LaughlinGap.Antisymmetric.ext_increasing line 115
  12. def OAI.LaughlinGap.Occupation.increasingConfiguration line 133
  13. lemma OAI.LaughlinGap.Occupation.increasingConfiguration_strictMono line 136
  14. lemma OAI.LaughlinGap.Occupation.ofFn_increasingConfiguration line 139
  15. lemma OAI.LaughlinGap.Occupation.normalizedReadout_increasing line 144
  16. def OAI.LaughlinGap.Occupation.coordinatesFromTensor line 151
  17. lemma OAI.LaughlinGap.Occupation.coordinatesFromTensor_apply line 158
  18. lemma OAI.LaughlinGap.Occupation.coordinatesFromTensor_readout line 163
  19. theorem OAI.LaughlinGap.Occupation.readout_coordinatesFromTensor line 172
  20. lemma OAI.LaughlinGap.Occupation.sectorReadout_inclusion line 190
  21. lemma OAI.LaughlinGap.Occupation.sectorInclusion_norm_sq line 195
  22. def OAI.LaughlinGap.Occupation.exteriorTensorIsometry line 200
  23. lemma OAI.LaughlinGap.unitary_conj_eq_of_quadraticForm line 219
  24. lemma OAI.LaughlinGap.Occupation.sum_symmetric_triangle line 241
  25. lemma OAI.LaughlinGap.Occupation.orderedPair_contraction line 256
  26. lemma OAI.LaughlinGap.Occupation.update_cons_cons line 278
  27. lemma OAI.LaughlinGap.Occupation.readout_pairAmplitude_head line 292
  28. def OAI.LaughlinGap.pairEnergyAt line 325
  29. lemma OAI.LaughlinGap.sum_head_anchored line 328
  30. lemma OAI.LaughlinGap.pairAmplitude_perm line 345
  31. lemma OAI.LaughlinGap.pairEnergyAt_perm line 354
  32. lemma OAI.LaughlinGap.exists_perm_head_pair line 366
  33. lemma OAI.LaughlinGap.pairEnergyAt_eq_head line 381
  34. theorem OAI.LaughlinGap.Occupation.readout_pairEnergyAt_head line 392
  35. lemma OAI.LaughlinGap.sum_increasing_positions line 415
  36. lemma OAI.LaughlinGap.energy_eq_pairEnergyAt_head line 422
  37. theorem OAI.LaughlinGap.Occupation.readout_energy line 442
  38. def OAI.LaughlinGap.Occupation.exteriorHamiltonian line 456
  39. lemma OAI.LaughlinGap.Occupation.exteriorHamiltonian_positive line 460
  40. lemma OAI.LaughlinGap.Occupation.exteriorHamiltonian_inner line 464
  41. lemma OAI.LaughlinGap.Occupation.exteriorHamiltonian_inclusion line 472
  42. theorem OAI.LaughlinGap.Occupation.tensor_exteriorHamiltonian line 478
  43. lemma OAI.LaughlinGap.Occupation.exteriorTensorIsometry_intertwines line 488
  44. lemma OAI.LaughlinGap.Occupation.exteriorTensorIsometry_hamiltonian_norm_sq line 495
  45. theorem OAI.LaughlinGap.Occupation.sector_square_of_occupation_square line 507
  46. theorem OAI.LaughlinGap.Occupation.mainTarget_of_uniform_occupation_square_estimate line 520