OAI/Analysis/CoulombIonization/RadialBounds/SharpLocalPotentialBarrier.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.sharpOrdinaryDensityConstant_nonneg line 18
  2. lemma OAI.CoulombAtom.ordinaryDensity_power_integrable line 24
  3. lemma OAI.CoulombAtom.ordinaryDensity_power_ball_mono line 30
  4. theorem OAI.CoulombAtom.sharp_cell_local_potential line 38
  5. theorem OAI.CoulombAtom.unshifted_cell_ordinary_density line 54
  6. theorem OAI.CoulombAtom.sharp_selected_patch_energy line 89
  7. def OAI.CoulombAtom.sharpLocalPotentialBudget line 139
  8. def OAI.CoulombAtom.sharpPotentialRemainder line 142
  9. theorem OAI.CoulombAtom.sharp_selected_potential_error line 149