OAI/Analysis/CoulombIonization/FormDomain/CosetWedge.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CoulombAtom.cosetWedgeFintype line 16
2. def OAI.CoulombAtom.SubgroupFermion line 19
3. def OAI.CoulombAtom.cosetWedgeTerm line 23
4. def OAI.CoulombAtom.cosetWedge line 27
5. lemma OAI.CoulombAtom.cosetWedgeTerm_value line 30
6. lemma OAI.CoulombAtom.SobolevVector.cosetWedgeTerm line 36
7. lemma OAI.CoulombAtom.cosetWedge_fermion line 41
8. lemma OAI.CoulombAtom.formMass_cosetWedgeTerm line 94
9. lemma OAI.CoulombAtom.formEnergy_cosetWedgeTerm line 99
10. lemma OAI.CoulombAtom.formMass_cosetWedge line 104
11. lemma OAI.CoulombAtom.formEnergy_cosetWedge line 110
12. theorem OAI.CoulombAtom.normalized_coset_wedge_trial line 116