OAI/Analysis/CoulombIonization/RadialBounds/PatchFailureMass.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.weighted_markov_integral line 17
2. def OAI.CoulombAtom.radialPatchGapSample line 32
3. lemma OAI.CoulombAtom.radialPatchGapSample_nonneg line 40
4. lemma OAI.CoulombAtom.radialPatchGapSample_aemeasurable line 46
5. def OAI.CoulombAtom.radialPatchFailureMass line 54
6. lemma OAI.CoulombAtom.radialPatchFailureMass_mem_Icc line 61
7. lemma OAI.CoulombAtom.radial_weightedPatchGap_integrable line 90
8. theorem OAI.CoulombAtom.radial_patch_failure_markov line 112