OAI/Analysis/CoulombRadii/RadialBounds/SpatialAnnulus.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NeutralAtom.rawCount_le_packetMass line 13
  2. def OAI.NeutralAtom.spatialAnnulus line 31
  3. theorem OAI.NeutralAtom.measurableSet_spatialAnnulus line 33
  4. theorem OAI.NeutralAtom.packetMass_annulus_sandwich line 37
  5. theorem OAI.NeutralAtom.conditional_integral_square_le line 85
  6. theorem OAI.NeutralAtom.conditional_l2_le line 94
  7. theorem OAI.NeutralAtom.exteriorMass_sub line 100
  8. theorem OAI.NeutralAtom.dyadic_tail_bound line 122
  9. def OAI.NeutralAtom.Admissible line 153
  10. def OAI.NeutralAtom.ExpectedExteriorAsymptotic line 158
  11. def OAI.NeutralAtom.radiusChargeThreshold line 166
  12. theorem OAI.NeutralAtom.radius_scales_admissible line 169
  13. theorem OAI.NeutralAtom.iterated_limits_of_expected_exterior_asymptotic line 188
  14. theorem OAI.NeutralAtom.rawExpectation_count_le_l2 line 233
  15. theorem OAI.NeutralAtom.small_shell_bounds_of_count_control line 244
  16. theorem OAI.NeutralAtom.scaled_dyadic_tail_bound line 281
  17. theorem OAI.NeutralAtom.tails_converge_of_annuli line 292