OAI/Analysis/CoulombIonization/Variational/CorePriceExcess.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.corePriceExcess line 162
  2. def OAI.CoulombAtom.normalizedCoreField line 165
  3. lemma OAI.CoulombAtom.corePriceExcess_nonneg line 168
  4. theorem OAI.CoulombAtom.vacant_core_field_cap line 172
  5. lemma OAI.CoulombAtom.vacant_core_field_cap_normalized line 201
  6. theorem OAI.CoulombAtom.vacant_core_quadratic_cap line 210
  7. def OAI.CoulombAtom.coreCapEnvelope line 237
  8. lemma OAI.CoulombAtom.coreCapEnvelope_nonneg line 241
  9. lemma OAI.CoulombAtom.vacant_core_field_cap_all_mass line 247
  10. theorem OAI.CoulombAtom.vacant_core_uniform_field_cap line 258
  11. lemma OAI.CoulombAtom.coreCapEnvelope_weighted_square line 278
  12. lemma OAI.CoulombAtom.SobolevVector.coreSlice_excess_integrable line 303
  13. lemma OAI.CoulombAtom.SobolevVector.coreSlice_envelope_measurable line 310
  14. lemma OAI.CoulombAtom.coreSlice_envelope_square_integrable line 318
  15. theorem OAI.CoulombAtom.integrated_core_envelope_square line 333