OAI/Analysis/CoulombRadii/FormDomain/Translate.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Coulomb.weak_partial_translate line 19
  2. def OAI.Coulomb.H1Vector.translate line 42
  3. lemma OAI.Coulomb.permute_add line 52
  4. lemma OAI.Coulomb.mass_translate line 57
  5. lemma OAI.Coulomb.kinetic_translate line 64
  6. def OAI.Coulomb.commonShift line 73
  7. lemma OAI.Coulomb.Antisymmetric.translate_common line 76
  8. def OAI.Coulomb.spinSpaceMeasure line 84
  9. instance OAI.Coulomb.spinSpaceMeasure_sigmaFinite line 85
  10. def OAI.Coulomb.centeredSpinCube line 89
  11. lemma OAI.Coulomb.centeredSpinCube_measurable line 91
  12. def OAI.Coulomb.centeredSpinMeasure line 94
  13. instance OAI.Coulomb.centeredSpinMeasure_sigmaFinite line 96
  14. def OAI.Coulomb.spinShift line 100
  15. lemma OAI.Coulomb.spinShift_measurePreserving line 104
  16. lemma OAI.Coulomb.spinCubeMeasure_eq_restrict line 108
  17. lemma OAI.Coulomb.shift_centeredCube_measurePreserving line 115
  18. lemma OAI.Coulomb.firstParticleDensity_equiv line 130
  19. lemma OAI.Coulomb.cubeState_translate line 148
  20. theorem OAI.Coulomb.centered_density_power_bound line 152