OAI/Analysis/CoulombIonization/FieldAnalysis/WeakHarmonicRegularityBarrier.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAnalysis.packetSmooth_mean line 21
2. theorem OAI.CoulombAnalysis.weak_harmonic_regular_at line 31
3. theorem OAI.CoulombAnalysis.weak_harmonic_bounded_above_constant line 95
4. lemma OAI.CoulombAnalysis.compact_source_weak_poisson line 122
5. theorem OAI.CoulombAnalysis.compact_laplacian_representation line 137
6. theorem OAI.CoulombAnalysis.compact_laplacian_uniform_limit line 174