OAI/Analysis/CoulombIonization/Variational/BoundedDensityPotential.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoulombAnalysis.truncatedInvSquare line 18
2. lemma OAI.CoulombAnalysis.truncatedInvSquare_nonneg line 21
3. lemma OAI.CoulombAnalysis.truncatedInvSquare_integrable line 24
4. lemma OAI.CoulombAnalysis.truncatedInvSquare_integral line 36
5. lemma OAI.CoulombAnalysis.bounded_support_memLp line 43
6. lemma OAI.CoulombAnalysis.bounded_support_integrable line 51
7. lemma OAI.CoulombAnalysis.coulomb_inv_difference line 56
8. lemma OAI.CoulombAnalysis.support_distance_lt line 73
9. theorem OAI.CoulombAnalysis.bounded_density_potential_le line 79
10. theorem OAI.CoulombAnalysis.bounded_density_potential_difference line 103