OAI/Analysis/CoulombIonization/FieldAnalysis/InnerFieldCap.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoulombAtom.innerFieldTestAnnulus line 14
2. lemma OAI.CoulombAtom.innerFieldTestAnnulus_measurable line 16
3. lemma OAI.CoulombAtom.innerFieldTestAnnulus_finite line 20
4. lemma OAI.CoulombAtom.positiveCoreField_annular_integrable line 24
5. lemma OAI.CoulombAtom.packet_on_inner_annulus line 36
6. lemma OAI.CoulombAtom.positiveCoreField_packet_le line 45
7. def OAI.CoulombAtom.actualInnerBoundaryCap line 77
8. lemma OAI.CoulombAtom.actualInnerBoundaryCap_nonneg line 82
9. theorem OAI.CoulombAtom.actual_inner_boundary_cap line 89
10. theorem OAI.CoulombAtom.actual_inner_exterior_cap line 145