OAI/Analysis/CoulombIonization/RadialBounds/RootMomentCauchyBarrier.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.integrable_sqrt_mul_sqrt line 19
  2. lemma OAI.CoulombAtom.sum_integral_sqrt_mul_sqrt_le line 33
  3. lemma OAI.CoulombAtom.rawFormPair_integrable line 54
  4. lemma OAI.CoulombAtom.rawBallFirst_le_sqrt_count line 59
  5. lemma OAI.CoulombAtom.collar_count_le_rawBallFirst line 73
  6. lemma OAI.CoulombAtom.radial_ims_le_sqrt_count line 109
  7. def OAI.CoulombAtom.localCellRadius line 122
  8. def OAI.CoulombAtom.localOffsetMass line 123
  9. lemma OAI.CoulombAtom.localCellRadius_pos line 126
  10. lemma OAI.CoulombAtom.localOffsetMass_one_le line 129
  11. lemma OAI.CoulombAtom.exists_localCountStencil line 133
  12. def OAI.CoulombAtom.localCountStencil line 151
  13. lemma OAI.CoulombAtom.localCountStencil_norm line 152
  14. lemma OAI.CoulombAtom.localCountStencil_cover line 154
  15. lemma OAI.CoulombAtom.localCellRadius_near line 158
  16. lemma OAI.CoulombAtom.localOffsetMass_near line 172
  17. lemma OAI.CoulombAtom.localCountStencil_scaled_cover line 198
  18. lemma OAI.CoulombAtom.rawBallCount_le_cover line 218
  19. lemma OAI.CoulombAtom.rawCountMoment_le_cover line 236