OAI/Analysis/CoulombIonization/FieldAnalysis/BoundedL1PoissonBarrier.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAnalysis.bounded_L1_laplacian_pair_integrable line 21
2. theorem OAI.CoulombAnalysis.bounded_L1_weak_poisson line 39
3. def OAI.CoulombBarrier.meanFieldOffset line 65
4. lemma OAI.CoulombBarrier.meanFieldOffset_weak_nuclear line 67
5. lemma OAI.CoulombAnalysis.weak_poisson_plus_potential_harmonic line 99
6. theorem OAI.CoulombAnalysis.exists_weak_poisson_L1_constants line 117