OAI/Analysis/CoulombRadii/ThomasFermi/FirstFiber.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Coulomb.firstFiber line 12
2. lemma OAI.Coulomb.firstFiber_memLp line 15
3. lemma OAI.Coulomb.lowProjection_density_pauli line 32
4. lemma OAI.Coulomb.norm_sq_le_two_norm_sq_add_sub line 52
5. lemma OAI.Coulomb.fiber_norm_sq_split line 58