OAI/Analysis/CoulombIonization/Localization/ArraySymmetry.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombObservation.arrayReindex line 17
  2. lemma OAI.CoulombObservation.arrayReindex_apply line 21
  3. lemma OAI.CoulombObservation.arrayReindex_preserving line 27
  4. lemma OAI.CoulombObservation.arrayLikelihood_reindex line 34
  5. def OAI.CoulombAtom.flattenConfiguration line 66
  6. lemma OAI.CoulombAtom.flattenConfiguration_apply line 70
  7. lemma OAI.CoulombAtom.flattenConfiguration_direction line 73
  8. lemma OAI.CoulombAtom.lineDeriv_flattenConfiguration line 80
  9. def OAI.CoulombAtom.flatRawLaw line 87
  10. lemma OAI.CoulombAtom.flatRawLaw_probability line 90
  11. def OAI.CoulombAtom.quantumEventLikelihood line 96
  12. def OAI.CoulombAtom.quantumEventProbability line 100
  13. lemma OAI.CoulombAtom.quantumEventProbability_eq_flat line 104
  14. lemma OAI.CoulombAtom.quantumEventLikelihood_nonneg line 112
  15. lemma OAI.CoulombAtom.quantumEventLikelihood_le_one line 117
  16. lemma OAI.CoulombAtom.quantumEventLikelihood_measurable line 122
  17. def OAI.CoulombAtom.QuantumEventSymmetric line 128
  18. lemma OAI.CoulombAtom.quantumEventLikelihood_symmetric line 133