OAI/Analysis/CoulombIonization/Variational/CoherentDensityTrace.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.nonneg_series_eq_of_integral line 17
2. lemma OAI.CoulombAtom.coherentOrbital_density_tsum line 34
3. lemma OAI.CoulombAtom.nonneg_series_weight_hasSum line 54
4. lemma OAI.CoulombAtom.coherentOrbital_density_hasSum line 73
5. lemma OAI.CoulombAtom.coherentOrbital_weight_hasSum line 84
6. lemma OAI.CoulombAtom.coherentDensity_bounded_weight_integrable line 102