OAI/Analysis/CoulombRadii/SpectralTheory/SectorBottomBridge.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.NeutralAtom.sectorEnergy_eq_formBottom line 16
2. lemma OAI.NeutralAtom.unrestrictedEnergy_eq_formBottom line 31
3. lemma OAI.Coulomb.atom_sectorFormBottom_antitone line 37
4. lemma OAI.Coulomb.atom_sectorFormBottom_real line 43
5. lemma OAI.Coulomb.slice_core_form_ge_sector line 58
6. lemma OAI.Coulomb.atom_sector_trial_approx line 82
7. lemma OAI.Coulomb.kinetic_bound_of_form_bound line 91
8. lemma OAI.Coulomb.atom_normalized_form_ge_bottom line 104
9. lemma OAI.Coulomb.atom_minimizing_sequence line 109