OAI/Analysis/CoulombIonization/Localization/Trace.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombPackets.basis_packet_parseval line 23
  2. lemma OAI.CoulombPackets.selectedFrame_norm_sq_lintegral line 35
  3. lemma OAI.CoulombPackets.densityMatrix_trace line 45
  4. lemma OAI.CoulombPackets.packet_coefficient_measurable line 76
  5. lemma OAI.CoulombPackets.packet_plancherel line 84
  6. def OAI.CoulombPackets.partialOccupation line 103
  7. lemma OAI.CoulombPackets.partialOccupation_measurable line 106
  8. lemma OAI.CoulombPackets.partialOccupation_mass line 122
  9. lemma OAI.CoulombPackets.partialOccupation_integrable line 144
  10. lemma OAI.CoulombPackets.partialOccupation_integral line 158
  11. def OAI.CoulombPackets.spinVector line 171
  12. lemma OAI.CoulombPackets.spinVector_inner line 174
  13. lemma OAI.CoulombPackets.spinVector_orthonormal line 179
  14. def OAI.CoulombPackets.spinBasis line 191
  15. lemma OAI.CoulombPackets.spinBasis_apply line 204
  16. abbrev OAI.CoulombPackets.spinSpaceMeasure line 210
  17. def OAI.CoulombPackets.spinPacket line 212
  18. lemma OAI.CoulombPackets.spinPacket_norm line 215
  19. lemma OAI.CoulombPackets.spinPacket_coefficient line 222
  20. lemma OAI.CoulombPackets.spinPacket_plancherel line 228