OAI/Analysis/CoulombRadii/RandomFields/ObservationMatching.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.NeutralAtom.observationProductDensity_ne_zero_support line 13
  2. lemma OAI.NeutralAtom.arrayEventLikelihood_pos_matching line 20
  3. def OAI.NeutralAtom.observationArrayPositions line 37
  4. lemma OAI.NeutralAtom.observationArrayPositions_displacement line 41
  5. lemma OAI.NeutralAtom.observed_annular_count_le line 60
  6. lemma OAI.NeutralAtom.observed_annular_event_implies_raw_count line 79
  7. lemma OAI.NeutralAtom.measurable_observationArrayPositions line 90
  8. lemma OAI.NeutralAtom.observed_annular_event_measurable line 95
  9. lemma OAI.NeutralAtom.observed_annular_event_symmetric line 102
  10. lemma OAI.NeutralAtom.stateWeightedIntegral_mono_bounded line 117
  11. lemma OAI.NeutralAtom.stateWeightedIntegral_const_mul line 128
  12. lemma OAI.NeutralAtom.event_count_square_lower line 134
  13. lemma OAI.NeutralAtom.observationEventOffset_mono_probability line 163
  14. theorem OAI.NeutralAtom.atomic_observed_annular_count_tail line 173