OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/SlabResidualScale.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A polynomial choice of slab dimensions makes the actual orbital residual small. The twenty-fourth moment absorbs the total slab mass.

  1. theorem OAI.ContinuumCoulomb.slabDomain_volume line 12
  2. def OAI.ContinuumCoulomb.slabGrowthConstant line 23
  3. theorem OAI.ContinuumCoulomb.slabUniformBound_polynomial line 26
  4. def OAI.ContinuumCoulomb.slabResidualPolynomialBound line 37
  5. theorem OAI.ContinuumCoulomb.div_pow_le_div_sq line 42
  6. theorem OAI.ContinuumCoulomb.slabOrbitalResidual_polynomial_bound line 46