OAI/Analysis/CoulombIonization/FormDomain/WeakChangeVariables.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.IsWeakDerivative.comp_linearEquiv line 20
  2. def OAI.CoulombAtom.weakGraphChangeAmbient line 56
  3. lemma OAI.CoulombAtom.weakGraphChangeAmbient_mem line 66
  4. def OAI.CoulombAtom.weakGraphChange line 75
  5. abbrev OAI.CoulombAtom.SectorHilbert line 82
  6. def OAI.CoulombAtom.permuteConfiguration line 84
  7. lemma OAI.CoulombAtom.permuteConfiguration_apply line 87
  8. lemma OAI.CoulombAtom.permuteConfiguration_preserving line 92
  9. def OAI.CoulombAtom.fermionPermutation line 96
  10. def OAI.CoulombAtom.fermionSpace line 105
  11. lemma OAI.CoulombAtom.mem_fermionSpace line 108
  12. lemma OAI.CoulombAtom.fermionSpace_isClosed line 112
  13. instance OAI.CoulombAtom.fermionSpace_completeSpace line 116
  14. abbrev OAI.CoulombAtom.sectorDirections line 119
  15. instance OAI.CoulombAtom.weakSectorGraph_normedAddCommGroup line 121
  16. instance OAI.CoulombAtom.weakSectorGraph_innerProductSpace line 123
  17. instance OAI.CoulombAtom.weakSectorGraph_normedSpace line 125
  18. abbrev OAI.CoulombAtom.SectorGraph line 128
  19. instance OAI.CoulombAtom.sectorGraph_normedAddCommGroup line 130
  20. instance OAI.CoulombAtom.sectorGraph_innerProductSpace line 132
  21. instance OAI.CoulombAtom.sectorGraph_normedSpace line 134
  22. def OAI.CoulombAtom.sectorGraphValue line 137
  23. lemma OAI.CoulombAtom.sectorGraphValue_apply line 143
  24. lemma OAI.CoulombAtom.sectorGraphValue_injective line 146
  25. def OAI.CoulombAtom.fermionGraph line 153
  26. instance OAI.CoulombAtom.fermionGraph_normedAddCommGroup line 156
  27. instance OAI.CoulombAtom.fermionGraph_innerProductSpace line 158
  28. instance OAI.CoulombAtom.fermionGraph_normedSpace line 160
  29. lemma OAI.CoulombAtom.fermionGraph_isClosed line 163
  30. instance OAI.CoulombAtom.fermionGraph_completeSpace line 166
  31. def OAI.CoulombAtom.fermionGraphValue line 169
  32. lemma OAI.CoulombAtom.fermionGraphValue_injective line 173