OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CubeGeometry.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Actual Euclidean mesh cells: volume, radius, node containment, and disjoint interiors. These retain the volume normalization of the Gauss rule.

  1. def OAI.ContinuumCoulomb.positionCube line 14
  2. def OAI.ContinuumCoulomb.positionOpenCube line 17
  3. theorem OAI.ContinuumCoulomb.mem_positionCube line 20
  4. theorem OAI.ContinuumCoulomb.mem_positionOpenCube line 30
  5. theorem OAI.ContinuumCoulomb.positionCube_isClosed line 41
  6. theorem OAI.ContinuumCoulomb.positionOpenCube_measurable line 44
  7. theorem OAI.ContinuumCoulomb.positionOpenCube_subset line 49
  8. theorem OAI.ContinuumCoulomb.positionCube_volume line 54
  9. theorem OAI.ContinuumCoulomb.positionOpenCube_volume line 63
  10. theorem OAI.ContinuumCoulomb.positionOpenCube_ae_eq line 73
  11. theorem OAI.ContinuumCoulomb.cubePoint_mem_positionCube line 80
  12. theorem OAI.ContinuumCoulomb.positionCube_norm_sub_le line 96
  13. theorem OAI.ContinuumCoulomb.positionCube_isCompact line 110
  14. theorem OAI.ContinuumCoulomb.positionCube_diameter_bound line 116
  15. theorem OAI.ContinuumCoulomb.grid_openCubes_disjoint line 122
  16. theorem OAI.ContinuumCoulomb.grid_cell_integral_sum_le line 138
  17. theorem OAI.ContinuumCoulomb.grid_cell_integral_sum_le_on line 152