OAI/Analysis/CoulombIonization/RadialBounds/CoulombTailNumerics.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.tailRadius line 14
  2. def OAI.CoulombAtom.tailWeight line 15
  3. lemma OAI.CoulombAtom.tailRadius_pos line 16
  4. lemma OAI.CoulombAtom.tailWeight_pos line 18
  5. lemma OAI.CoulombAtom.tailRadius_succ line 19
  6. lemma OAI.CoulombAtom.tailRadius_zero line 21
  7. lemma OAI.CoulombAtom.tailRadius_mono line 22
  8. lemma OAI.CoulombAtom.sum_tailWeight_le line 24
  9. lemma OAI.CoulombAtom.annularOffsetMass_sq_le line 30
  10. lemma OAI.CoulombAtom.tailRadius_weight_identity line 43
  11. lemma OAI.CoulombAtom.tailWeight_le_one line 51
  12. lemma OAI.CoulombAtom.tail_annular_scale line 54
  13. lemma OAI.CoulombAtom.finite_tail_cauchy line 82
  14. def OAI.CoulombAtom.truncatedTailWeight line 95
  15. lemma OAI.CoulombAtom.truncatedTailWeight_measurable line 97
  16. lemma OAI.CoulombAtom.truncatedTailWeight_nonneg line 101
  17. lemma OAI.CoulombAtom.truncatedTailWeight_le line 103
  18. lemma OAI.CoulombAtom.truncatedTailWeight_zero line 107
  19. lemma OAI.CoulombAtom.truncatedTailWeight_step line 110
  20. lemma OAI.CoulombAtom.raw_truncated_tail_le_shells line 137
  21. lemma OAI.CoulombAtom.truncatedTailWeight_tendsto line 150
  22. lemma OAI.CoulombAtom.raw_truncated_tail_tendsto line 159
  23. lemma OAI.CoulombAtom.rawWeightedCount_sq_integrable line 164
  24. lemma OAI.CoulombAtom.truncated_tail_moment_tendsto line 172