OAI/Analysis/CoulombRadii/RandomFields/ConditionalMatching.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NeutralAtom.condExp_matching line 15
  2. theorem OAI.NeutralAtom.master_kernel_posterior_matching line 45
  3. def OAI.NeutralAtom.configurationOrderSetoid line 125
  4. def OAI.NeutralAtom.UnorderedArray line 138
  5. def OAI.NeutralAtom.forgetOrder line 140
  6. instance OAI.NeutralAtom.unorderedArrayMeasurable line 142
  7. theorem OAI.NeutralAtom.measurable_forgetOrder line 145
  8. theorem OAI.NeutralAtom.forgetOrder_permutation line 148
  9. abbrev OAI.NeutralAtom.ObservationNoise line 153
  10. abbrev OAI.NeutralAtom.ObservationSample line 154
  11. def OAI.NeutralAtom.allObservationNoiseLaw line 156
  12. instance OAI.NeutralAtom.allObservationNoiseLaw_probability line 160
  13. def OAI.NeutralAtom.observationLaw line 165
  14. instance OAI.NeutralAtom.observationLaw_probability line 168
  15. theorem OAI.NeutralAtom.observationLaw_rawProjection line 173
  16. def OAI.NeutralAtom.observationNoiseVector line 176
  17. theorem OAI.NeutralAtom.observationNoiseVector_coordinate line 179
  18. theorem OAI.NeutralAtom.continuous_observationNoiseVector line 183
  19. def OAI.NeutralAtom.observedOrdered line 187
  20. def OAI.NeutralAtom.observedArray line 191
  21. theorem OAI.NeutralAtom.measurable_observedOrdered line 195
  22. theorem OAI.NeutralAtom.measurable_observedArray line 204
  23. def OAI.NeutralAtom.tailObservation line 208
  24. theorem OAI.NeutralAtom.measurable_tailObservation line 212
  25. def OAI.NeutralAtom.observationSigma line 221
  26. theorem OAI.NeutralAtom.observationSigma_le line 225
  27. def OAI.NeutralAtom.eraseEarlierArrays line 229
  28. theorem OAI.NeutralAtom.measurable_eraseEarlierArrays line 232
  29. theorem OAI.NeutralAtom.tailObservation_erase line 241
  30. theorem OAI.NeutralAtom.observationSigma_antitone line 249
  31. theorem OAI.NeutralAtom.observationSigma_trivial line 256