OAI/Analysis/CoulombIonization/FieldAnalysis/RetainedKineticLower.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombNeumann.retainedPressure_value_integrable line 20
  2. lemma OAI.CoulombNeumann.physicalPressure_spin_integrable line 31
  3. theorem OAI.CoulombAtom.SobolevFermion.neumann_retained line 45
  4. theorem OAI.CoulombAtom.FormAdmissible.neumann_retained line 61
  5. lemma OAI.CoulombNeumann.retained_slice_pressure_integrable line 79
  6. lemma OAI.CoulombNeumann.retained_slice_pressure_sum_integrable line 94
  7. lemma OAI.CoulombNeumann.retained_section_measurable line 100
  8. theorem OAI.CoulombAtom.CoreAntisymmetric.neumann_retained_slices line 110
  9. lemma OAI.CoulombNeumann.pointRepulsion_join_integrable line 142
  10. lemma OAI.CoulombNeumann.retained_slice_direct_integrable line 159
  11. lemma OAI.CoulombNeumann.retained_slice_direct_sum_integrable line 183
  12. theorem OAI.CoulombAtom.CoreAntisymmetric.retained_repulsion_slices line 194