OAI/Analysis/CoulombIonization/Variational/IntegrableCutTower.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.weighted_coreSlice_eq_full_integrable line 18
2. lemma OAI.CoulombAtom.cutOuter_expectation_eq_full_integrable line 40
3. def OAI.CoulombAtom.rawLocalPotential line 67
4. lemma OAI.CoulombAtom.rawLocalPotential_nonneg line 70
5. lemma OAI.CoulombAtom.rawLocalPotential_measurable line 78
6. lemma OAI.CoulombAtom.rawLocalPotential_weighted_integrable line 85
7. lemma OAI.CoulombAtom.rawLocalPotential_core_integrable line 97
8. lemma OAI.CoulombAtom.rawLocalPotential_out_weighted_integrable line 109
9. lemma OAI.CoulombAtom.rawLocalPotential_cutOutPositions_le line 121
10. lemma OAI.CoulombAtom.rawLocalPotential_cut_weighted_integrable line 135
11. theorem OAI.CoulombAtom.fresh_cut_raw_local_control line 153