OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedGramSpacing.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A fixed logarithmic spacing controls the total leakage for every polynomial number of sites. The exponent is chosen once for the reduction.

  1. def OAI.ContinuumCoulomb.localLeakageConstant line 13
  2. theorem OAI.ContinuumCoulomb.localLeakageConstant_nonnegative line 16
  3. theorem OAI.ContinuumCoulomb.localLeakageBound_log line 20
  4. theorem OAI.ContinuumCoulomb.exists_localizedGram_spacing line 26
  5. theorem OAI.ContinuumCoulomb.exists_uniform_localizedGram_coercivity line 61