OAI/Analysis/CoulombRadii/RandomFields/ObservedUnordered.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.NeutralAtom.unorderedSum line 13
2. theorem OAI.NeutralAtom.unorderedSum_forgetOrder line 18
3. lemma OAI.NeutralAtom.measurable_unorderedSum line 21
4. lemma OAI.NeutralAtom.unorderedSum_bound line 27
5. lemma OAI.NeutralAtom.observationNoiseLaw_ae_support line 34
6. lemma OAI.NeutralAtom.allObservationNoiseLaw_ae_support line 41
7. lemma OAI.NeutralAtom.observationNoiseVector_norm_le line 49
8. lemma OAI.NeutralAtom.observationLaw_ae_displacement line 59
9. lemma OAI.NeutralAtom.unorderedSum_tail_stronglyMeasurable line 71
10. theorem OAI.NeutralAtom.physical_posterior_kernel_matching line 85