OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarSiteCutoffs.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Actual scaled cutoffs for separated planar sites. Their square partition has a localization cost of order D⁻² independent of site count.

  1. def OAI.ContinuumCoulomb.planarSiteAngle line 16
  2. theorem OAI.ContinuumCoulomb.planarSiteAngle_C1 line 19
  3. theorem OAI.ContinuumCoulomb.planarSiteAngle_support line 24
  4. theorem OAI.ContinuumCoulomb.planarSiteAngle_disjoint line 40
  5. theorem OAI.ContinuumCoulomb.planarSiteAngle_inner line 54
  6. def OAI.ContinuumCoulomb.planarSitePartition line 64
  7. theorem OAI.ContinuumCoulomb.planarSitePartition_C1 line 67
  8. theorem OAI.ContinuumCoulomb.planarSitePartition_square_sum line 71
  9. theorem OAI.ContinuumCoulomb.planarSitePartition_site_inner line 76
  10. theorem OAI.ContinuumCoulomb.planarSiteAngle_partial line 82
  11. def OAI.ContinuumCoulomb.planarSiteDerivativeBound line 96
  12. theorem OAI.ContinuumCoulomb.planarSiteDerivativeBound_nonnegative line 99
  13. theorem OAI.ContinuumCoulomb.planarSiteAngle_partial_bound line 105
  14. theorem OAI.ContinuumCoulomb.planarSitePartition_direction_bound line 115
  15. theorem OAI.ContinuumCoulomb.planarSitePartition_gradient_bound line 124