OAI/Analysis/CoulombIonization/Localization/QuantumRawLaw.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.graphRawDensity line 19
  2. lemma OAI.CoulombAtom.graphRawDensity_nonneg line 22
  3. lemma OAI.CoulombAtom.graphRawDensity_measurable line 25
  4. lemma OAI.CoulombAtom.graphRawDensity_integrable line 31
  5. lemma OAI.CoulombAtom.graphRawDensity_integral line 37
  6. def OAI.CoulombAtom.graphRawLaw line 50
  7. lemma OAI.CoulombAtom.graphRawLaw_univ line 53
  8. lemma OAI.CoulombAtom.graphRawLaw_probability line 61
  9. lemma OAI.CoulombAtom.graphRawLaw_integral line 66
  10. lemma OAI.CoulombAtom.graphRawLaw_integrable_iff line 73
  11. def OAI.CoulombObservation.compactNoiseWeight line 90
  12. def OAI.CoulombObservation.compactNoiseNormalizer line 93
  13. def OAI.CoulombObservation.compactNoiseDensity line 95
  14. def OAI.CoulombObservation.compactNoiseLaw line 97
  15. def OAI.CoulombObservation.compactNoiseScore line 100
  16. lemma OAI.CoulombObservation.compactNoiseWeight_measurable line 103
  17. lemma OAI.CoulombObservation.compactNoiseScore_measurable line 108
  18. lemma OAI.CoulombObservation.compactNoiseWeight_nonneg line 113
  19. lemma OAI.CoulombObservation.compactNoiseWeight_le_one line 117
  20. lemma OAI.CoulombObservation.compactNoiseWeight_even line 125
  21. lemma OAI.CoulombObservation.compactNoiseScore_odd line 128
  22. lemma OAI.CoulombObservation.compactNoiseWeight_integrable line 133
  23. lemma OAI.CoulombObservation.compactNoiseWeight_support line 146
  24. lemma OAI.CoulombObservation.compactNoiseWeight_integral_pos line 154
  25. lemma OAI.CoulombObservation.compactNoiseNormalizer_pos line 159
  26. lemma OAI.CoulombObservation.compactNoiseDensity_nonneg line 162
  27. lemma OAI.CoulombObservation.compactNoiseDensity_measurable line 165
  28. lemma OAI.CoulombObservation.compactNoiseDensity_integrable line 168
  29. lemma OAI.CoulombObservation.compactNoiseDensity_integral line 171
  30. instance OAI.CoulombObservation.compactNoiseLaw_probability line 176
  31. lemma OAI.CoulombObservation.compactNoiseLaw_integral line 183