OAI/Analysis/CoulombIonization/Localization/Cut.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombPackets.cutLinear line 20
  2. lemma OAI.CoulombPackets.cutLinear_norm_le line 43
  3. def OAI.CoulombPackets.cut line 51
  4. lemma OAI.CoulombPackets.cut_norm_sq line 54
  5. def OAI.CoulombPackets.selectedFrame line 67
  6. def OAI.CoulombPackets.densityMatrix line 72
  7. lemma OAI.CoulombPackets.densityMatrix_positive line 76
  8. lemma OAI.CoulombPackets.selectedFrame_norm_le line 80
  9. lemma OAI.CoulombPackets.densityMatrix_le_one line 86
  10. lemma OAI.CoulombPackets.densityMatrix_schwartz_form line 100
  11. def OAI.CoulombPackets.packetFunction line 114
  12. lemma OAI.CoulombPackets.packetFunction_norm line 118
  13. lemma OAI.CoulombPackets.packetFunction_memLp line 122
  14. def OAI.CoulombPackets.packet line 131
  15. lemma OAI.CoulombPackets.packet_norm_sq line 134
  16. lemma OAI.CoulombPackets.packet_frameFunction line 145
  17. lemma OAI.CoulombPackets.frame_ae_packet line 156