OAI/Analysis/CoulombIonization/RadialBounds/InverseNumericalStatementsBarrier.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.inverseDensityError line 21
  2. def OAI.CoulombAtom.inversePotentialError line 26
  3. def OAI.CoulombAtom.inverseGapBudget line 32
  4. def OAI.CoulombAtom.LowInverseNumerics line 35
  5. def OAI.CoulombAtom.HighInverseNumerics line 46
  6. lemma OAI.CoulombAtom.scaled_div_pow_constant line 61
  7. lemma OAI.CoulombAtom.inverse_density_error_tendsto line 68
  8. theorem OAI.CoulombAtom.low_inverse_numerics_eventually line 86
  9. lemma OAI.CoulombAtom.inverse_unscaled_oscillation_tendsto line 143
  10. theorem OAI.CoulombAtom.high_inverse_numerics_eventually line 157