OAI/Analysis/CoulombIonization/FormDomain/WeakDerivativeSmulL2.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.weak_derivative_smul_L2 line 23
2. def OAI.CoulombLT.fermionDensity line 44
3. lemma OAI.CoulombLT.fermionDensity_eq_family line 49
4. lemma OAI.CoulombLT.fermion_lt_numeric line 80
5. theorem OAI.CoulombLT.fermion_lieb_thirring line 95