OAI/Analysis/CoulombIonization/RadialBounds/SharpOrdinaryCapBarrier.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.ordinaryDensity_raw_potential line 20
2. theorem OAI.CoulombAtom.sharp_unconditional_field_cap line 38
3. lemma OAI.CoulombAnalysis.ae_off_norm_sphere line 84
4. lemma OAI.CoulombAnalysis.rotation_kernel_integrable_off_sphere line 92
5. lemma OAI.CoulombAnalysis.L1_rotation_density_kernel_integrable line 101
6. lemma OAI.CoulombAnalysis.L1_potential_rotation_integrable line 125
7. theorem OAI.CoulombAnalysis.L1_sphereMean_potential line 131
8. lemma OAI.CoulombAnalysis.L1_residualCharge_le_sphereMean line 146
9. theorem OAI.CoulombAnalysis.L1_residualCharge_of_field_cap line 164