OAI/Analysis/CoulombIonization/Localization/FermionL2.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombPackets.spinPartialOccupation_integrable line 23
2. lemma OAI.CoulombPackets.spinPartialOccupation_total_integral line 41
3. abbrev OAI.CoulombPackets.fermionL2 line 61
4. def OAI.CoulombPackets.splitFermion line 63
5. lemma OAI.CoulombPackets.splitFermion_norm line 67
6. lemma OAI.CoulombPackets.insert_adjoint_split line 70
7. def OAI.CoulombPackets.fermionHusimi line 77
8. lemma OAI.CoulombPackets.fermionHusimi_eq line 81
9. lemma OAI.CoulombPackets.fermionHusimi_integrable line 87
10. lemma OAI.CoulombPackets.fermionHusimi_mass line 96
11. lemma OAI.CoulombPackets.fermionHusimi_nonneg line 103
12. lemma OAI.CoulombPackets.fermionHusimi_le_two line 107