OAI/Analysis/CoulombIonization/ThomasFermi/FlatFermionGradient.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombNeumann.flatSignedPermutation_gradient line 20
2. lemma OAI.CoulombNeumann.flatFermionAverage_gradient line 33
3. lemma OAI.CoulombNeumann.flatSignedPermutation_gradient_memLp line 48
4. lemma OAI.CoulombNeumann.flatFermionAverage_gradient_memLp line 58
5. lemma OAI.CoulombNeumann.flatSignedPermutation_kinetic line 67
6. lemma OAI.CoulombNeumann.flatFermionAverage_kinetic_le line 94
7. def OAI.CoulombNeumann.FlatAEAntisymmetric line 121
8. lemma OAI.CoulombNeumann.flatSignedPermutation_ae_fixed line 125
9. lemma OAI.CoulombNeumann.flatFermionAverage_ae_fixed line 136
10. lemma OAI.CoulombNeumann.flatFermionAverage_ae_tendsto line 147