OAI/Analysis/CoulombRadii/RandomFields/PhysicalLikelihoodBridge.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NeutralAtom.flattenObservationNoise line 14
  2. lemma OAI.NeutralAtom.flattenObservationNoise_preserving line 24
  3. def OAI.NeutralAtom.observationCoordinateData line 40
  4. lemma OAI.NeutralAtom.measurable_observationCoordinateData line 44
  5. lemma OAI.NeutralAtom.observationCoordinateData_positions line 49
  6. lemma OAI.NeutralAtom.arrayEventLikelihood_nested_integral line 58
  7. lemma OAI.NeutralAtom.rawExpectation_eq_stateWeightedIntegral line 68
  8. theorem OAI.NeutralAtom.physical_arrayEvent_bayes_integral line 78
  9. def OAI.NeutralAtom.coordinateTailObservation line 119
  10. lemma OAI.NeutralAtom.measurable_coordinateTailObservation line 123
  11. lemma OAI.NeutralAtom.coordinateTailObservation_permute line 134
  12. lemma OAI.NeutralAtom.coordinateTailObservation_physical line 143
  13. lemma OAI.NeutralAtom.physical_tailEvent_bayes_integral line 153
  14. lemma OAI.NeutralAtom.physical_tailEvent_probability line 173
  15. theorem OAI.NeutralAtom.physical_tailEvent_state line 186