OAI/Analysis/CoulombIonization/FieldAnalysis/CubeTranslationAverage.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombNeumann.cubeIndex line 19
  2. def OAI.CoulombNeumann.sameCube line 21
  3. lemma OAI.CoulombNeumann.sameCube_nonneg line 23
  4. lemma OAI.CoulombNeumann.sameCube_le line 27
  5. lemma OAI.CoulombNeumann.cubeIndex_measurable line 32
  6. lemma OAI.CoulombNeumann.sameCube_measurable line 35
  7. lemma OAI.CoulombNeumann.sameCube_t_measurable line 42
  8. lemma OAI.CoulombNeumann.sameCube_I_integrable line 45
  9. lemma OAI.CoulombNeumann.cubeChar_sub_cubeShift line 54
  10. lemma OAI.CoulombNeumann.sameCube_periodization line 63
  11. lemma OAI.CoulombNeumann.cubeOverlap_alternative line 76
  12. lemma OAI.CoulombNeumann.cubeOverlap_alternative_integrable line 85
  13. theorem OAI.CoulombNeumann.integral_sameCube line 93
  14. lemma OAI.CoulombNeumann.integral_interval_cos_int line 113
  15. def OAI.CoulombNeumann.cosMode line 126
  16. lemma OAI.CoulombNeumann.cosMode_integrable line 130
  17. lemma OAI.CoulombNeumann.cosMode_product_integral line 133
  18. def OAI.CoulombNeumann.cosNormalization line 165
  19. def OAI.CoulombNeumann.neumannMode line 167
  20. lemma OAI.CoulombNeumann.neumannMode_inner line 171