OAI/Analysis/CoulombIonization/Variational/CutExpectedOut.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.orderedCutForm_zero_of_factor line 126
2. lemma OAI.CoulombAtom.cut_exterior_energy_lower line 142
3. def OAI.CoulombAtom.cutExpectedOut line 162
4. lemma OAI.CoulombAtom.cutExpectedOut_nonneg line 166
5. theorem OAI.CoulombAtom.fock_priced_exterior_bound line 171
6. lemma OAI.CoulombAtom.weightedParticleCount_le_const line 189
7. theorem OAI.CoulombAtom.radial_priced_exterior_bound line 208