OAI/Analysis/CoulombIonization/FieldAnalysis/ScaledSmearPressure.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombNeumann.vartheta_even line 17
  2. lemma OAI.CoulombNeumann.varthetaScaled_even line 19
  3. def OAI.CoulombNeumann.physicalSmear line 22
  4. lemma OAI.CoulombNeumann.physicalSmear_nonneg line 25
  5. lemma OAI.CoulombNeumann.physicalSmear_le line 27
  6. lemma OAI.CoulombNeumann.physicalSmear_measurable line 30
  7. lemma OAI.CoulombNeumann.physicalSmear_scaled line 38
  8. lemma OAI.CoulombNeumann.inverse_cube_rpow line 48
  9. lemma OAI.CoulombNeumann.physicalSmear_rpow line 52
  10. lemma OAI.CoulombNeumann.physicalSmear_pressure_integrable line 58
  11. lemma OAI.CoulombNeumann.integral_physicalSmear_pressure line 63
  12. def OAI.CoulombNeumann.physicalPressure line 71
  13. def OAI.CoulombNeumann.physicalPressureAverage line 74
  14. lemma OAI.CoulombNeumann.physicalPressure_measurable line 77
  15. lemma OAI.CoulombNeumann.physicalPressure_nonneg line 79
  16. lemma OAI.CoulombNeumann.physicalPressureAverage_measurable line 82
  17. lemma OAI.CoulombNeumann.physicalPressureAverage_nonneg line 86
  18. lemma OAI.CoulombNeumann.physicalPressureAverage_le line 88
  19. theorem OAI.CoulombNeumann.physicalPressure_le_average line 92