OAI/Analysis/CoulombIonization/Localization/ObservationSmooth.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombObservation.compactNoiseWeight_eq_glue line 17
  2. lemma OAI.CoulombObservation.compactNoiseWeight_contDiff line 24
  3. lemma OAI.CoulombObservation.compactNoiseDensity_contDiff line 28
  4. lemma OAI.CoulombObservation.compactNoiseWeight_hasDerivAt line 31
  5. lemma OAI.CoulombObservation.compactNoiseDensity_hasDerivAt line 46
  6. lemma OAI.CoulombObservation.compactNoiseWeight_compactSupport line 52
  7. lemma OAI.CoulombObservation.compactNoiseDensity_compactSupport line 61
  8. def OAI.CoulombObservation.compactNoiseKernel line 69
  9. lemma OAI.CoulombObservation.compactNoiseKernel_nonneg line 72
  10. lemma OAI.CoulombObservation.compactNoiseKernel_even line 75
  11. lemma OAI.CoulombObservation.compactNoiseKernel_contDiff line 79
  12. lemma OAI.CoulombObservation.compactNoiseKernel_integrable line 83
  13. lemma OAI.CoulombObservation.compactNoiseKernel_compactSupport line 87
  14. lemma OAI.CoulombObservation.compactNoiseLaw_apply line 101
  15. lemma OAI.CoulombObservation.compactNoiseLaw_pi line 107
  16. lemma OAI.CoulombObservation.compactNoiseLaw_pi_integral line 120
  17. lemma OAI.CoulombObservation.compactNoiseKernel_hasFDerivAt line 128
  18. lemma OAI.CoulombObservation.compactNoiseKernel_fderiv_apply line 147