OAI/Analysis/CoulombIonization/Localization/ActualPosteriorCapBarrier.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.jointMasterPosterior_potential_measurable line 20
2. lemma OAI.CoulombAtom.normalized_setIntegral_const_sub line 31
3. def OAI.CoulombAtom.dyadicUniformEventBudget line 39
4. lemma OAI.CoulombAtom.dyadicUniformEventBudget_nonneg line 42
5. lemma OAI.CoulombAtom.dyadicUniformEventBudget_mono line 52
6. theorem OAI.CoulombAtom.actual_posterior_pointwise_cap line 67