OAI/Analysis/CoulombIonization/Localization/ConditionalRetainedGap.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CoulombAtom.conditional_retained_patch_gap line 23
  2. theorem OAI.CoulombAtom.actual_retained_patch_gap line 60
  3. def OAI.CoulombAtom.finiteCorePatchBound line 107
  4. lemma OAI.CoulombAtom.finiteCorePatchBound_nonneg line 109
  5. lemma OAI.CoulombAtom.conditionalPatchField_upper line 112
  6. def OAI.CoulombAtom.weightedPatchMass line 132
  7. lemma OAI.CoulombAtom.weightedPatchMass_nonneg line 137
  8. lemma OAI.CoulombAtom.weightedPatchMass_integrable line 142
  9. lemma OAI.CoulombAtom.coreSlice_priceExcess_integrable line 160
  10. def OAI.CoulombAtom.weightedPatchGap line 166
  11. lemma OAI.CoulombAtom.weightedPatchGap_nonneg line 172
  12. theorem OAI.CoulombAtom.conditionalPatchGap_upper line 178
  13. theorem OAI.CoulombAtom.weightedPatchGap_integrable line 212