OAI/Analysis/CoulombIonization/Localization/DyadicObservation.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombObservation.dyadicObservationWidth line 16
  2. lemma OAI.CoulombObservation.dyadicObservationWidth_pos line 18
  3. lemma OAI.CoulombObservation.dyadicObservationWidth_inv_sq line 21
  4. lemma OAI.CoulombObservation.dyadicObservationRatio_nonneg line 30
  5. lemma OAI.CoulombObservation.dyadicObservationRatio_le_half line 32
  6. lemma OAI.CoulombObservation.geometric_sum_le_two line 37
  7. lemma OAI.CoulombObservation.dyadicObservation_inv_sq_sum line 47
  8. theorem OAI.CoulombAtom.quantum_dyadic_observation_event_tilt line 60
  9. def OAI.CoulombObservation.scaleObservationArray line 111
  10. lemma OAI.CoulombObservation.scaleObservationArray_apply line 115
  11. lemma OAI.CoulombObservation.scaleObservationArray_reindex line 119
  12. def OAI.CoulombAtom.physicalObservationArray line 129
  13. def OAI.CoulombAtom.physicalObservationEvent line 133
  14. def OAI.CoulombAtom.physicalObservationProbability line 138
  15. lemma OAI.CoulombAtom.physicalObservationEvent_eq line 143
  16. lemma OAI.CoulombAtom.scaledObservationEvent_symmetric line 158
  17. lemma OAI.CoulombAtom.quantumEventProbability_eq_physical line 167
  18. theorem OAI.CoulombAtom.quantum_physical_observation_event_tilt line 181
  19. theorem OAI.CoulombAtom.quantum_physical_dyadic_event_tilt line 209