OAI/Analysis/CoulombIonization/FieldAnalysis/CubeDensity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombNeumann.integral_sameCube_y line 19
  2. lemma OAI.CoulombNeumann.sameCube_y_integrable line 30
  3. def OAI.CoulombNeumann.cubeDensity line 40
  4. def OAI.CoulombNeumann.cubeAssignment line 43
  5. lemma OAI.CoulombNeumann.cubeDensity_count line 46
  6. lemma OAI.CoulombNeumann.cubeDensity_nonneg line 53
  7. lemma OAI.CoulombNeumann.cubeDensity_le line 56
  8. lemma OAI.CoulombNeumann.cellCount_rpow_query line 60
  9. lemma OAI.CoulombNeumann.cubeDensity_rpow line 75
  10. lemma OAI.CoulombNeumann.cubeDensity_rpow_integrable line 84
  11. theorem OAI.CoulombNeumann.integral_cubeDensity_rpow line 89
  12. lemma OAI.CoulombNeumann.integral_cubeDensity_t line 95
  13. theorem OAI.CoulombNeumann.average_pressure line 109