OAI/Analysis/CoulombIonization/FormDomain/FourierMomentGradient.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombLT.fourierMoment_le_gradient line 27
2. theorem OAI.CoulombLT.weak_family_lieb_thirring line 47
3. lemma OAI.CoulombLT.besselFamily_of_unit line 69
4. lemma OAI.CoulombLT.spinMarginal_coefficient line 90
5. lemma OAI.CoulombLT.sum_insert_adjoint_sq_le line 98
6. def OAI.CoulombLT.fermionFamily line 108
7. lemma OAI.CoulombLT.fermionFamily_coefficient_sum line 114
8. lemma OAI.CoulombLT.fermionFamily_bessel line 142