OAI/Analysis/CoulombIonization/RadialBounds/Average.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombBarrier.deterministicBound_integrable_section line 19
  2. lemma OAI.CoulombBarrier.deterministicBound_integrable_test line 26
  3. lemma OAI.CoulombBarrier.average_measurable line 41
  4. lemma OAI.CoulombBarrier.average_deterministic_bound line 47
  5. lemma OAI.CoulombBarrier.average_continuous line 58
  6. theorem OAI.CoulombBarrier.weak_lower_average line 72
  7. theorem OAI.CoulombBarrier.conditional_all_properties line 94
  8. lemma OAI.CoulombBarrier.DeterministicLocalBound.add line 108
  9. lemma OAI.CoulombBarrier.DeterministicLocalBound.spatial_comp line 116
  10. lemma OAI.CoulombBarrier.DeterministicLocalBound.bounded_mul line 126
  11. lemma OAI.CoulombBarrier.deterministicBound_locallyIntegrable line 137
  12. lemma OAI.CoulombBarrier.average_locallyIntegrable line 148
  13. theorem OAI.CoulombBarrier.weak_spatial_average line 154