OAI/Analysis/CoulombIonization/Fermionic/Pull.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombPauli.pull line 20
  2. lemma OAI.CoulombPauli.pull_ae line 23
  3. lemma OAI.CoulombPauli.pull_norm line 26
  4. lemma OAI.CoulombPauli.pull_inner line 29
  5. lemma OAI.CoulombPauli.pull_involution line 33
  6. lemma OAI.CoulombPauli.pull_symm line 44
  7. lemma OAI.CoulombPauli.pull_injective line 51
  8. abbrev OAI.CoulombPauli.configMeasure line 60
  9. abbrev OAI.CoulombPauli.sectorL2 line 61
  10. lemma OAI.CoulombPauli.memLp_pure line 63
  11. def OAI.CoulombPauli.pureTensor line 74
  12. lemma OAI.CoulombPauli.pureTensor_ae line 77
  13. def OAI.CoulombPauli.splitAt line 80
  14. lemma OAI.CoulombPauli.splitAt_preserving line 83
  15. lemma OAI.CoulombPauli.pureTensor_split line 87
  16. lemma OAI.CoulombPauli.pureTensor_zero_inner line 103
  17. lemma OAI.CoulombPauli.eq_zero_of_pureTensor_orthogonal line 120
  18. lemma OAI.CoulombPauli.continuousLinearMap_ext_pure line 151
  19. lemma OAI.CoulombPauli.pull_adjoint_pull line 167
  20. def OAI.CoulombPauli.insertOrbital line 174
  21. def OAI.CoulombPauli.projectOrbital line 178
  22. lemma OAI.CoulombPauli.insertOrbital_adjoint_pure line 182
  23. lemma OAI.CoulombPauli.insertOrbital_pure line 190
  24. lemma OAI.CoulombPauli.projectOrbital_pure line 196
  25. def OAI.CoulombPauli.permCoords line 202
  26. lemma OAI.CoulombPauli.permCoords_apply line 205
  27. lemma OAI.CoulombPauli.permCoords_preserving line 210
  28. def OAI.CoulombPauli.permute line 214
  29. lemma OAI.CoulombPauli.permute_norm line 217
  30. lemma OAI.CoulombPauli.permute_pure line 220
  31. lemma OAI.CoulombPauli.projectOrbital_covariance line 231