OAI/Analysis/CoulombIonization/RadialBounds/StripAveraging.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombRadialAveraging.slidingBit line 15
  2. def OAI.CoulombRadialAveraging.slidingCount line 17
  3. def OAI.CoulombRadialAveraging.upperCount line 20
  4. lemma OAI.CoulombRadialAveraging.slidingBit_nonneg line 23
  5. lemma OAI.CoulombRadialAveraging.slidingBit_le_one line 26
  6. lemma OAI.CoulombRadialAveraging.slidingBit_measurable line 29
  7. lemma OAI.CoulombRadialAveraging.slidingCount_nonneg line 35
  8. lemma OAI.CoulombRadialAveraging.slidingCount_le line 38
  9. lemma OAI.CoulombRadialAveraging.upperCount_nonneg line 44
  10. lemma OAI.CoulombRadialAveraging.upperCount_le line 48
  11. lemma OAI.CoulombRadialAveraging.slidingCount_measurable line 53
  12. lemma OAI.CoulombRadialAveraging.upperCount_measurable line 59
  13. lemma OAI.CoulombRadialAveraging.slidingCount_sq_integrable line 66
  14. lemma OAI.CoulombRadialAveraging.upperCount_sq_integrable line 76
  15. lemma OAI.CoulombRadialAveraging.slidingBit_eq_indicator line 86
  16. lemma OAI.CoulombRadialAveraging.slidingBit_integrable line 91
  17. lemma OAI.CoulombRadialAveraging.slidingBit_integral line 96
  18. lemma OAI.CoulombRadialAveraging.slidingBit_setIntegral_le line 103
  19. lemma OAI.CoulombRadialAveraging.slidingCount_eq_sum_upper line 109
  20. lemma OAI.CoulombRadialAveraging.upperCount_eq_card line 122
  21. theorem OAI.CoulombRadialAveraging.slidingCount_square_integral line 127
  22. theorem OAI.CoulombRadialAveraging.expected_slidingCount_square_integral line 163
  23. theorem OAI.CoulombRadialAveraging.exists_radius_expected_square line 176