OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/WellCover.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A cover of the actual well support by boxes whose total volume is linear in the number of wells and the vertical cutoff radius.

  1. def OAI.ContinuumCoulomb.wellCoverBox line 14
  2. theorem OAI.ContinuumCoulomb.mem_wellCoverBox line 17
  3. theorem OAI.ContinuumCoulomb.wellCoverBox_isClosed line 33
  4. theorem OAI.ContinuumCoulomb.wellCoverBox_measure_ne_top line 37
  5. theorem OAI.ContinuumCoulomb.wellCoverBox_volume line 43
  6. theorem OAI.ContinuumCoulomb.manufacturedWellField_support_cover line 51
  7. theorem OAI.ContinuumCoulomb.wellCover_volume_bound line 74