OAI/Analysis/CoulombRadii/RandomFields/PosteriorDensityContinuity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NeutralAtom.mixturePacketDensity_continuous line 11
2. lemma OAI.NeutralAtom.conditionalPacketDensity_continuous line 28
3. lemma OAI.NeutralAtom.measurable_conditionalPacketDensity_joint line 36
4. def OAI.NeutralAtom.posteriorAverage line 60
5. lemma OAI.NeutralAtom.posteriorAverage_joint_measurable line 62
6. lemma OAI.NeutralAtom.posteriorAverage_uniform_bounds line 68
7. lemma OAI.NeutralAtom.posterior_ae line 80
8. lemma OAI.NeutralAtom.posteriorAverage_invariant line 85
9. instance OAI.NeutralAtom.observationNoise_standardBorel line 106
10. instance OAI.NeutralAtom.observationSample_standardBorel line 110
11. lemma OAI.NeutralAtom.ae_all_position_eq line 121
12. theorem OAI.NeutralAtom.posteriorPacketDensity_tower line 130