OAI/Analysis/CoulombIonization/Localization/UniformObservationNoiseBarrier.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.uniform_observation_noise_eventually line 18
2. lemma OAI.CoulombAtom.raw_annular_count_le_observed line 48
3. lemma OAI.CoulombAtom.observedAnnularCount_integrable line 65
4. lemma OAI.CoulombAtom.original_posterior_annular_count_le_observed line 76
5. lemma OAI.CoulombBarrier.posterior_density_le_raw_ball_count line 118
6. lemma OAI.CoulombBarrier.integral_raw_ball_le_annular line 159
7. theorem OAI.CoulombBarrier.exists_posterior_annular_density_constant line 171