OAI/Analysis/CoulombIonization/RadialBounds/SharpErrorLimitBarrier.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.patch_power_ratio line 19
  2. lemma OAI.CoulombAtom.patch_sqrt_ratio line 24
  3. def OAI.CoulombAtom.weightedDimensionlessPatch line 31
  4. lemma OAI.CoulombAtom.dimensionlessPatchRemainder_weight line 39
  5. theorem OAI.CoulombAtom.dimensionlessPatchRemainder_div_tendsto line 53
  6. lemma OAI.CoulombAtom.dimensionlessLocalPotential_tendsto line 80
  7. theorem OAI.CoulombAtom.dimensionlessPotentialRemainder_tendsto line 89
  8. lemma OAI.CoulombAtom.microscopicWidth_eq line 124
  9. lemma OAI.CoulombAtom.microscopic_collar line 129
  10. lemma OAI.CoulombAtom.normalized_excess_ratio line 140
  11. theorem OAI.CoulombAtom.physical_local_mass_tendsto line 145
  12. theorem OAI.CoulombAtom.physical_potential_error_tendsto line 168
  13. theorem OAI.CoulombAtom.physical_patch_error_tendsto line 196
  14. theorem OAI.CoulombAtom.physical_master_error_tendsto line 220