OAI/Analysis/CoulombIonization/Localization/OriginalPosteriorMomentBarrier.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombBarrier.bounded_integrable_square line 22
2. lemma OAI.CoulombBarrier.square_integral_le_of_bound line 30
3. lemma OAI.CoulombBarrier.bounded_original_posterior_mean line 37
4. theorem OAI.CoulombBarrier.original_posterior_square_le line 54
5. theorem OAI.CoulombBarrier.original_master_second_moment_from_count line 83