OAI/Analysis/CoulombIonization/FormDomain/FormRawPotential.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoulombAtom.rawPotential line 16
2. lemma OAI.CoulombAtom.rawPotential_nonneg line 18
3. lemma OAI.CoulombAtom.rawPotential_measurable line 21
4. lemma OAI.CoulombAtom.formRawLaw_integrable_iff line 24
5. lemma OAI.CoulombAtom.rawPotential_form_integrable line 32
6. lemma OAI.CoulombAtom.rawLocalPotential_le_raw line 42
7. lemma OAI.CoulombAtom.rawLocalPotential_form_integrable line 50
8. lemma OAI.CoulombAtom.formRawLaw_ae_no_poles line 56