OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CubeIntegral.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The normalized tensor cell integral is the ordinary Euclidean volume integral on the translated cube, with no change of volume convention.

  1. def OAI.ContinuumCoulomb.cubeTripleBox line 13
  2. theorem OAI.ContinuumCoulomb.cubeTripleBox_measurable line 17
  3. theorem OAI.ContinuumCoulomb.cubeTripleBox_preimage line 21
  4. theorem OAI.ContinuumCoulomb.cube_setIntegral_triple line 42
  5. theorem OAI.ContinuumCoulomb.centered_interval_integral line 50
  6. theorem OAI.ContinuumCoulomb.centered_triple_integral line 57
  7. theorem OAI.ContinuumCoulomb.positionCellIntegral_eq_setIntegral line 87