OAI/Analysis/CoulombIonization/FieldAnalysis/RetainedSmear.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombNeumann.retainedSmear line 19
  2. lemma OAI.CoulombNeumann.retainedSmear_nonneg line 22
  3. lemma OAI.CoulombNeumann.retainedSmear_le_full line 26
  4. lemma OAI.CoulombNeumann.retainedSmear_ite line 31
  5. lemma OAI.CoulombNeumann.retainedSmear_measurable line 36
  6. lemma OAI.CoulombNeumann.retainedSmear_pressure_integrable line 46
  7. def OAI.CoulombNeumann.retainedPressure line 56
  8. lemma OAI.CoulombNeumann.retainedPressure_measurable line 59
  9. lemma OAI.CoulombNeumann.retainedPressure_nonneg line 64
  10. lemma OAI.CoulombNeumann.retainedPressure_le_full line 68
  11. lemma OAI.CoulombNeumann.retainedPressure_le_average line 73
  12. lemma OAI.CoulombNeumann.retainedSmear_support line 77
  13. lemma OAI.CoulombNeumann.integral_retainedSmear line 82
  14. lemma OAI.CoulombNeumann.varthetaScaled_support_bound line 97
  15. lemma OAI.CoulombNeumann.finiteSmear_retention line 102
  16. theorem OAI.CoulombNeumann.retained_physical_coulomb_lower line 109
  17. theorem OAI.CoulombNeumann.ae_retained_physical_coulomb_lower line 120
  18. def OAI.CoulombNeumann.retainedDirect line 138
  19. lemma OAI.CoulombNeumann.retainedDirect_nonneg line 142
  20. lemma OAI.CoulombNeumann.retainedDirect_measurable line 148
  21. def OAI.CoulombNeumann.pointRepulsion line 164
  22. lemma OAI.CoulombNeumann.pointRepulsion_nonneg line 167
  23. lemma OAI.CoulombNeumann.pointRepulsion_mul line 171
  24. lemma OAI.CoulombNeumann.pointRepulsion_value_integrable line 181
  25. lemma OAI.CoulombNeumann.integral_pointRepulsion_value line 192
  26. lemma OAI.CoulombNeumann.retainedDirect_value_integrable line 208
  27. theorem OAI.CoulombAtom.SobolevFermion.retained_repulsion line 226