OAI/Analysis/CoulombIonization/ThomasFermi/QuantumSectorNearMinimizer.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CoulombAtom.quantum_sector_near_minimizer line 81
2. lemma OAI.CoulombAtom.quantum_price_le_sector line 104
3. theorem OAI.CoulombAtom.quantum_priced_near_minimizer line 110
4. theorem OAI.CoulombAtom.SobolevFermion.priced_lower_bound line 120
5. theorem OAI.CoulombAtom.conditional_core_priced_energy line 129
6. theorem OAI.CoulombAtom.integrated_core_priced_energy line 135
7. theorem OAI.CoulombAtom.quantum_priced_partition_excess line 144