OAI/Analysis/CoulombIonization/Localization/ObservationScoreMoments.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombObservation.pow_mul_exp_neg_le line 17
2. lemma OAI.CoulombObservation.compactNoiseScore_weight_bound line 27
3. lemma OAI.CoulombObservation.compactNoiseScore_weight_integrable line 64
4. lemma OAI.CoulombObservation.compactNoiseScore_moment_integrable line 80
5. def OAI.CoulombObservation.compactScoreConstant line 88
6. lemma OAI.CoulombObservation.compactScoreConstant_pos line 90
7. lemma OAI.CoulombObservation.compactNoiseScore_moment_le line 95
8. lemma OAI.CoulombObservation.compactNoiseLaw_neg_preserving line 134