OAI/Analysis/CoulombRadii/RandomFields/PhysicalRetainedLikelihood.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NeutralAtom.flattenIndexedNoise line 13
  2. lemma OAI.NeutralAtom.flattenIndexedNoise_preserving line 23
  3. abbrev OAI.NeutralAtom.RetainedScales line 39
  4. def OAI.NeutralAtom.retainedNoise line 41
  5. lemma OAI.NeutralAtom.retainedNoise_preserving line 45
  6. def OAI.NeutralAtom.retainedObservationData line 58
  7. lemma OAI.NeutralAtom.measurable_retainedObservationData line 62
  8. lemma OAI.NeutralAtom.arrayEventLikelihood_retained_integral line 67
  9. theorem OAI.NeutralAtom.physical_retainedEvent_bayes_integral line 79
  10. def OAI.NeutralAtom.retainedTailObservation line 118
  11. lemma OAI.NeutralAtom.measurable_retainedTailObservation line 122
  12. lemma OAI.NeutralAtom.retainedTailObservation_permute line 133
  13. lemma OAI.NeutralAtom.retainedTailObservation_physical line 142
  14. lemma OAI.NeutralAtom.physical_retainedTailEvent_bayes_integral line 156
  15. lemma OAI.NeutralAtom.physical_retainedTailEvent_probability line 176
  16. theorem OAI.NeutralAtom.physical_retainedTailEvent_state line 189